import Init

def OA_statement : Prop := ((fun (cost : List (Sum (Option Nat) (Option Nat)) → Nat) =>
(fun (apply : List (Sum (Option Nat) (Option Nat)) → List Nat → Option (List Nat)) =>
(fun (best : List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat))) =>
(fun (diff : Nat → List Nat → List Nat → List (Sum (Option Nat) (Option Nat))) =>
∀ (xs ys : List Nat) (fuel : Nat), xs.length + ys.length ≤ fuel →
 apply (diff fuel xs ys) xs = some ys ∧
 ∀ script : List (Sum (Option Nat) (Option Nat)), apply script xs = some ys → cost (diff fuel xs ys) ≤ cost script
) (fun fuel => Nat.rec (fun _ _ : List Nat => [])
 (fun _ recur xs ys => match xs, ys with
 | [], _ => ys.map (fun y => Sum.inr (some y))
 | _, [] => List.replicate xs.length (Sum.inr none)
 | x :: xt, y :: yt => if x = y then Sum.inl none :: recur xt yt
   else best (Sum.inl (some y) :: recur xt yt)
             (Sum.inr none :: recur xt ys)
             (Sum.inr (some y) :: recur xs yt)) fuel)
) (fun a b c => if cost a ≤ cost b ∧ cost a ≤ cost c then a else if cost b ≤ cost c then b else c)
) (fun script => List.rec (fun xs : List Nat => some xs)
 (fun edit _ rest xs => match edit, xs with
 | .inl none, x :: xt => (rest xt).map (fun ys => x :: ys)
 | .inl (some y), _ :: xt => (rest xt).map (fun ys => y :: ys)
 | .inr none, _ :: xt => rest xt
 | .inr (some y), _ => (rest xs).map (fun ys => y :: ys)
 | _, [] => none) script)
) (fun script => script.foldr (fun edit n => match edit with | .inl none => n | _ => n + 1) 0))

theorem OA_target : OA_statement :=
  by
    dsimp only [OA_statement]
    refine (fun (main : ∀ (cost : List (Sum (Option Nat) (Option Nat)) → Nat)
        (apply : List (Sum (Option Nat) (Option Nat)) → List Nat → Option (List Nat))
        (best : List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat)))
        (diff : Nat → List Nat → List Nat → List (Sum (Option Nat) (Option Nat))),
        cost [] = 0 →
        (∀ s, cost (Sum.inl none :: s) = cost s) →
        (∀ y s, cost (Sum.inl (some y) :: s) = cost s + 1) →
        (∀ s, cost (Sum.inr none :: s) = cost s + 1) →
        (∀ y s, cost (Sum.inr (some y) :: s) = cost s + 1) →
        (∀ xs, apply [] xs = some xs) →
        (∀ s x xt, apply (Sum.inl none :: s) (x :: xt) = (apply s xt).map (fun ys => x :: ys)) →
        (∀ s y x xt, apply (Sum.inl (some y) :: s) (x :: xt) = (apply s xt).map (fun ys => y :: ys)) →
        (∀ s x xt, apply (Sum.inr none :: s) (x :: xt) = apply s xt) →
        (∀ s y xs, apply (Sum.inr (some y) :: s) xs = (apply s xs).map (fun ys => y :: ys)) →
        (∀ s, apply (Sum.inl none :: s) [] = none) →
        (∀ s y, apply (Sum.inl (some y) :: s) [] = none) →
        (∀ s, apply (Sum.inr none :: s) [] = none) →
        (∀ a b c, best a b c = if cost a ≤ cost b ∧ cost a ≤ cost c then a else if cost b ≤ cost c then b else c) →
        (∀ a b, diff 0 a b = []) →
        (∀ f ys, diff (f + 1) [] ys = ys.map (fun y => Sum.inr (some y))) →
        (∀ f x xt, diff (f + 1) (x :: xt) [] = List.replicate (xt.length + 1) (Sum.inr none)) →
        (∀ f x xt y yt, diff (f + 1) (x :: xt) (y :: yt) =
          if x = y then Sum.inl none :: diff f xt yt
          else best (Sum.inl (some y) :: diff f xt yt) (Sum.inr none :: diff f xt (y :: yt)) (Sum.inr (some y) :: diff f (x :: xt) yt)) →
        ∀ (xs ys : List Nat) (fuel : Nat), xs.length + ys.length ≤ fuel →
          apply (diff fuel xs ys) xs = some ys ∧
          ∀ script, apply script xs = some ys → cost (diff fuel xs ys) ≤ cost script) =>
        main _ _ _ _ rfl (fun _ => rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
      (fun _ => rfl) (fun _ _ _ => rfl) (fun _ _ _ _ => rfl) (fun _ _ _ => rfl) (fun _ _ _ => rfl)
      (fun _ => rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
      (fun _ _ _ => rfl) (fun _ _ _ _ _ => rfl)) ?_
    intro cost apply best diff hc0 hc1 hc2 hc3 hc4 ha0 ha1 ha2 ha3 ha4 ha5 ha5' ha6 hb hd0 hd1 hd2 hd3
    have bestFacts : ∀ a b c,
        (cost (best a b c) ≤ cost a ∧ cost (best a b c) ≤ cost b ∧ cost (best a b c) ≤ cost c) ∧
        (best a b c = a ∨ best a b c = b ∨ best a b c = c) := by
      intro a b c
      rewrite [hb]; (try with_reducible exact rfl)
      split
      next h1 => exact ⟨⟨Nat.le_refl _, h1.1, h1.2⟩, Or.inl rfl⟩
      next h1 =>
        split
        next h2 => exact ⟨⟨by omega, Nat.le_refl _, h2⟩, Or.inr (Or.inl rfl)⟩
        next h2 => exact ⟨⟨by omega, by omega, Nat.le_refl _⟩, Or.inr (Or.inr rfl)⟩
    have FI : ∀ f g a b, a.length + b.length ≤ f → a.length + b.length ≤ g → diff f a b = diff g a b := by
      intro f
      induction f with
      | zero =>
        intro g a b hf hg
        have ha : a = [] := List.eq_nil_of_length_eq_zero (by omega)
        have hb' : b = [] := List.eq_nil_of_length_eq_zero (by omega)
        subst ha
        subst hb'
        cases g with
        | zero => exact rfl
        | succ g => rewrite [hd0, hd1]; (try with_reducible exact rfl); exact rfl
      | succ f ih =>
        intro g a b hf hg
        cases g with
        | zero =>
          have ha : a = [] := List.eq_nil_of_length_eq_zero (by omega)
          have hb' : b = [] := List.eq_nil_of_length_eq_zero (by omega)
          subst ha
          subst hb'
          rewrite [hd0, hd1]; (try with_reducible exact rfl)
          exact rfl
        | succ g =>
          cases a with
          | nil => rewrite [hd1, hd1]; (try with_reducible exact rfl)
          | cons x xt =>
            cases b with
            | nil => rewrite [hd2, hd2]; (try with_reducible exact rfl)
            | cons y yt =>
              simp only [List.length_cons] at hf hg
              rewrite [hd3, hd3, ih g xt yt (by omega) (by omega),
                ih g xt (y :: yt) (by simp only [List.length_cons]; omega) (by simp only [List.length_cons]; omega),
                ih g (x :: xt) yt (by simp only [List.length_cons]; omega) (by simp only [List.length_cons]; omega)]; (try with_reducible exact rfl)
    have insApply : ∀ (b xs : List Nat), apply (b.map (fun y => Sum.inr (some y))) xs = some (b ++ xs) := by
      intro b xs
      induction b with
      | nil => exact ha0 xs
      | cons y bt ih =>
        rewrite [List.map_cons, ha4, ih]; (try with_reducible exact rfl)
        exact rfl
    have delApply : ∀ (l : List Nat), apply (List.replicate l.length (Sum.inr none)) l = some [] := by
      intro l
      induction l with
      | nil => exact ha0 []
      | cons x xt ih =>
        show apply (Sum.inr none :: List.replicate xt.length (Sum.inr none)) (x :: xt) = some []
        rewrite [ha3, ih]; (try with_reducible exact rfl)
    have insCost : ∀ (b : List Nat), cost (b.map (fun y => Sum.inr (some y))) = b.length := by
      intro b
      induction b with
      | nil => exact hc0
      | cons y bt ih =>
        rewrite [List.map_cons, hc4, ih]; (try with_reducible exact rfl)
        exact rfl
    have delCost : ∀ n, cost (List.replicate n (Sum.inr none)) = n := by
      intro n
      induction n with
      | zero => exact hc0
      | succ n ih =>
        show cost (Sum.inr none :: List.replicate n (Sum.inr none)) = n + 1
        rewrite [hc3, ih]; (try with_reducible exact rfl)
    have CORRs : ∀ f, (∀ a b, a.length + b.length ≤ f → apply (diff f a b) a = some b) →
        ∀ a b, a.length + b.length ≤ f + 1 → apply (diff (f + 1) a b) a = some b := by
      intro f ih a b h
      rcases a with _ | ⟨x, xt⟩
      · rewrite [hd1, insApply, List.append_nil]
        exact rfl
      rcases b with _ | ⟨y, yt⟩
      · rewrite [hd2]
        exact delApply (x :: xt)
      simp only [List.length_cons] at h
      have l1 : xt.length + yt.length ≤ f := by omega
      have l2 : xt.length + (y :: yt).length ≤ f := by simp only [List.length_cons]; omega
      have l3 : (x :: xt).length + yt.length ≤ f := by simp only [List.length_cons]; omega
      rewrite [hd3]
      by_cases hxy : x = y
      · subst hxy
        simp only [ite_true]
        rewrite [ha1, ih xt yt l1]
        exact rfl
      simp only [hxy, ite_false]
      rcases (bestFacts (Sum.inl (some y) :: diff f xt yt) (Sum.inr none :: diff f xt (y :: yt))
          (Sum.inr (some y) :: diff f (x :: xt) yt)).2 with e | e | e
      · rewrite [e, ha2, ih xt yt l1]
        exact rfl
      · rewrite [e, ha3, ih xt (y :: yt) l2]
        exact rfl
      rewrite [e, ha4, ih (x :: xt) yt l3]
      exact rfl
    have CORR : ∀ f a b, a.length + b.length ≤ f → apply (diff f a b) a = some b := by
      intro f
      induction f with
      | zero =>
        intro a b h
        have ha : a = [] := List.eq_nil_of_length_eq_zero (by omega)
        have hb' : b = [] := List.eq_nil_of_length_eq_zero (by omega)
        subst ha
        subst hb'
        rewrite [hd0, ha0]
        exact rfl
      | succ f ih => exact CORRs f ih
    obtain ⟨D, hD⟩ : ∃ D : List Nat → List Nat → Nat, ∀ f a b, a.length + b.length ≤ f → cost (diff f a b) = D a b :=
      ⟨fun a b => cost (diff (a.length + b.length) a b), fun f a b h => by
        rewrite [FI f (a.length + b.length) a b h (Nat.le_refl _)]; (try with_reducible exact rfl)⟩
    have D0 : ∀ b, D [] b = b.length := by
      intro b
      rewrite [← hD (b.length + 1) [] b (by simp only [List.length_nil]; omega), hd1, insCost]; (try with_reducible exact rfl)
    have Dnil : ∀ a, D a [] = a.length := by
      intro a
      cases a with
      | nil => rewrite [D0]; (try with_reducible exact rfl)
      | cons x xt =>
        rewrite [← hD (xt.length + 1 + 1) (x :: xt) [] (by simp only [List.length_cons, List.length_nil]; omega), hd2, delCost]; (try with_reducible exact rfl)
        exact rfl
    have D2eq : ∀ x xt yt, D (x :: xt) (x :: yt) = D xt yt := by
      intro x xt yt
      rewrite [← hD (xt.length + yt.length + 1 + 1) (x :: xt) (x :: yt) (by simp only [List.length_cons]; omega), hd3]; (try with_reducible exact rfl)
      split
      next _ =>
        rewrite [hc1, hD (xt.length + yt.length + 1) xt yt (by omega)]; (try with_reducible exact rfl)
      next h => exact absurd rfl h
    have D2ne : ∀ x xt y yt, x ≠ y →
        D (x :: xt) (y :: yt) ≤ D xt yt + 1 ∧ D (x :: xt) (y :: yt) ≤ D xt (y :: yt) + 1 ∧
        D (x :: xt) (y :: yt) ≤ D (x :: xt) yt + 1 ∧
        (D (x :: xt) (y :: yt) = D xt yt + 1 ∨ D (x :: xt) (y :: yt) = D xt (y :: yt) + 1 ∨
          D (x :: xt) (y :: yt) = D (x :: xt) yt + 1) := by
      intro x xt y yt hne
      have hf := hD (xt.length + yt.length + 1 + 1) (x :: xt) (y :: yt) (by simp only [List.length_cons]; omega)
      rewrite [hd3] at hf; (try with_reducible exact rfl)
      split at hf
      next h => exact absurd h hne
      next _ =>
        have e1 : cost (Sum.inl (some y) :: diff (xt.length + yt.length + 1) xt yt) = D xt yt + 1 := by
          rewrite [hc2, hD (xt.length + yt.length + 1) xt yt (by omega)]; (try with_reducible exact rfl)
        have e2 : cost (Sum.inr none :: diff (xt.length + yt.length + 1) xt (y :: yt)) = D xt (y :: yt) + 1 := by
          rewrite [hc3, hD (xt.length + yt.length + 1) xt (y :: yt) (by simp only [List.length_cons]; omega)]; (try with_reducible exact rfl)
        have e3 : cost (Sum.inr (some y) :: diff (xt.length + yt.length + 1) (x :: xt) yt) = D (x :: xt) yt + 1 := by
          rewrite [hc4, hD (xt.length + yt.length + 1) (x :: xt) yt (by simp only [List.length_cons]; omega)]; (try with_reducible exact rfl)
        obtain ⟨⟨b1, b2, b3⟩, bc⟩ := bestFacts (Sum.inl (some y) :: diff (xt.length + yt.length + 1) xt yt)
          (Sum.inr none :: diff (xt.length + yt.length + 1) xt (y :: yt))
          (Sum.inr (some y) :: diff (xt.length + yt.length + 1) (x :: xt) yt)
        rewrite [hf, e1] at b1; (try with_reducible exact rfl)
        rewrite [hf, e2] at b2; (try with_reducible exact rfl)
        rewrite [hf, e3] at b3; (try with_reducible exact rfl)
        refine ⟨b1, b2, b3, ?_⟩
        rcases bc with e | e | e
        · rewrite [e, e1] at hf; (try with_reducible exact rfl)
          exact Or.inl hf.symm
        · rewrite [e, e2] at hf; (try with_reducible exact rfl)
          exact Or.inr (Or.inl hf.symm)
        · rewrite [e, e3] at hf; (try with_reducible exact rfl)
          exact Or.inr (Or.inr hf.symm)
    have FOUR0 : ∀ a b, a.length + b.length ≤ 0 → ∀ c,
        D a (c :: b) ≤ D a b + 1 ∧ D (c :: a) b ≤ D a b + 1 ∧
        D a b ≤ D a (c :: b) + 1 ∧ D a b ≤ D (c :: a) b + 1 := by
      intro a b h c
      have ha : a = [] := List.eq_nil_of_length_eq_zero (by omega)
      have hb' : b = [] := List.eq_nil_of_length_eq_zero (by omega)
      subst ha
      subst hb'
      have e1 := D0 [c]
      have e2 := Dnil [c]
      have e3 := D0 []
      simp only [List.length_cons, List.length_nil] at e1 e2 e3
      omega
    have SU1 : ∀ n, (∀ a b, a.length + b.length ≤ n → ∀ c,
        D a (c :: b) ≤ D a b + 1 ∧ D (c :: a) b ≤ D a b + 1 ∧
        D a b ≤ D a (c :: b) + 1 ∧ D a b ≤ D (c :: a) b + 1) →
        ∀ a b, a.length + b.length ≤ n + 1 → ∀ c, D a (c :: b) ≤ D a b + 1 := by
      intro n ih a b h c
      rcases a with _ | ⟨x, at'⟩
      · have e1 := D0 (c :: b)
        have e2 := D0 b
        simp only [List.length_cons] at e1
        omega
      rcases b with _ | ⟨y, bt⟩
      · have e1 := Dnil at'
        have e2 := Dnil (x :: at')
        simp only [List.length_cons] at e2
        by_cases hxc : x = c
        · subst hxc
          rewrite [D2eq]
          omega
        have := (D2ne x at' c [] hxc).1
        omega
      simp only [List.length_cons] at h
      have l1 : at'.length + (y :: bt).length ≤ n := by simp only [List.length_cons]; omega
      by_cases hxc : x = c
      · subst hxc
        rewrite [D2eq]
        exact (ih at' (y :: bt) l1 x).2.2.2
      exact (D2ne x at' c (y :: bt) hxc).2.2.1
    have SU2 : ∀ n, (∀ a b, a.length + b.length ≤ n → ∀ c,
        D a (c :: b) ≤ D a b + 1 ∧ D (c :: a) b ≤ D a b + 1 ∧
        D a b ≤ D a (c :: b) + 1 ∧ D a b ≤ D (c :: a) b + 1) →
        ∀ a b, a.length + b.length ≤ n + 1 → ∀ c, D (c :: a) b ≤ D a b + 1 := by
      intro n ih a b h c
      rcases b with _ | ⟨y, bt⟩
      · have e1 := Dnil (c :: a)
        have e2 := Dnil a
        simp only [List.length_cons] at e1
        omega
      rcases a with _ | ⟨x, at'⟩
      · have e1 := D0 bt
        have e2 := D0 (y :: bt)
        simp only [List.length_cons] at e2
        by_cases hcy : c = y
        · subst hcy
          rewrite [D2eq]
          omega
        have := (D2ne c [] y bt hcy).1
        omega
      simp only [List.length_cons] at h
      have l1 : (x :: at').length + bt.length ≤ n := by simp only [List.length_cons]; omega
      by_cases hcy : c = y
      · subst hcy
        rewrite [D2eq]
        exact (ih (x :: at') bt l1 c).2.2.1
      exact (D2ne c (x :: at') y bt hcy).2.1
    have SL1 : ∀ n, (∀ a b, a.length + b.length ≤ n → ∀ c,
        D a (c :: b) ≤ D a b + 1 ∧ D (c :: a) b ≤ D a b + 1 ∧
        D a b ≤ D a (c :: b) + 1 ∧ D a b ≤ D (c :: a) b + 1) →
        ∀ a b, a.length + b.length ≤ n + 1 → ∀ c, D a b ≤ D a (c :: b) + 1 := by
      intro n ih a b h c
      rcases a with _ | ⟨x, at'⟩
      · have e1 := D0 (c :: b)
        have e2 := D0 b
        simp only [List.length_cons] at e1
        omega
      rcases b with _ | ⟨y, bt⟩
      · have e1 := Dnil at'
        have e2 := Dnil (x :: at')
        simp only [List.length_cons] at e2
        simp only [List.length_cons, List.length_nil] at h
        have l0 : at'.length + ([] : List Nat).length ≤ n := by simp only [List.length_nil]; omega
        by_cases hxc : x = c
        · subst hxc
          rewrite [D2eq]
          omega
        have i1 := (ih at' [] l0 c).2.2.1
        rcases (D2ne x at' c [] hxc).2.2.2 with e | e | e <;> omega
      simp only [List.length_cons] at h
      have l1 : at'.length + (y :: bt).length ≤ n := by simp only [List.length_cons]; omega
      by_cases hxc : x = c
      · subst hxc
        rewrite [D2eq]
        exact (ih at' (y :: bt) l1 x).2.1
      have i1 := (ih at' (y :: bt) l1 x).2.1
      have i2 := (ih at' (y :: bt) l1 c).2.2.1
      rcases (D2ne x at' c (y :: bt) hxc).2.2.2 with e | e | e <;> omega
    have SL2 : ∀ n, (∀ a b, a.length + b.length ≤ n → ∀ c,
        D a (c :: b) ≤ D a b + 1 ∧ D (c :: a) b ≤ D a b + 1 ∧
        D a b ≤ D a (c :: b) + 1 ∧ D a b ≤ D (c :: a) b + 1) →
        ∀ a b, a.length + b.length ≤ n + 1 → ∀ c, D a b ≤ D (c :: a) b + 1 := by
      intro n ih a b h c
      rcases b with _ | ⟨y, bt⟩
      · have e1 := Dnil (c :: a)
        have e2 := Dnil a
        simp only [List.length_cons] at e1
        omega
      rcases a with _ | ⟨x, at'⟩
      · have e1 := D0 bt
        have e2 := D0 (y :: bt)
        simp only [List.length_cons] at e2
        simp only [List.length_cons, List.length_nil] at h
        have l0 : ([] : List Nat).length + bt.length ≤ n := by simp only [List.length_nil]; omega
        by_cases hcy : c = y
        · subst hcy
          rewrite [D2eq]
          omega
        have i1 := (ih [] bt l0 c).2.2.2
        rcases (D2ne c [] y bt hcy).2.2.2 with e | e | e <;> omega
      simp only [List.length_cons] at h
      have l1 : (x :: at').length + bt.length ≤ n := by simp only [List.length_cons]; omega
      by_cases hcy : c = y
      · subst hcy
        rewrite [D2eq]
        exact (ih (x :: at') bt l1 c).1
      have i1 := (ih (x :: at') bt l1 y).1
      have i2 := (ih (x :: at') bt l1 c).2.2.2
      rcases (D2ne c (x :: at') y bt hcy).2.2.2 with e | e | e <;> omega
    have FOUR : ∀ n a b, a.length + b.length ≤ n → ∀ c,
        D a (c :: b) ≤ D a b + 1 ∧ D (c :: a) b ≤ D a b + 1 ∧
        D a b ≤ D a (c :: b) + 1 ∧ D a b ≤ D (c :: a) b + 1 := by
      intro n
      induction n with
      | zero => exact FOUR0
      | succ n ih => exact fun a b h c => ⟨SU1 n ih a b h c, SU2 n ih a b h c, SL1 n ih a b h c, SL2 n ih a b h c⟩
    have Drefl : ∀ a, D a a = 0 := by
      intro a
      induction a with
      | nil => rewrite [D0]; exact rfl
      | cons x xt ih => rewrite [D2eq, ih]; exact rfl
    have MINc : ∀ s, (∀ a b, apply s a = some b → D a b ≤ cost s) →
        ∀ a b, apply (Sum.inl none :: s) a = some b → D a b ≤ cost (Sum.inl none :: s) := by
      intro s ih a b h
      rcases a with _ | ⟨x, xt⟩
      · rewrite [ha5] at h
        cases h
      rewrite [ha1] at h
      rewrite [hc1]
      rcases hs : apply s xt with _ | b'
      · rewrite [hs] at h
        cases h
      rewrite [hs] at h
      injection h with h
      subst h
      rewrite [D2eq]
      exact ih xt b' hs
    have MINr : ∀ s y, (∀ a b, apply s a = some b → D a b ≤ cost s) →
        ∀ a b, apply (Sum.inl (some y) :: s) a = some b → D a b ≤ cost (Sum.inl (some y) :: s) := by
      intro s y ih a b h
      rcases a with _ | ⟨x, xt⟩
      · rewrite [ha5'] at h
        cases h
      rewrite [ha2] at h
      rewrite [hc2]
      rcases hs : apply s xt with _ | b'
      · rewrite [hs] at h
        cases h
      rewrite [hs] at h
      injection h with h
      subst h
      dsimp only
      have := ih xt b' hs
      by_cases hxy : x = y
      · subst hxy
        rewrite [D2eq]
        omega
      have := (D2ne x xt y b' hxy).1
      omega
    have MINd : ∀ s, (∀ a b, apply s a = some b → D a b ≤ cost s) →
        ∀ a b, apply (Sum.inr none :: s) a = some b → D a b ≤ cost (Sum.inr none :: s) := by
      intro s ih a b h
      rcases a with _ | ⟨x, xt⟩
      · rewrite [ha6] at h
        cases h
      rewrite [ha3] at h
      rewrite [hc3]
      have := ih xt b h
      have := (FOUR (xt.length + b.length) xt b (Nat.le_refl _) x).2.1
      omega
    have MINi : ∀ s y, (∀ a b, apply s a = some b → D a b ≤ cost s) →
        ∀ a b, apply (Sum.inr (some y) :: s) a = some b → D a b ≤ cost (Sum.inr (some y) :: s) := by
      intro s y ih a b h
      rewrite [ha4] at h
      rewrite [hc4]
      rcases hs : apply s a with _ | b'
      · rewrite [hs] at h
        cases h
      rewrite [hs] at h
      injection h with h
      subst h
      dsimp only
      have := ih a b' hs
      have := (FOUR (a.length + b'.length) a b' (Nat.le_refl _) y).1
      omega
    have MIN : ∀ s a b, apply s a = some b → D a b ≤ cost s := by
      intro s
      induction s with
      | nil =>
        intro a b h
        rewrite [ha0] at h
        injection h with h
        subst h
        rewrite [Drefl]
        exact Nat.zero_le _
      | cons e s ih =>
        rcases e with o | o <;> rcases o with _ | y
        · exact MINc s ih
        · exact MINr s y ih
        · exact MINd s ih
        · exact MINi s y ih
    intro xs ys fuel hfuel
    refine ⟨CORR fuel xs ys hfuel, ?_⟩
    intro script hs
    rewrite [hD fuel xs ys hfuel]
    exact MIN script xs ys hs

#print axioms OA_target
#check OA_target