awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
cons :
  TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
      (tr
        ((fun (x : Option Γ') ↦
            Λ'.read fun (s : Option Γ') ↦
              (if s = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) stack) (unrev q))
          (some Γ'.cons)))
      (some Γ'.cons)
      (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
        (update (β := fun (k : K') ↦ List Γ')
          (update (β := fun (a : K') ↦ List Γ') (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃)) stack
            (trList L₂ ++ Γ'.consₗ :: L₃))
          rev ((trNat a).reverseAux (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃) rev)))
        rev
        ((fun (s : Option Γ') ↦ (Option.getD ((fun (x : Option Γ') ↦ some Γ'.cons) s) default : Γ')) (some Γ'.cons) ::
          update (β := fun (k : K') ↦ List Γ')
            (update (β := fun (a : K') ↦ List Γ') (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃)) stack
              (trList L₂ ++ Γ'.consₗ :: L₃))
            rev ((trNat a).reverseAux (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃) rev)) rev)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList ((a :: L₂).headI :: L₁)) [] [] L₃))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (head stack q)) s
      (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList ((a :: L₂).headI :: L₁)) [] [] L₃))

Tactic:
refine
      TransGen.trans
        (move_ok (by decide)
          (splitAtPred_eq _ _ (trNat a) (some Γ'.cons) (trList L₂ ++ Γ'.consₗ :: L₃)
            (trNat_natEnd _) ⟨rfl, by simp⟩))
        (TransGen.head rfl (TransGen.head rfl ?_))

Premises used: Turing.PartrecToTM2.Γ'.consₗ, Relation.TransGen.head, Turing.PartrecToTM2.trList, Turing.PartrecToTM2.move_ok, Turing.PartrecToTM2.Γ'.cons, Option.some, List.cons, Turing.PartrecToTM2.splitAtPred_eq, Relation.TransGen.trans, And.intro, Turing.PartrecToTM2.trNat, HAppend.hAppend, rfl, Turing.PartrecToTM2.trNat_natEnd
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
cons :
  TransGen
    (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
      (match (motive :=
          TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ') → Option (TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))) a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
      (tr
        (Λ'.read fun (s : Option Γ') ↦
          (if s = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) stack) (unrev q)))
      (some Γ'.cons)
      (elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNat a ++ Γ'.cons :: trList L₁) [] [] L₃))
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
      (tr
        ((fun (x : Option Γ') ↦
            Λ'.read fun (s : Option Γ') ↦
              (if s = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) stack) (unrev q))
          (some Γ'.cons)))
      (some Γ'.cons)
      (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
        (update (β := fun (k : K') ↦ List Γ')
          (update (β := fun (a : K') ↦ List Γ') (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃)) stack
            (trList L₂ ++ Γ'.consₗ :: L₃))
          rev ((trNat a).reverseAux (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃) rev)))
        rev
        ((fun (s : Option Γ') ↦ (Option.getD ((fun (x : Option Γ') ↦ some Γ'.cons) s) default : Γ')) (some Γ'.cons) ::
          update (β := fun (k : K') ↦ List Γ')
            (update (β := fun (a : K') ↦ List Γ') (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃)) stack
              (trList L₂ ++ Γ'.consₗ :: L₃))
            rev ((trNat a).reverseAux (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃) rev)) rev)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList ((a :: L₂).headI :: L₁)) [] [] L₃))

Tactic:
simp only [TM2.step, Option.mem_def, trList, List.append_assoc,
      List.cons_append, elim_update_stack, elim_rev, elim_update_rev, Function.update_self,
      List.headI_cons]

Premises used: List.append_assoc, Turing.PartrecToTM2.trList, Turing.PartrecToTM2.K'.elim_rev, Turing.TM2.step, List.headI_cons, Turing.PartrecToTM2.K'.elim_update_stack, Function.update_self, List.cons_append, Turing.PartrecToTM2.K'.elim_update_rev, Option.mem_def
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃) stack =
    trList L₂ ++ Γ'.consₗ :: L₃

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
cons :
  TransGen
    (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
      (match (motive :=
          TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ') → Option (TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))) a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) (some Γ'.consₗ)
      (update (β := fun (k : K') ↦ List Γ')
        (elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃))
        stack L₃))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNat a ++ Γ'.cons :: trList L₁) [] [] L₃))
⊢ TransGen
    (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
      (match (motive :=
          TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ') → Option (TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))) a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
      (tr
        (Λ'.read fun (s : Option Γ') ↦
          (if s = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) stack) (unrev q)))
      (some Γ'.cons)
      (elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNat a ++ Γ'.cons :: trList L₁) [] [] L₃))

Tactic:
refine
      TransGen.trans
        (clear_ok
          (splitAtPred_eq _ _ (trList L₂) (some Γ'.consₗ) L₃
            (fun x h => Bool.decide_false (trList_ne_consₗ _ _ h)) ⟨rfl, by simp⟩))
        ?_

Premises used: Turing.PartrecToTM2.Γ'.consₗ, Turing.PartrecToTM2.trList, Option.some, Turing.PartrecToTM2.splitAtPred_eq, Relation.TransGen.trans, And.intro, Turing.PartrecToTM2.clear_ok, Turing.PartrecToTM2.trList_ne_consₗ, rfl, Bool.decide_false
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) (some Γ'.consₗ)
      (update (β := fun (k : K') ↦ List Γ')
        (elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃))
        stack L₃))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ')
          (update (β := fun (k : K') ↦ List Γ')
            (elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃))
            stack L₃)
          rev [])
        main
        ((update (β := fun (k : K') ↦ List Γ')
              (elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) []
                (trList L₂ ++ Γ'.consₗ :: L₃))
              stack L₃ rev).reverseAux
          (update (β := fun (k : K') ↦ List Γ')
            (elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃))
            stack L₃ main))))

Tactic:
unrev_ok

Premises used: Turing.PartrecToTM2.unrev_ok
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
h :
  elim (trNat a ++ Γ'.cons :: trList L₁) [] [] L₃ =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ')
        (update (β := fun (k : K') ↦ List Γ')
          (elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃))
          stack L₃)
        rev [])
      main
      ((update (β := fun (k : K') ↦ List Γ')
            (elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃))
            stack L₃ rev).reverseAux
        (update (β := fun (k : K') ↦ List Γ')
          (elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃))
          stack L₃ main))
⊢ TransGen
    (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
      (match (motive :=
          TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ') → Option (TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))) a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) (some Γ'.consₗ)
      (update (β := fun (k : K') ↦ List Γ')
        (elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃))
        stack L₃))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNat a ++ Γ'.cons :: trList L₁) [] [] L₃))

Tactic:
convert! unrev_ok using 2

Premises used: Turing.PartrecToTM2.unrev_ok
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ elim (trNat a ++ Γ'.cons :: trList L₁) [] [] L₃ =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ')
        (update (β := fun (k : K') ↦ List Γ')
          (elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃))
          stack L₃)
        rev [])
      main
      ((update (β := fun (k : K') ↦ List Γ')
            (elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃))
            stack L₃ rev).reverseAux
        (update (β := fun (k : K') ↦ List Γ')
          (elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃))
          stack L₃ main))

Tactic:
simp [List.reverseAux_eq]

Premises used: List.reverseAux_eq
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
simp :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trNum (↑n : Num) ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNum (Num.succ (↑n : Num)) ++ [Γ'.cons]) [] c d))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trList [n]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList [n.succ]) [] c d))

Tactic:
simp only [trList, trNat.eq_1, Nat.cast_succ, Num.add_one]

Premises used: Nat.cast_succ, Turing.PartrecToTM2.trNat.eq_1, Turing.PartrecToTM2.trList, Num.add_one
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
zero :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d))
pos :
  ∀ (a : PosNum),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trNum (Num.pos a) ++ [Γ'.cons]) [] c d))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNum (Num.pos a).succ ++ [Γ'.cons]) [] c d))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trNum (↑n : Num) ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNum (Num.succ (↑n : Num)) ++ [Γ'.cons]) [] c d))

Tactic:
rcases (n : Num) with - | a

Premises used: Nat.cast
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d))

Tactic:
TransGen.head rfl ?_

Premises used: Relation.TransGen.head, StateTransition.Reaches₁, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
zero :
  TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr q.succ) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d))

Tactic:
refine TransGen.head rfl ?_

Premises used: Relation.TransGen.head, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
⊢ Eq (α := TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none
      (elim (Γ'.bit1 :: Γ'.cons :: (trNum Num.zero ++ [Γ'.cons]).tail) [] c d))

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
a : PosNum
this :
  ∀ (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum a.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
obtain :
  ∀ (l₁' l₂' : List Γ') (s' : Option Γ') (e : List.reverseAux [] (trPosNum a.succ) = l₁'.reverseAux l₂')
    (h :
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) [] c d))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) [] c d))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trPosNum a.succ ++ [Γ'.cons]) [] c d))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trPosNum a.succ ++ [Γ'.cons]) [] c d))

Tactic:
obtain ⟨l₁', l₂', s', e, h⟩ := this []

Premises used: List.nil
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
a : PosNum
this :
  ∀ (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum a.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
l₁' l₂' : List Γ'
s' : Option Γ'
e : trPosNum a.succ = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trPosNum a.succ ++ [Γ'.cons]) [] c d))

Tactic:
h.trans ?_

Premises used: Relation.TransGen.trans, StateTransition.Reaches₁
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
a : PosNum
this :
  ∀ (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum a.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
l₁' l₂' : List Γ'
s' : Option Γ'
e : trPosNum a.succ = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
refine :
  TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trPosNum a.succ ++ [Γ'.cons]) [] c d))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trPosNum a.succ ++ [Γ'.cons]) [] c d))

Tactic:
refine h.trans ?_

Premises used: Relation.TransGen.trans
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
a : PosNum
this :
  ∀ (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum a.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
l₁' l₂' : List Γ'
s' : Option Γ'
e : trPosNum a.succ = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ') (elim (l₂' ++ [Γ'.cons]) l₁' c d) rev []) main
        ((elim (l₂' ++ [Γ'.cons]) l₁' c d rev).reverseAux (elim (l₂' ++ [Γ'.cons]) l₁' c d main))))

Tactic:
unrev_ok

Premises used: Turing.PartrecToTM2.unrev_ok
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
a : PosNum
this :
  ∀ (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum a.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
l₁' l₂' : List Γ'
s' : Option Γ'
e : trPosNum a.succ = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
h₁ :
  elim (trPosNum a.succ ++ [Γ'.cons]) [] c d =
    update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') (elim (l₂' ++ [Γ'.cons]) l₁' c d) rev [])
      main ((elim (l₂' ++ [Γ'.cons]) l₁' c d rev).reverseAux (elim (l₂' ++ [Γ'.cons]) l₁' c d main))
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trPosNum a.succ ++ [Γ'.cons]) [] c d))

Tactic:
convert! unrev_ok using 2

Premises used: Turing.PartrecToTM2.unrev_ok
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
a : PosNum
this :
  ∀ (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum a.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
l₁' l₂' : List Γ'
s' : Option Γ'
e : trPosNum a.succ = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
⊢ elim (trPosNum a.succ ++ [Γ'.cons]) [] c d =
    update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') (elim (l₂' ++ [Γ'.cons]) l₁' c d) rev [])
      main ((elim (l₂' ++ [Γ'.cons]) l₁' c d rev).reverseAux (elim (l₂' ++ [Γ'.cons]) l₁' c d main))

Tactic:
simp [e, List.reverseAux_eq]

Premises used: List.reverseAux_eq
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
a : PosNum
pos :
  ∀ (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum a.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trPosNum a.succ ++ [Γ'.cons]) [] c d))

Tactic:
suffices ∀ l₁, ∃ l₁' l₂' s',
      List.reverseAux l₁ (trPosNum a.succ) = List.reverseAux l₁' l₂' ∧
        Reaches₁ (TM2.step tr) ⟨some q.succ, s, K'.elim (trPosNum a ++ [Γ'.cons]) l₁ c d⟩
          ⟨some (unrev q), s', K'.elim (l₂' ++ [Γ'.cons]) l₁' c d⟩ by
    obtain ⟨l₁', l₂', s', e, h⟩ := this []
    simp only [List.reverseAux] at e
    refine h.trans ?_
    convert! unrev_ok using 2
    simp [e, List.reverseAux_eq]