ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>l : List Γ<GOAL>(Turing.ListBlank.mk l).tail = Turing.ListBlank.mk l.tail
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>a : Γ<VAR>l : List Γ<GOAL>Turing.ListBlank.cons a (Turing.ListBlank.mk l) = Turing.ListBlank.mk (a :: l)
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>a : Γ<VAR>l : Turing.ListBlank Γ<GOAL>(Turing.ListBlank.cons a l).head = a
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>a : Γ<VAR>l : Turing.ListBlank Γ<GOAL>(Turing.ListBlank.cons a l).tail = l
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>l : Turing.ListBlank Γ<GOAL>Turing.ListBlank.cons l.head l.tail = l
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>l : Turing.ListBlank Γ<GOAL>∃ a l', l = Turing.ListBlank.cons a l'
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>l : List Γ<VAR>n : ℕ<GOAL>(Turing.ListBlank.mk l).nth n = l.getI n
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>l : Turing.ListBlank Γ<GOAL>l.nth 0 = l.head
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>l : Turing.ListBlank Γ<VAR>n : ℕ<GOAL>l.nth (n + 1) = l.tail.nth n
<VAR>Γ : Type u_1<VAR>i : Inhabited Γ<VAR>L₁ L₂ : Turing.ListBlank Γ<GOAL>(∀ (i_1 : ℕ), L₁.nth i_1 = L₂.nth i_1) → L₁ = L₂
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>f : Γ → Γ<VAR>n i : ℕ<VAR>L : Turing.ListBlank Γ<GOAL>(Turing.ListBlank.modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
<VAR>Γ : Type u<VAR>Γ' : Type v<VAR>Inhabited Γ<VAR>Inhabited Γ'<VAR>self : Turing.PointedMap Γ Γ'<GOAL>self.f default = default
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>Inhabited Γ<VAR>Inhabited Γ'<VAR>f : Γ → Γ'<VAR>pt : f default = default<GOAL>{ f := f, map_pt' := pt }.f = f
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>Inhabited Γ<VAR>Inhabited Γ'<VAR>f : Turing.PointedMap Γ Γ'<GOAL>f.f default = default
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>Inhabited Γ<VAR>Inhabited Γ'<VAR>f : Turing.PointedMap Γ Γ'<VAR>l : List Γ<GOAL>(List.map f.f l).headI = f.f l.headI
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>Inhabited Γ<VAR>Inhabited Γ'<VAR>f : Turing.PointedMap Γ Γ'<VAR>l : List Γ<GOAL>Turing.ListBlank.map f (Turing.ListBlank.mk l) = Turing.ListBlank.mk (List.map f.f l)
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>Inhabited Γ<VAR>Inhabited Γ'<VAR>f : Turing.PointedMap Γ Γ'<VAR>l : Turing.ListBlank Γ<GOAL>(Turing.ListBlank.map f l).head = f.f l.head
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>Inhabited Γ<VAR>Inhabited Γ'<VAR>f : Turing.PointedMap Γ Γ'<VAR>l : Turing.ListBlank Γ<GOAL>(Turing.ListBlank.map f l).tail = Turing.ListBlank.map f l.tail
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>Inhabited Γ<VAR>Inhabited Γ'<VAR>f : Turing.PointedMap Γ Γ'<VAR>l : Turing.ListBlank Γ<VAR>a : Γ<GOAL>Turing.ListBlank.map f (Turing.ListBlank.cons a l) = Turing.ListBlank.cons (f.f a) (Turing.ListBlank.map f l)
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>Inhabited Γ<VAR>Inhabited Γ'<VAR>f : Turing.PointedMap Γ Γ'<VAR>l : Turing.ListBlank Γ<VAR>n : ℕ<GOAL>(Turing.ListBlank.map f l).nth n = f.f (l.nth n)
<VAR>ι : Type u_1<VAR>Γ : ι → Type u_2<VAR>(i : ι) → Inhabited (Γ i)<VAR>i : ι<VAR>L : Turing.ListBlank ((i : ι) → Γ i)<VAR>n : ℕ<GOAL>(Turing.ListBlank.map (Turing.proj i) L).nth n = L.nth n i
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>Inhabited Γ<VAR>Inhabited Γ'<VAR>F : Turing.PointedMap Γ Γ'<VAR>f : Γ → Γ<VAR>f' : Γ' → Γ'<VAR>H : ∀ (x : Γ), F.f (f x) = f' (F.f x)<VAR>n : ℕ<VAR>L : Turing.ListBlank Γ<GOAL>Turing.ListBlank.map F (Turing.ListBlank.modifyNth f n L) = Turing.ListBlank.modifyNth f' n (Turing.ListBlank.map F L)
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>l₁ l₂ : List Γ<GOAL>Turing.ListBlank.append l₁ (Turing.ListBlank.mk l₂) = Turing.ListBlank.mk (l₁ ++ l₂)
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>l₁ l₂ : List Γ<VAR>l₃ : Turing.ListBlank Γ<GOAL>Turing.ListBlank.append (l₁ ++ l₂) l₃ = Turing.ListBlank.append l₁ (Turing.ListBlank.append l₂ l₃)
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>Inhabited Γ<VAR>Inhabited Γ'<VAR>l : List Γ<VAR>f : Γ → List Γ'<VAR>hf : ∃ n, f default = List.replicate n default<GOAL>(Turing.ListBlank.mk l).bind f hf = Turing.ListBlank.mk (l.bind f)
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>Inhabited Γ<VAR>Inhabited Γ'<VAR>a : Γ<VAR>l : Turing.ListBlank Γ<VAR>f : Γ → List Γ'<VAR>hf : ∃ n, f default = List.replicate n default<GOAL>(Turing.ListBlank.cons a l).bind f hf = Turing.ListBlank.append (f a) (l.bind f hf)
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>T : Turing.Tape Γ<GOAL>Turing.Tape.move Turing.Dir.right (Turing.Tape.move Turing.Dir.left T) = T
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>T : Turing.Tape Γ<GOAL>Turing.Tape.move Turing.Dir.left (Turing.Tape.move Turing.Dir.right T) = T
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>L R : Turing.ListBlank Γ<GOAL>(Turing.Tape.mk' L R).left = L
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>L R : Turing.ListBlank Γ<GOAL>(Turing.Tape.mk' L R).head = R.head
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>L R : Turing.ListBlank Γ<GOAL>(Turing.Tape.mk' L R).right = R.tail
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>L R : Turing.ListBlank Γ<GOAL>(Turing.Tape.mk' L R).right₀ = R
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>T : Turing.Tape Γ<GOAL>Turing.Tape.mk' T.left T.right₀ = T
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>T : Turing.Tape Γ<GOAL>∃ L R, T = Turing.Tape.mk' L R
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>L R : Turing.ListBlank Γ<GOAL>Turing.Tape.move Turing.Dir.left (Turing.Tape.mk' L R) = Turing.Tape.mk' L.tail (Turing.ListBlank.cons L.head R)
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>L R : Turing.ListBlank Γ<GOAL>Turing.Tape.move Turing.Dir.right (Turing.Tape.mk' L R) = Turing.Tape.mk' (Turing.ListBlank.cons R.head L) R.tail
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>T : Turing.Tape Γ<GOAL>T.nth 0 = T.head
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>T : Turing.Tape Γ<VAR>n : ℕ<GOAL>T.right₀.nth n = T.nth ↑n
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>L R : Turing.ListBlank Γ<VAR>n : ℕ<GOAL>(Turing.Tape.mk' L R).nth ↑n = R.nth n
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>T : Turing.Tape Γ<VAR>i : ℤ<GOAL>(Turing.Tape.move Turing.Dir.left T).nth i = T.nth (i - 1)
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>T : Turing.Tape Γ<VAR>i : ℤ<GOAL>(Turing.Tape.move Turing.Dir.right T).nth i = T.nth (i + 1)
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>T : Turing.Tape Γ<VAR>i : ℕ<GOAL>((Turing.Tape.move Turing.Dir.right)^[i] T).head = T.nth ↑i
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>T : Turing.Tape Γ<GOAL>Turing.Tape.write T.head T = T
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>b : Γ<VAR>T : Turing.Tape Γ<VAR>i : ℤ<GOAL>(Turing.Tape.write b T).nth i = if i = 0 then b else T.nth i
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>a b : Γ<VAR>L R : Turing.ListBlank Γ<GOAL>Turing.Tape.write b (Turing.Tape.mk' L (Turing.ListBlank.cons a R)) = Turing.Tape.mk' L (Turing.ListBlank.cons b R)
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>Inhabited Γ<VAR>Inhabited Γ'<VAR>f : Turing.PointedMap Γ Γ'<VAR>T : Turing.Tape Γ<GOAL>(Turing.Tape.map f T).head = f.f T.head
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>Inhabited Γ<VAR>Inhabited Γ'<VAR>f : Turing.PointedMap Γ Γ'<VAR>b : Γ<VAR>T : Turing.Tape Γ<GOAL>Turing.Tape.map f (Turing.Tape.write b T) = Turing.Tape.write (f.f b) (Turing.Tape.map f T)
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>f : Γ → Γ<VAR>L R : Turing.ListBlank Γ<VAR>n : ℕ<GOAL>Turing.Tape.write (f (R.nth n)) ((Turing.Tape.move Turing.Dir.right)^[n] (Turing.Tape.mk' L R)) = (Turing.Tape.move Turing.Dir.right)^[n] (Turing.Tape.mk' L (Turing.ListBlank.modifyNth f n R))
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>Inhabited Γ<VAR>Inhabited Γ'<VAR>f : Turing.PointedMap Γ Γ'<VAR>T : Turing.Tape Γ<VAR>d : Turing.Dir<GOAL>Turing.Tape.map f (Turing.Tape.move d T) = Turing.Tape.move d (Turing.Tape.map f T)
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>Inhabited Γ<VAR>Inhabited Γ'<VAR>f : Turing.PointedMap Γ Γ'<VAR>L R : Turing.ListBlank Γ<GOAL>Turing.Tape.map f (Turing.Tape.mk' L R) = Turing.Tape.mk' (Turing.ListBlank.map f L) (Turing.ListBlank.map f R)
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>Inhabited Γ<VAR>Inhabited Γ'<VAR>f : Turing.PointedMap Γ Γ'<VAR>L R : List Γ<GOAL>Turing.Tape.map f (Turing.Tape.mk₂ L R) = Turing.Tape.mk₂ (List.map f.f L) (List.map f.f R)
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>Inhabited Γ<VAR>Inhabited Γ'<VAR>f : Turing.PointedMap Γ Γ'<VAR>l : List Γ<GOAL>Turing.Tape.map f (Turing.Tape.mk₁ l) = Turing.Tape.mk₁ (List.map f.f l)
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b c : σ<VAR>h : f a = f b<GOAL>Turing.Reaches₁ f a c ↔ Turing.Reaches₁ f b c
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b c : σ<VAR>hab : Turing.Reaches f a b<VAR>hac : Turing.Reaches f a c<GOAL>Turing.Reaches f b c ∨ Turing.Reaches f c b
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b c : σ<VAR>h₁ : Turing.Reaches₁ f a c<VAR>h₂ : b ∈ f a<GOAL>Turing.Reaches f b c
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b c : σ<VAR>h₁ : Turing.Reaches₀ f a b<VAR>h₂ : Turing.Reaches₀ f b c<GOAL>Turing.Reaches₀ f a c
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a : σ<GOAL>Turing.Reaches₀ f a a
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b : σ<VAR>h : b ∈ f a<GOAL>Turing.Reaches₀ f a b
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b c : σ<VAR>h : b ∈ f a<VAR>h₂ : Turing.Reaches₀ f b c<GOAL>Turing.Reaches₀ f a c
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b c : σ<VAR>h₁ : Turing.Reaches₀ f a b<VAR>h : c ∈ f b<GOAL>Turing.Reaches₀ f a c
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b : σ<VAR>e : f a = f b<GOAL>Turing.Reaches₀ f a b
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b : σ<VAR>h : Turing.Reaches₁ f a b<GOAL>Turing.Reaches₀ f a b
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b : σ<VAR>h : Turing.Reaches f a b<GOAL>Turing.Reaches₀ f a b
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b c : σ<VAR>h : Turing.Reaches₀ f a b<VAR>h₂ : c ∈ f b<GOAL>Turing.Reaches₁ f a c
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b : σ<GOAL>b ∈ Turing.eval f a ↔ Turing.Reaches f a b ∧ f b = none
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b : σ<VAR>h : b ∈ Turing.eval f a<VAR>c : σ<GOAL>¬Turing.Reaches₁ f b c
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b : σ<VAR>h : b ∈ Turing.eval f a<VAR>c : σ<GOAL>Turing.Reaches f b c ↔ c = b
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b : σ<VAR>ab : Turing.Reaches f a b<GOAL>Turing.eval f a = Turing.eval f b
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂ → Prop<VAR>H : Turing.Respects f₁ f₂ tr<VAR>a₁ : σ₁<VAR>a₂ : σ₂<VAR>aa : tr a₁ a₂<VAR>b₁ : σ₁<VAR>ab : Turing.Reaches₁ f₁ a₁ b₁<GOAL>∃ b₂, tr b₁ b₂ ∧ Turing.Reaches₁ f₂ a₂ b₂
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂ → Prop<VAR>H : Turing.Respects f₁ f₂ tr<VAR>a₁ : σ₁<VAR>a₂ : σ₂<VAR>aa : tr a₁ a₂<VAR>b₁ : σ₁<VAR>ab : Turing.Reaches f₁ a₁ b₁<GOAL>∃ b₂, tr b₁ b₂ ∧ Turing.Reaches f₂ a₂ b₂
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂ → Prop<VAR>H : Turing.Respects f₁ f₂ tr<VAR>a₁ : σ₁<VAR>a₂ : σ₂<VAR>aa : tr a₁ a₂<VAR>b₂ : σ₂<VAR>ab : Turing.Reaches f₂ a₂ b₂<GOAL>∃ c₁ c₂, Turing.Reaches f₂ b₂ c₂ ∧ tr c₁ c₂ ∧ Turing.Reaches f₁ a₁ c₁
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂ → Prop<VAR>H : Turing.Respects f₁ f₂ tr<VAR>a₁ b₁ : σ₁<VAR>a₂ : σ₂<VAR>aa : tr a₁ a₂<VAR>ab : b₁ ∈ Turing.eval f₁ a₁<GOAL>∃ b₂, tr b₁ b₂ ∧ b₂ ∈ Turing.eval f₂ a₂
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂ → Prop<VAR>H : Turing.Respects f₁ f₂ tr<VAR>a₁ : σ₁<VAR>b₂ a₂ : σ₂<VAR>aa : tr a₁ a₂<VAR>ab : b₂ ∈ Turing.eval f₂ a₂<GOAL>∃ b₁, tr b₁ b₂ ∧ b₁ ∈ Turing.eval f₁ a₁
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂ → Prop<VAR>H : Turing.Respects f₁ f₂ tr<VAR>a₁ : σ₁<VAR>a₂ : σ₂<VAR>aa : tr a₁ a₂<GOAL>(Turing.eval f₂ a₂).Dom ↔ (Turing.eval f₁ a₁).Dom
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂<VAR>a₂ b₂ : σ₂<VAR>h : f₂ a₂ = f₂ b₂<VAR>b₁ : Option σ₁<GOAL>Turing.FRespects f₂ tr a₂ b₁ ↔ Turing.FRespects f₂ tr b₂ b₁
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂<GOAL>(Turing.Respects f₁ f₂ fun a b => tr a = b) ↔ ∀ ⦃a₁ : σ₁⦄, Turing.FRespects f₂ tr (tr a₁) (f₁ a₁)
<VAR>σ₁ σ₂ : Type u_1<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂<VAR>H : Turing.Respects f₁ f₂ fun a b => tr a = b<VAR>a₁ : σ₁<GOAL>Turing.eval f₂ (tr a₁) = tr <$> Turing.eval f₁ a₁
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>Λ : Type u_2<VAR>Inhabited Λ<VAR>M : Turing.TM0.Machine Γ Λ<VAR>S : Set Λ<VAR>ss : Turing.TM0.Supports M S<VAR>c c' : Turing.TM0.Cfg Γ Λ<GOAL>c' ∈ Turing.TM0.step M c → c.q ∈ S → c'.q ∈ S
<VAR>Γ : Type u_1<VAR>Λ : Type u_2<VAR>Inhabited Λ<VAR>M : Turing.TM0.Machine Γ Λ<GOAL>Turing.TM0.Supports M Set.univ
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>Γ' : Type u_2<VAR>Inhabited Γ'<VAR>Λ : Type u_3<VAR>Inhabited Λ<VAR>Λ' : Type u_4<VAR>Inhabited Λ'<VAR>M : Turing.TM0.Machine Γ Λ<VAR>f₁ : Turing.PointedMap Γ Γ'<VAR>f₂ : Turing.PointedMap Γ' Γ<VAR>g₁ : Λ → Λ'<VAR>g₂ : Λ' → Λ<VAR>S : Set Λ<VAR>f₂₁ : Function.RightInverse f₁.f f₂.f<VAR>g₂₁ : ∀ q ∈ S, g₂ (g₁ q) = q<VAR>c : Turing.TM0.Cfg Γ Λ<GOAL>c.q ∈ S → Option.map (Turing.TM0.Cfg.map f₁ g₁) (Turing.TM0.step M c) = Turing.TM0.step (M.map f₁ f₂ g₁ g₂) (Turing.TM0.Cfg.map f₁ g₁ c)
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>Γ' : Type u_2<VAR>Inhabited Γ'<VAR>Λ : Type u_3<VAR>Inhabited Λ<VAR>Λ' : Type u_4<VAR>Inhabited Λ'<VAR>f₁ : Turing.PointedMap Γ Γ'<VAR>g₁ : Turing.PointedMap Λ Λ'<VAR>l : List Γ<GOAL>Turing.TM0.Cfg.map f₁ g₁.f (Turing.TM0.init l) = Turing.TM0.init (List.map f₁.f l)
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>Γ' : Type u_2<VAR>Inhabited Γ'<VAR>Λ : Type u_3<VAR>Inhabited Λ<VAR>Λ' : Type u_4<VAR>Inhabited Λ'<VAR>M : Turing.TM0.Machine Γ Λ<VAR>f₁ : Turing.PointedMap Γ Γ'<VAR>f₂ : Turing.PointedMap Γ' Γ<VAR>g₁ : Turing.PointedMap Λ Λ'<VAR>g₂ : Λ' → Λ<VAR>S : Set Λ<VAR>ss : Turing.TM0.Supports M S<VAR>f₂₁ : Function.RightInverse f₁.f f₂.f<VAR>g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q<GOAL>Turing.Respects (Turing.TM0.step M) (Turing.TM0.step (M.map f₁ f₂ g₁.f g₂)) fun a b => a.q ∈ S ∧ Turing.TM0.Cfg.map f₁ g₁.f a = b
<VAR>Γ : Type u_1<VAR>Λ : Type u_2<VAR>σ : Type u_3<VAR>q : Turing.TM1.Stmt Γ Λ σ<GOAL>q ∈ Turing.TM1.stmts₁ q
<VAR>Γ : Type u_1<VAR>Λ : Type u_2<VAR>σ : Type u_3<VAR>q₁ q₂ : Turing.TM1.Stmt Γ Λ σ<GOAL>q₁ ∈ Turing.TM1.stmts₁ q₂ → Turing.TM1.stmts₁ q₁ ⊆ Turing.TM1.stmts₁ q₂
<VAR>Γ : Type u_1<VAR>Λ : Type u_2<VAR>σ : Type u_3<VAR>S : Finset Λ<VAR>q₁ q₂ : Turing.TM1.Stmt Γ Λ σ<VAR>h : q₁ ∈ Turing.TM1.stmts₁ q₂<VAR>hs : Turing.TM1.SupportsStmt S q₂<GOAL>Turing.TM1.SupportsStmt S q₁
<VAR>Γ : Type u_1<VAR>Λ : Type u_2<VAR>σ : Type u_3<VAR>M : Λ → Turing.TM1.Stmt Γ Λ σ<VAR>S : Finset Λ<VAR>q₁ q₂ : Turing.TM1.Stmt Γ Λ σ<VAR>h₁ : q₁ ∈ Turing.TM1.stmts₁ q₂<GOAL>some q₂ ∈ Turing.TM1.stmts M S → some q₁ ∈ Turing.TM1.stmts M S
<VAR>Γ : Type u_1<VAR>Λ : Type u_2<VAR>σ : Type u_3<VAR>Inhabited Λ<VAR>M : Λ → Turing.TM1.Stmt Γ Λ σ<VAR>S : Finset Λ<VAR>q : Turing.TM1.Stmt Γ Λ σ<VAR>ss : Turing.TM1.Supports M S<GOAL>some q ∈ Turing.TM1.stmts M S → Turing.TM1.SupportsStmt S q
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>Λ : Type u_2<VAR>σ : Type u_3<VAR>Inhabited Λ<VAR>M : Λ → Turing.TM1.Stmt Γ Λ σ<VAR>S : Finset Λ<VAR>ss : Turing.TM1.Supports M S<VAR>c c' : Turing.TM1.Cfg Γ Λ σ<GOAL>c' ∈ Turing.TM1.step M c → c.l ∈ Finset.insertNone S → c'.l ∈ Finset.insertNone S
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>Λ : Type u_2<VAR>Inhabited Λ<VAR>σ : Type u_3<VAR>Inhabited σ<VAR>M : Λ → Turing.TM1.Stmt Γ Λ σ<GOAL>Turing.Respects (Turing.TM1.step M) (Turing.TM0.step (Turing.TM1to0.tr M)) fun c₁ c₂ => Turing.TM1to0.trCfg M c₁ = c₂
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>Λ : Type u_2<VAR>Inhabited Λ<VAR>σ : Type u_3<VAR>Inhabited σ<VAR>M : Λ → Turing.TM1.Stmt Γ Λ σ<VAR>l : List Γ<GOAL>Turing.TM0.eval (Turing.TM1to0.tr M) l = Turing.TM1.eval M l
<VAR>Γ : Type u_1<VAR>Λ : Type u_2<VAR>Inhabited Λ<VAR>σ : Type u_3<VAR>Inhabited σ<VAR>M : Λ → Turing.TM1.Stmt Γ Λ σ<VAR>Fintype σ<VAR>S : Finset Λ<VAR>ss : Turing.TM1.Supports M S<GOAL>Turing.TM0.Supports (Turing.TM1to0.tr M) ↑(Turing.TM1to0.trStmts M S)
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>Finite Γ<GOAL>∃ n enc dec, enc default = Mathlib.Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a
<VAR>Γ : Type u_1<VAR>Λ : Type u_2<VAR>σ : Type u_3<VAR>n : ℕ<VAR>d : Turing.Dir<VAR>q : Turing.TM1.Stmt Bool Turing.TM1to1.Λ' σ<VAR>v : σ<VAR>T : Turing.Tape Bool<GOAL>Turing.TM1.stepAux (Turing.TM1to1.move d q) v T = Turing.TM1.stepAux q v ((Turing.Tape.move d)^[n] T)
<VAR>Γ : Type u_1<VAR>Λ : Type u_2<VAR>σ : Type u_3<VAR>n : ℕ<VAR>S : Finset Turing.TM1to1.Λ'<VAR>d : Turing.Dir<VAR>q : Turing.TM1.Stmt Bool Turing.TM1to1.Λ' σ<GOAL>Turing.TM1.SupportsStmt S (Turing.TM1to1.move d q) = Turing.TM1.SupportsStmt S q
<VAR>Γ : Type u_1<VAR>Λ : Type u_2<VAR>σ : Type u_3<VAR>S : Finset Turing.TM1to1.Λ'<VAR>l : List Bool<VAR>q : Turing.TM1.Stmt Bool Turing.TM1to1.Λ' σ<GOAL>Turing.TM1.SupportsStmt S (Turing.TM1to1.write l q) = Turing.TM1.SupportsStmt S q
<VAR>Γ : Type u_1<VAR>Λ : Type u_2<VAR>σ : Type u_3<VAR>n : ℕ<VAR>dec : Mathlib.Vector Bool n → Γ<VAR>S : Finset Turing.TM1to1.Λ'<VAR>f : Γ → Turing.TM1.Stmt Bool Turing.TM1to1.Λ' σ<GOAL>(∀ (a : Γ), Turing.TM1.SupportsStmt S (f a)) → Turing.TM1.SupportsStmt S (Turing.TM1to1.read dec f)
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>n : ℕ<VAR>enc : Γ → Mathlib.Vector Bool n<VAR>enc0 : enc default = Mathlib.Vector.replicate n false<VAR>L R : Turing.ListBlank Γ<GOAL>Turing.TM1to1.trTape enc0 (Turing.Tape.mk' L R) = Turing.TM1to1.trTape' enc0 L R
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>n : ℕ<VAR>enc : Γ → Mathlib.Vector Bool n<VAR>enc0 : enc default = Mathlib.Vector.replicate n false<VAR>L R : Turing.ListBlank Γ<GOAL>(Turing.Tape.move Turing.Dir.left)^[n] (Turing.TM1to1.trTape' enc0 L R) = Turing.TM1to1.trTape' enc0 L.tail (Turing.ListBlank.cons L.head R)
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>n : ℕ<VAR>enc : Γ → Mathlib.Vector Bool n<VAR>enc0 : enc default = Mathlib.Vector.replicate n false<VAR>L R : Turing.ListBlank Γ<GOAL>(Turing.Tape.move Turing.Dir.right)^[n] (Turing.TM1to1.trTape' enc0 L R) = Turing.TM1to1.trTape' enc0 (Turing.ListBlank.cons R.head L) R.tail
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>Λ : Type u_2<VAR>σ : Type u_3<VAR>n : ℕ<VAR>enc : Γ → Mathlib.Vector Bool n<VAR>enc0 : enc default = Mathlib.Vector.replicate n false<VAR>q : Turing.TM1.Stmt Bool Turing.TM1to1.Λ' σ<VAR>v : σ<VAR>a b : Γ<VAR>L R : Turing.ListBlank Γ<GOAL>Turing.TM1.stepAux (Turing.TM1to1.write (enc a).toList q) v (Turing.TM1to1.trTape' enc0 L (Turing.ListBlank.cons b R)) = Turing.TM1.stepAux q v (Turing.TM1to1.trTape' enc0 (Turing.ListBlank.cons a L) R)
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>Λ : Type u_2<VAR>σ : Type u_3<VAR>n : ℕ<VAR>enc : Γ → Mathlib.Vector Bool n<VAR>dec : Mathlib.Vector Bool n → Γ<VAR>enc0 : enc default = Mathlib.Vector.replicate n false<VAR>encdec : ∀ (a : Γ), dec (enc a) = a<VAR>f : Γ → Turing.TM1.Stmt Bool Turing.TM1to1.Λ' σ<VAR>v : σ<VAR>L R : Turing.ListBlank Γ<GOAL>Turing.TM1.stepAux (Turing.TM1to1.read dec f) v (Turing.TM1to1.trTape' enc0 L R) = Turing.TM1.stepAux (f R.head) v (Turing.TM1to1.trTape' enc0 L R)
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>Λ : Type u_2<VAR>σ : Type u_3<VAR>n : ℕ<VAR>enc : Γ → Mathlib.Vector Bool n<VAR>dec : Mathlib.Vector Bool n → Γ<VAR>enc0 : enc default = Mathlib.Vector.replicate n false<VAR>M : Λ → Turing.TM1.Stmt Γ Λ σ<VAR>encdec : ∀ (a : Γ), dec (enc a) = a<VAR>enc₀ : enc default = Mathlib.Vector.replicate n false<GOAL>Turing.Respects (Turing.TM1.step M) (Turing.TM1.step (Turing.TM1to1.tr enc dec M)) fun c₁ c₂ => Turing.TM1to1.trCfg enc enc₀ c₁ = c₂
<VAR>Γ : Type u_1<VAR>Λ : Type u_2<VAR>Inhabited Λ<VAR>σ : Type u_3<VAR>n : ℕ<VAR>enc : Γ → Mathlib.Vector Bool n<VAR>dec : Mathlib.Vector Bool n → Γ<VAR>M : Λ → Turing.TM1.Stmt Γ Λ σ<VAR>Fintype Γ<VAR>S : Finset Λ<VAR>ss : Turing.TM1.Supports M S<GOAL>Turing.TM1.Supports (Turing.TM1to1.tr enc dec M) (Turing.TM1to1.trSupp M S)
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>Λ : Type u_2<VAR>Inhabited Λ<VAR>M : Turing.TM0.Machine Γ Λ<GOAL>Turing.Respects (Turing.TM0.step M) (Turing.TM1.step (Turing.TM0to1.tr M)) fun a b => Turing.TM0to1.trCfg M a = b
<VAR>K : Type u_1<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>q : Turing.TM2.Stmt Γ Λ σ<GOAL>q ∈ Turing.TM2.stmts₁ q
<VAR>K : Type u_1<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>q₁ q₂ : Turing.TM2.Stmt Γ Λ σ<GOAL>q₁ ∈ Turing.TM2.stmts₁ q₂ → Turing.TM2.stmts₁ q₁ ⊆ Turing.TM2.stmts₁ q₂
<VAR>K : Type u_1<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>S : Finset Λ<VAR>q₁ q₂ : Turing.TM2.Stmt Γ Λ σ<VAR>h : q₁ ∈ Turing.TM2.stmts₁ q₂<VAR>hs : Turing.TM2.SupportsStmt S q₂<GOAL>Turing.TM2.SupportsStmt S q₁
<VAR>K : Type u_1<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>M : Λ → Turing.TM2.Stmt Γ Λ σ<VAR>S : Finset Λ<VAR>q₁ q₂ : Turing.TM2.Stmt Γ Λ σ<VAR>h₁ : q₁ ∈ Turing.TM2.stmts₁ q₂<GOAL>some q₂ ∈ Turing.TM2.stmts M S → some q₁ ∈ Turing.TM2.stmts M S
<VAR>K : Type u_1<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>Inhabited Λ<VAR>M : Λ → Turing.TM2.Stmt Γ Λ σ<VAR>S : Finset Λ<VAR>q : Turing.TM2.Stmt Γ Λ σ<VAR>ss : Turing.TM2.Supports M S<GOAL>some q ∈ Turing.TM2.stmts M S → Turing.TM2.SupportsStmt S q
<VAR>K : Type u_1<VAR>DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>Inhabited Λ<VAR>M : Λ → Turing.TM2.Stmt Γ Λ σ<VAR>S : Finset Λ<VAR>ss : Turing.TM2.Supports M S<VAR>c c' : Turing.TM2.Cfg Γ Λ σ<GOAL>c' ∈ Turing.TM2.step M c → c.l ∈ Finset.insertNone S → c'.l ∈ Finset.insertNone S
<VAR>K : Type u_1<VAR>Γ : K → Type u_2<VAR>L : Turing.ListBlank ((k : K) → Option (Γ k))<VAR>k : K<VAR>S : List (Γ k)<VAR>n : ℕ<VAR>hL : Turing.ListBlank.map (Turing.proj k) L = Turing.ListBlank.mk (List.map some S).reverse<GOAL>L.nth n k = S.reverse.get? n
<VAR>K : Type u_1<VAR>Γ : K → Type u_2<VAR>L : Turing.ListBlank ((k : K) → Option (Γ k))<GOAL>Turing.ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (Turing.TM2to1.addBottom L) = L
<VAR>K : Type u_1<VAR>Γ : K → Type u_2<VAR>f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)<VAR>L : Turing.ListBlank ((k : K) → Option (Γ k))<VAR>n : ℕ<GOAL>Turing.ListBlank.modifyNth (fun a => (a.1, f a.2)) n (Turing.TM2to1.addBottom L) = Turing.TM2to1.addBottom (Turing.ListBlank.modifyNth f n L)
<VAR>K : Type u_1<VAR>Γ : K → Type u_2<VAR>L : Turing.ListBlank ((k : K) → Option (Γ k))<VAR>n : ℕ<GOAL>((Turing.TM2to1.addBottom L).nth n).2 = L.nth n
<VAR>K : Type u_1<VAR>Γ : K → Type u_2<VAR>L : Turing.ListBlank ((k : K) → Option (Γ k))<VAR>n : ℕ<GOAL>((Turing.TM2to1.addBottom L).nth (n + 1)).1 = false
<VAR>K : Type u_1<VAR>Γ : K → Type u_2<VAR>L : Turing.ListBlank ((k : K) → Option (Γ k))<GOAL>(Turing.TM2to1.addBottom L).head.1 = true
<VAR>K : Type u_1<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>S : Finset Λ<VAR>k : K<VAR>s : Turing.TM2to1.StAct k<VAR>q : Turing.TM2.Stmt Γ Λ σ<GOAL>Turing.TM2.SupportsStmt S (Turing.TM2to1.stRun s q) ↔ Turing.TM2.SupportsStmt S q
<VAR>K : Type u_1<VAR>DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>k : K<VAR>q : Turing.TM2.Stmt Γ Λ σ<VAR>v : σ<VAR>S : (k : K) → List (Γ k)<VAR>s : Turing.TM2to1.StAct k<GOAL>Turing.TM2.stepAux (Turing.TM2to1.stRun s q) v S = Turing.TM2.stepAux q (Turing.TM2to1.stVar v (S k) s) (Function.update S k (Turing.TM2to1.stWrite v (S k) s))
<VAR>K : Type u_1<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>k : K<VAR>s : Turing.TM2to1.StAct k<VAR>q : Turing.TM2.Stmt Γ Λ σ<GOAL>Turing.TM2to1.trNormal (Turing.TM2to1.stRun s q) = Turing.TM1.Stmt.goto fun x x => Turing.TM2to1.Λ'.go k s q
<VAR>K : Type u_1<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>k : K<VAR>s : Turing.TM2to1.StAct k<VAR>q : Turing.TM2.Stmt Γ Λ σ<GOAL>Turing.TM2to1.trStmts₁ (Turing.TM2to1.stRun s q) = {Turing.TM2to1.Λ'.go k s q, Turing.TM2to1.Λ'.ret q} ∪ Turing.TM2to1.trStmts₁ q
<VAR>K : Type u_1<VAR>DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>k : K<VAR>q : Turing.TM1.Stmt Turing.TM2to1.Γ' Turing.TM2to1.Λ' σ<VAR>v : σ<VAR>S : (k : K) → List (Γ k)<VAR>L : Turing.ListBlank ((k : K) → Option (Γ k))<VAR>hL : ∀ (k : K), Turing.ListBlank.map (Turing.proj k) L = Turing.ListBlank.mk (List.map some (S k)).reverse<VAR>o : Turing.TM2to1.StAct k<GOAL>let v' := Turing.TM2to1.stVar v (S k) o;
let Sk' := Turing.TM2to1.stWrite v (S k) o;