ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>F : Type u_4<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>NormedAddCommGroup F<VAR>ρ : MeasureTheory.Measure (α × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>f : α × Ω → F<VAR>hf : MeasureTheory.AEStronglyMeasurable f ρ<GOAL>(∀ᵐ (a : α) ∂ρ.fst, MeasureTheory.Integrable (fun ω => f (a, ω)) (ρ.condKernel a)) ∧ MeasureTheory.Integrable (fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst ↔ MeasureTheory.Integrable f ρ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>F : Type u_4<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>NormedAddCommGroup F<VAR>ρ : MeasureTheory.Measure (α × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>f : α × Ω → F<VAR>hf_int : MeasureTheory.Integrable f ρ<GOAL>∀ᵐ (a : α) ∂ρ.fst, MeasureTheory.Integrable (fun ω => f (a, ω)) (ρ.condKernel a)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>F : Type u_4<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>NormedAddCommGroup F<VAR>ρ : MeasureTheory.Measure (α × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>f : α × Ω → F<VAR>hf_int : MeasureTheory.Integrable f ρ<GOAL>MeasureTheory.Integrable (fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂ρ.condKernel x) ρ.fst
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>E : Type u_3<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>ρ : MeasureTheory.Measure (α × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>f : α × Ω → E<VAR>hf_int : MeasureTheory.Integrable f ρ<GOAL>MeasureTheory.Integrable (fun x => ‖∫ (y : Ω), f (x, y) ∂ρ.condKernel x‖) ρ.fst
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>E : Type u_3<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>ρ : MeasureTheory.Measure (α × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>f : α × Ω → E<VAR>hf_int : MeasureTheory.Integrable f ρ<GOAL>MeasureTheory.Integrable (fun x => ∫ (y : Ω), f (x, y) ∂ρ.condKernel x) ρ.fst
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s : Set Ω<VAR>hcs : μ s ≠ 0<VAR>hs : μ s ≠ ⊤<GOAL>MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.cond μ s)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s : Set Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hcs : μ s ≠ 0<GOAL>MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.cond μ s)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s : Set Ω<GOAL>ProbabilityTheory.cond μ (MeasureTheory.toMeasurable μ s) = ProbabilityTheory.cond μ s
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s : Set Ω<GOAL>ProbabilityTheory.cond μ s ≪ μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>μ ≪ ProbabilityTheory.cond μ Set.univ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<GOAL>ProbabilityTheory.cond μ ∅ = 0
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<GOAL>ProbabilityTheory.cond μ Set.univ = μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s : Set Ω<VAR>hμs : μ s ≠ ⊤<GOAL>ProbabilityTheory.cond μ s = 0 ↔ μ s = 0
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s : Set Ω<VAR>hμs : μ s = 0<GOAL>ProbabilityTheory.cond μ s = 0
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s : Set Ω<VAR>hms : MeasurableSet s<VAR>t : Set Ω<GOAL>(ProbabilityTheory.cond μ s) t = (μ s)⁻¹ * μ (s ∩ t)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s t : Set Ω<VAR>hA : MeasurableSet t<GOAL>(ProbabilityTheory.cond μ s) t = (μ s)⁻¹ * μ (s ∩ t)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s : Set Ω<VAR>hms : MeasurableSet s<VAR>t : Set Ω<GOAL>(ProbabilityTheory.cond μ s) (s ∩ t) = (ProbabilityTheory.cond μ s) t
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s t : Set Ω<VAR>hms : MeasurableSet s<VAR>hcst : (ProbabilityTheory.cond μ s) t ≠ 0<GOAL>0 < μ (s ∩ t)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s t : Set Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hms : MeasurableSet s<VAR>hci : μ (s ∩ t) ≠ 0<GOAL>0 < (ProbabilityTheory.cond μ s) t
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s t : Set Ω<VAR>hms : MeasurableSet s<VAR>hmt : MeasurableSet t<VAR>hcs : μ s ≠ ⊤<GOAL>ProbabilityTheory.cond (ProbabilityTheory.cond μ s) t = ProbabilityTheory.cond μ (s ∩ t)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s t : Set Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hms : MeasurableSet s<VAR>hmt : MeasurableSet t<GOAL>ProbabilityTheory.cond (ProbabilityTheory.cond μ s) t = ProbabilityTheory.cond μ (s ∩ t)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s : Set Ω<VAR>hms : MeasurableSet s<VAR>hcs' : μ s ≠ ⊤<VAR>t : Set Ω<GOAL>(ProbabilityTheory.cond μ s) t * μ s = μ (s ∩ t)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s : Set Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hms : MeasurableSet s<VAR>t : Set Ω<GOAL>(ProbabilityTheory.cond μ s) t * μ s = μ (s ∩ t)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s t : Set Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hms : MeasurableSet s<GOAL>(ProbabilityTheory.cond μ s) t * μ s + (ProbabilityTheory.cond μ sᶜ) t * μ sᶜ = μ t
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s t : Set Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hms : MeasurableSet s<VAR>hmt : MeasurableSet t<GOAL>(ProbabilityTheory.cond μ s) t = (μ s)⁻¹ * (ProbabilityTheory.cond μ t) s * μ t
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : MeasureTheory.Measure Ω<VAR>s : Set Ω<VAR>i : Ω' → Ω<VAR>hi : MeasurableEmbedding i<VAR>hi' : ∀ᵐ (ω : Ω) ∂μ, ω ∈ Set.range i<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.Measure.comap i (ProbabilityTheory.cond μ s) = ProbabilityTheory.cond (MeasureTheory.Measure.comap i μ) (i ⁻¹' s)
<VAR>Ω : Type u_1<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>Fintype α<VAR>MeasurableSpace α<VAR>DiscreteMeasurableSpace α<VAR>X : Ω → α<VAR>hX : Measurable X<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>∑ x : α, μ (X ⁻¹' {x}) • ProbabilityTheory.cond μ (X ⁻¹' {x}) = μ
<GOAL>Turing.ToPartrec.Code.zero'.eval = fun v => pure (0 :: v)
<GOAL>Turing.ToPartrec.Code.succ.eval = fun v => pure [v.headI.succ]
<GOAL>Turing.ToPartrec.Code.tail.eval = fun v => pure v.tail
<VAR>f fs : Turing.ToPartrec.Code<GOAL>(f.cons fs).eval = fun v => do let n ← f.eval v let ns ← fs.eval v pure (n.headI :: ns)
<VAR>f g : Turing.ToPartrec.Code<GOAL>(f.comp g).eval = fun v => g.eval v >>= f.eval
<VAR>f g : Turing.ToPartrec.Code<GOAL>(f.case g).eval = fun v => Nat.rec (f.eval v.tail) (fun y x => g.eval (y :: v.tail)) v.headI
<VAR>f : Turing.ToPartrec.Code<GOAL>f.fix.eval = PFun.fix fun v => Part.map (fun v => if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)
<VAR>v : List ℕ<GOAL>Turing.ToPartrec.Code.nil.eval v = pure []
<VAR>v : List ℕ<GOAL>Turing.ToPartrec.Code.id.eval v = pure v
<VAR>v : List ℕ<GOAL>Turing.ToPartrec.Code.head.eval v = pure [v.headI]
<VAR>v : List ℕ<GOAL>Turing.ToPartrec.Code.zero.eval v = pure [0]
<VAR>v : List ℕ<GOAL>Turing.ToPartrec.Code.pred.eval v = pure [v.headI.pred]
<VAR>m n : ℕ<VAR>f : Mathlib.Vector ℕ n →. ℕ<VAR>g : Fin n → Mathlib.Vector ℕ m →. ℕ<VAR>hf : ∃ c, ∀ (v : Mathlib.Vector ℕ n), c.eval ↑v = pure <$> f v<VAR>hg : ∀ (i : Fin n), ∃ c, ∀ (v : Mathlib.Vector ℕ m), c.eval ↑v = pure <$> g i v<GOAL>∃ c, ∀ (v : Mathlib.Vector ℕ m), c.eval ↑v = pure <$> ((Mathlib.Vector.mOfFn fun i => g i v) >>= f)
<VAR>n : ℕ<VAR>f : Mathlib.Vector ℕ n →. ℕ<VAR>hf : Nat.Partrec' f<GOAL>∃ c, ∀ (v : Mathlib.Vector ℕ n), c.eval ↑v = pure <$> f v
<VAR>k k' : Turing.ToPartrec.Cont<VAR>v : List ℕ<GOAL>(k.then k').eval v = k.eval v >>= k'.eval
<VAR>c : Turing.ToPartrec.Code<VAR>k k' : Turing.ToPartrec.Cont<VAR>v : List ℕ<GOAL>Turing.ToPartrec.stepNormal c (k.then k') v = (Turing.ToPartrec.stepNormal c k v).then k'
<VAR>k k' : Turing.ToPartrec.Cont<VAR>v : List ℕ<GOAL>Turing.ToPartrec.stepRet (k.then k') v = (Turing.ToPartrec.stepRet k v).then k'
<VAR>c : Turing.ToPartrec.Code<VAR>h : c.Ok<VAR>v : List ℕ<GOAL>Turing.eval Turing.ToPartrec.step (Turing.ToPartrec.stepNormal c Turing.ToPartrec.Cont.halt v) = Turing.ToPartrec.Cfg.halt <$> c.eval v
<VAR>c : Turing.ToPartrec.Code<VAR>k : Turing.ToPartrec.Cont<VAR>v : List ℕ<GOAL>∃ k' v', Turing.ToPartrec.stepNormal c k v = Turing.ToPartrec.Cfg.ret k' v'
<VAR>f : Turing.ToPartrec.Code<VAR>k : Turing.ToPartrec.Cont<VAR>v : List ℕ<VAR>fok : f.Ok<GOAL>Turing.eval Turing.ToPartrec.step (Turing.ToPartrec.stepNormal f (Turing.ToPartrec.Cont.fix f k) v) = do let v ← f.fix.eval v Turing.eval Turing.ToPartrec.step (Turing.ToPartrec.Cfg.ret k v)
<VAR>c : Turing.ToPartrec.Code<GOAL>c.Ok
<VAR>c : Turing.ToPartrec.Code<VAR>v : List ℕ<GOAL>Turing.eval Turing.ToPartrec.step (Turing.ToPartrec.stepNormal c Turing.ToPartrec.Cont.halt v) = Turing.ToPartrec.Cfg.halt <$> c.eval v
<VAR>k : Turing.ToPartrec.Cont<VAR>v : List ℕ<GOAL>Turing.eval Turing.ToPartrec.step (Turing.ToPartrec.stepRet k v) = Turing.ToPartrec.Cfg.halt <$> k.eval v
<VAR>p : Turing.PartrecToTM2.Γ' → Bool<VAR>k₁ k₂ : Turing.PartrecToTM2.K'<VAR>q : Turing.PartrecToTM2.Λ'<GOAL>Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q) = Turing.PartrecToTM2.pop' k₁ (Turing.TM2.Stmt.branch (fun s => s.elim true p) (Turing.TM2.Stmt.goto fun x => q) (Turing.PartrecToTM2.push' k₂ (Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.Λ'.move p k₁ k₂ q)))
<VAR>k : Turing.PartrecToTM2.K'<VAR>f : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ'<VAR>q : Turing.PartrecToTM2.Λ'<GOAL>Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.push k f q) = Turing.TM2.Stmt.branch (fun s => (f s).isSome) (Turing.TM2.Stmt.push k (fun s => (f s).iget) (Turing.TM2.Stmt.goto fun x => q)) (Turing.TM2.Stmt.goto fun x => q)
<VAR>q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ'<GOAL>Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.read q) = Turing.TM2.Stmt.goto q
<VAR>p : Turing.PartrecToTM2.Γ' → Bool<VAR>k : Turing.PartrecToTM2.K'<VAR>q : Turing.PartrecToTM2.Λ'<GOAL>Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.clear p k q) = Turing.PartrecToTM2.pop' k (Turing.TM2.Stmt.branch (fun s => s.elim true p) (Turing.TM2.Stmt.goto fun x => q) (Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.Λ'.clear p k q))
<VAR>q : Turing.PartrecToTM2.Λ'<GOAL>Turing.PartrecToTM2.tr q.copy = Turing.PartrecToTM2.pop' Turing.PartrecToTM2.K'.rev (Turing.TM2.Stmt.branch Option.isSome (Turing.PartrecToTM2.push' Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.push' Turing.PartrecToTM2.K'.stack (Turing.TM2.Stmt.goto fun x => q.copy))) (Turing.TM2.Stmt.goto fun x => q))
<VAR>q : Turing.PartrecToTM2.Λ'<GOAL>Turing.PartrecToTM2.tr q.succ = Turing.PartrecToTM2.pop' Turing.PartrecToTM2.K'.main (Turing.TM2.Stmt.branch (fun s => decide (s = some Turing.PartrecToTM2.Γ'.bit1)) (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.rev (fun x => Turing.PartrecToTM2.Γ'.bit0) (Turing.TM2.Stmt.goto fun x => q.succ)) (Turing.TM2.Stmt.branch (fun s => decide (s = some Turing.PartrecToTM2.Γ'.cons)) (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.main (fun x => Turing.PartrecToTM2.Γ'.cons) (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.main (fun x => Turing.PartrecToTM2.Γ'.bit1) (Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.unrev q))) (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.main (fun x => Turing.PartrecToTM2.Γ'.bit1) (Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.unrev q))))
<VAR>q₁ q₂ : Turing.PartrecToTM2.Λ'<GOAL>Turing.PartrecToTM2.tr (q₁.pred q₂) = Turing.PartrecToTM2.pop' Turing.PartrecToTM2.K'.main (Turing.TM2.Stmt.branch (fun s => decide (s = some Turing.PartrecToTM2.Γ'.bit0)) (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.rev (fun x => Turing.PartrecToTM2.Γ'.bit1) (Turing.TM2.Stmt.goto fun x => q₁.pred q₂)) (Turing.TM2.Stmt.branch (fun s => Turing.PartrecToTM2.natEnd s.iget) (Turing.TM2.Stmt.goto fun x => q₁) (Turing.PartrecToTM2.peek' Turing.PartrecToTM2.K'.main (Turing.TM2.Stmt.branch (fun s => Turing.PartrecToTM2.natEnd s.iget) (Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.unrev q₂) (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.rev (fun x => Turing.PartrecToTM2.Γ'.bit0) (Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.unrev q₂))))))
<VAR>fs : Turing.ToPartrec.Code<VAR>k : Turing.PartrecToTM2.Cont'<GOAL>Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k)) = Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.move₂ (fun x => false) Turing.PartrecToTM2.K'.main Turing.PartrecToTM2.K'.aux (Turing.PartrecToTM2.move₂ (fun s => decide (s = Turing.PartrecToTM2.Γ'.consₗ)) Turing.PartrecToTM2.K'.stack Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.move₂ (fun x => false) Turing.PartrecToTM2.K'.aux Turing.PartrecToTM2.K'.stack (Turing.PartrecToTM2.trNormal fs k.cons₂)))
<VAR>k : Turing.PartrecToTM2.Cont'<GOAL>Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret k.cons₂) = Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.stack (Turing.PartrecToTM2.Λ'.ret k)
<VAR>f : Turing.ToPartrec.Code<VAR>k : Turing.PartrecToTM2.Cont'<GOAL>Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k)) = Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.trNormal f k
<VAR>f : Turing.ToPartrec.Code<VAR>k : Turing.PartrecToTM2.Cont'<GOAL>Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k)) = Turing.PartrecToTM2.pop' Turing.PartrecToTM2.K'.main (Turing.TM2.Stmt.goto fun s => bif Turing.PartrecToTM2.natEnd s.iget then Turing.PartrecToTM2.Λ'.ret k else Turing.PartrecToTM2.Λ'.clear Turing.PartrecToTM2.natEnd Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.trNormal f (Turing.PartrecToTM2.Cont'.fix f k)))
<GOAL>Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt) = Turing.TM2.Stmt.load (fun x => none) Turing.TM2.Stmt.halt
<GOAL>Turing.PartrecToTM2.trNat 0 = []
<GOAL>Turing.PartrecToTM2.trNat default = []
<VAR>a b c d : List Turing.PartrecToTM2.Γ'<GOAL>Turing.PartrecToTM2.K'.elim a b c d Turing.PartrecToTM2.K'.main = a
<VAR>a b c d : List Turing.PartrecToTM2.Γ'<GOAL>Turing.PartrecToTM2.K'.elim a b c d Turing.PartrecToTM2.K'.rev = b
<VAR>a b c d : List Turing.PartrecToTM2.Γ'<GOAL>Turing.PartrecToTM2.K'.elim a b c d Turing.PartrecToTM2.K'.aux = c
<VAR>a b c d : List Turing.PartrecToTM2.Γ'<GOAL>Turing.PartrecToTM2.K'.elim a b c d Turing.PartrecToTM2.K'.stack = d
<VAR>a b c d a' : List Turing.PartrecToTM2.Γ'<GOAL>Function.update (Turing.PartrecToTM2.K'.elim a b c d) Turing.PartrecToTM2.K'.main a' = Turing.PartrecToTM2.K'.elim a' b c d
<VAR>a b c d b' : List Turing.PartrecToTM2.Γ'<GOAL>Function.update (Turing.PartrecToTM2.K'.elim a b c d) Turing.PartrecToTM2.K'.rev b' = Turing.PartrecToTM2.K'.elim a b' c d
<VAR>a b c d c' : List Turing.PartrecToTM2.Γ'<GOAL>Function.update (Turing.PartrecToTM2.K'.elim a b c d) Turing.PartrecToTM2.K'.aux c' = Turing.PartrecToTM2.K'.elim a b c' d
<VAR>a b c d d' : List Turing.PartrecToTM2.Γ'<GOAL>Function.update (Turing.PartrecToTM2.K'.elim a b c d) Turing.PartrecToTM2.K'.stack d' = Turing.PartrecToTM2.K'.elim a b c d'
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>L l₁ : List α<VAR>o : Option α<VAR>l₂ : List α<GOAL>(∀ x ∈ l₁, p x = false) → Option.elim' (L = l₁ ∧ l₂ = []) (fun a => p a = true ∧ L = l₁ ++ a :: l₂) o → Turing.PartrecToTM2.splitAtPred p L = (l₁, o, l₂)
<VAR>α : Type u_1<VAR>L : List α<GOAL>Turing.PartrecToTM2.splitAtPred (fun x => false) L = (L, none, [])
<VAR>p : Turing.PartrecToTM2.Γ' → Bool<VAR>k₁ k₂ : Turing.PartrecToTM2.K'<VAR>q : Turing.PartrecToTM2.Λ'<VAR>s : Option Turing.PartrecToTM2.Γ'<VAR>L₁ : List Turing.PartrecToTM2.Γ'<VAR>o : Option Turing.PartrecToTM2.Γ'<VAR>L₂ : List Turing.PartrecToTM2.Γ'<VAR>S : Turing.PartrecToTM2.K' → List Turing.PartrecToTM2.Γ'<VAR>h₁ : k₁ ≠ k₂<VAR>e : Turing.PartrecToTM2.splitAtPred p (S k₁) = (L₁, o, L₂)<GOAL>Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) { l := some (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q), var := s, stk := S } { l := some q, var := o, stk := Function.update (Function.update S k₁ L₂) k₂ (L₁.reverseAux (S k₂)) }
<VAR>q : Turing.PartrecToTM2.Λ'<VAR>s : Option Turing.PartrecToTM2.Γ'<VAR>S : Turing.PartrecToTM2.K' → List Turing.PartrecToTM2.Γ'<GOAL>Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) { l := some (Turing.PartrecToTM2.unrev q), var := s, stk := S } { l := some q, var := none, stk := Function.update (Function.update S Turing.PartrecToTM2.K'.rev []) Turing.PartrecToTM2.K'.main ((S Turing.PartrecToTM2.K'.rev).reverseAux (S Turing.PartrecToTM2.K'.main)) }
<VAR>p : Turing.PartrecToTM2.Γ' → Bool<VAR>k₁ k₂ : Turing.PartrecToTM2.K'<VAR>q : Turing.PartrecToTM2.Λ'<VAR>s : Option Turing.PartrecToTM2.Γ'<VAR>L₁ : List Turing.PartrecToTM2.Γ'<VAR>o : Option Turing.PartrecToTM2.Γ'<VAR>L₂ : List Turing.PartrecToTM2.Γ'<VAR>S : Turing.PartrecToTM2.K' → List Turing.PartrecToTM2.Γ'<VAR>h₁ : k₁ ≠ Turing.PartrecToTM2.K'.rev ∧ k₂ ≠ Turing.PartrecToTM2.K'.rev ∧ k₁ ≠ k₂<VAR>h₂ : S Turing.PartrecToTM2.K'.rev = []<VAR>e : Turing.PartrecToTM2.splitAtPred p (S k₁) = (L₁, o, L₂)<GOAL>Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) { l := some (Turing.PartrecToTM2.move₂ p k₁ k₂ q), var := s, stk := S } { l := some q, var := none, stk := Function.update (Function.update S k₁ (o.elim id List.cons L₂)) k₂ (L₁ ++ S k₂) }
<VAR>p : Turing.PartrecToTM2.Γ' → Bool<VAR>k : Turing.PartrecToTM2.K'<VAR>q : Turing.PartrecToTM2.Λ'<VAR>s : Option Turing.PartrecToTM2.Γ'<VAR>L₁ : List Turing.PartrecToTM2.Γ'<VAR>o : Option Turing.PartrecToTM2.Γ'<VAR>L₂ : List Turing.PartrecToTM2.Γ'<VAR>S : Turing.PartrecToTM2.K' → List Turing.PartrecToTM2.Γ'<VAR>e : Turing.PartrecToTM2.splitAtPred p (S k) = (L₁, o, L₂)<GOAL>Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) { l := some (Turing.PartrecToTM2.Λ'.clear p k q), var := s, stk := S } { l := some q, var := o, stk := Function.update S k L₂ }
<VAR>q : Turing.PartrecToTM2.Λ'<VAR>s : Option Turing.PartrecToTM2.Γ'<VAR>a b c d : List Turing.PartrecToTM2.Γ'<GOAL>Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) { l := some q.copy, var := s, stk := Turing.PartrecToTM2.K'.elim a b c d } { l := some q, var := none, stk := Turing.PartrecToTM2.K'.elim (b.reverseAux a) [] c (b.reverseAux d) }
<VAR>n : PosNum<VAR>x : Turing.PartrecToTM2.Γ'<GOAL>x ∈ Turing.PartrecToTM2.trPosNum n → Turing.PartrecToTM2.natEnd x = false
<VAR>n : Num<VAR>x : Turing.PartrecToTM2.Γ'<GOAL>x ∈ Turing.PartrecToTM2.trNum n → Turing.PartrecToTM2.natEnd x = false
<VAR>n : ℕ<VAR>x : Turing.PartrecToTM2.Γ'<GOAL>x ∈ Turing.PartrecToTM2.trNat n → Turing.PartrecToTM2.natEnd x = false
<VAR>l : List ℕ<VAR>x : Turing.PartrecToTM2.Γ'<GOAL>x ∈ Turing.PartrecToTM2.trList l → x ≠ Turing.PartrecToTM2.Γ'.consₗ
<VAR>q : Turing.PartrecToTM2.Λ'<VAR>s : Option Turing.PartrecToTM2.Γ'<VAR>L : List ℕ<VAR>c d : List Turing.PartrecToTM2.Γ'<GOAL>Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) { l := some (Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.main q), var := s, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList L) [] c d } { l := some q, var := none, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList [L.headI]) [] c d }
<VAR>q : Turing.PartrecToTM2.Λ'<VAR>s : Option Turing.PartrecToTM2.Γ'<VAR>L₁ L₂ : List ℕ<VAR>L₃ : List Turing.PartrecToTM2.Γ'<GOAL>Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) { l := some (Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.stack q), var := s, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList L₁) [] [] (Turing.PartrecToTM2.trList L₂ ++ Turing.PartrecToTM2.Γ'.consₗ :: L₃) } { l := some q, var := none, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList (L₂.headI :: L₁)) [] [] L₃ }
<VAR>q : Turing.PartrecToTM2.Λ'<VAR>s : Option Turing.PartrecToTM2.Γ'<VAR>n : ℕ<VAR>c d : List Turing.PartrecToTM2.Γ'<GOAL>Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) { l := some q.succ, var := s, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList [n]) [] c d } { l := some q, var := none, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList [n.succ]) [] c d }
<VAR>q₁ q₂ : Turing.PartrecToTM2.Λ'<VAR>s : Option Turing.PartrecToTM2.Γ'<VAR>v : List ℕ<VAR>c d : List Turing.PartrecToTM2.Γ'<GOAL>∃ s', Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) { l := some (q₁.pred q₂), var := s, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList v) [] c d } (Nat.rec { l := some q₁, var := s', stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList v.tail) [] c d } (fun n x => { l := some q₂, var := s', stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList (n :: v.tail)) [] c d }) v.headI)
<VAR>c : Turing.ToPartrec.Code<VAR>k : Turing.ToPartrec.Cont<VAR>v : List ℕ<VAR>s : Option Turing.PartrecToTM2.Γ'<GOAL>∃ b₂, Turing.PartrecToTM2.TrCfg (Turing.ToPartrec.stepNormal c k v) b₂ ∧ Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) { l := some (Turing.PartrecToTM2.trNormal c (Turing.PartrecToTM2.trCont k)), var := s, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList v) [] [] (Turing.PartrecToTM2.trContStack k) } b₂
<VAR>k : Turing.ToPartrec.Cont<VAR>v : List ℕ<VAR>s : Option Turing.PartrecToTM2.Γ'<GOAL>∃ b₂, Turing.PartrecToTM2.TrCfg (Turing.ToPartrec.stepRet k v) b₂ ∧ Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) { l := some (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.trCont k)), var := s, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList v) [] [] (Turing.PartrecToTM2.trContStack k) } b₂
<GOAL>Turing.Respects Turing.ToPartrec.step (Turing.TM2.step Turing.PartrecToTM2.tr) Turing.PartrecToTM2.TrCfg
<VAR>c : Turing.ToPartrec.Code<VAR>v : List ℕ<GOAL>∃ b, Turing.PartrecToTM2.TrCfg (Turing.ToPartrec.stepNormal c Turing.ToPartrec.Cont.halt v) b ∧ Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) (Turing.PartrecToTM2.init c v) b
<VAR>c : Turing.ToPartrec.Code<VAR>v : List ℕ<GOAL>Turing.eval (Turing.TM2.step Turing.PartrecToTM2.tr) (Turing.PartrecToTM2.init c v) = Turing.PartrecToTM2.halt <$> c.eval v
<VAR>q q' : Turing.PartrecToTM2.Λ'<GOAL>q' ∈ Turing.PartrecToTM2.trStmts₁ q → Turing.PartrecToTM2.trStmts₁ q' ⊆ Turing.PartrecToTM2.trStmts₁ q
<VAR>q : Turing.PartrecToTM2.Λ'<GOAL>q ∈ Turing.PartrecToTM2.trStmts₁ q
<VAR>c : Turing.ToPartrec.Code<VAR>k : Turing.PartrecToTM2.Cont'<GOAL>Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal c k) ⊆ Turing.PartrecToTM2.codeSupp' c k
<VAR>c : Turing.ToPartrec.Code<VAR>k : Turing.PartrecToTM2.Cont'<GOAL>Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal c k) ⊆ Turing.PartrecToTM2.codeSupp c k
<VAR>k : Turing.PartrecToTM2.Cont'<GOAL>Turing.PartrecToTM2.codeSupp Turing.ToPartrec.Code.zero' k = Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal Turing.ToPartrec.Code.zero' k) ∪ Turing.PartrecToTM2.contSupp k
<VAR>k : Turing.PartrecToTM2.Cont'<GOAL>Turing.PartrecToTM2.codeSupp Turing.ToPartrec.Code.succ k = Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal Turing.ToPartrec.Code.succ k) ∪ Turing.PartrecToTM2.contSupp k
<VAR>k : Turing.PartrecToTM2.Cont'<GOAL>Turing.PartrecToTM2.codeSupp Turing.ToPartrec.Code.tail k = Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal Turing.ToPartrec.Code.tail k) ∪ Turing.PartrecToTM2.contSupp k
<VAR>f fs : Turing.ToPartrec.Code<VAR>k : Turing.PartrecToTM2.Cont'<GOAL>Turing.PartrecToTM2.codeSupp (f.cons fs) k = Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal (f.cons fs) k) ∪ Turing.PartrecToTM2.codeSupp f (Turing.PartrecToTM2.Cont'.cons₁ fs k)
<VAR>f g : Turing.ToPartrec.Code<VAR>k : Turing.PartrecToTM2.Cont'<GOAL>Turing.PartrecToTM2.codeSupp (f.comp g) k = Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal (f.comp g) k) ∪ Turing.PartrecToTM2.codeSupp g (Turing.PartrecToTM2.Cont'.comp f k)