internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Derivation.ProofList.F_primrec
Proof state before:
μ : Type ?u.22616
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec₂ fun p f => decide (Semiformula.nrel f.snd.1 f.snd.2 ∈ p.1.1)
Tactic:
apply list_mem.comp₂ (Semiformula.nrel_primrec.comp₂ Primrec₂.right) (fst.comp₂ $ fst.comp₂ Primrec₂.left)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.F_primrec
Proof state before:
μ : Type ?u.22616
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec₂ fun p val => (fun x => decide (⊤ ∈ p.1.1.1)) val
Tactic:
apply list_mem.comp₂ (Primrec₂.const ⊤) (fst.comp₂ $ fst.comp₂ $ fst.comp₂ Primrec₂.left)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.F_primrec
Proof state before:
μ : Type ?u.22616
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec₂ fun p val => decide (val.1 ⋏ val.2 ∈ p.1.1.1.1)
Tactic:
apply list_mem.comp₂
  (Semiformula.and_primrec.comp₂ (fst.comp₂ Primrec₂.right) (snd.comp₂ Primrec₂.right))
  (fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ Primrec₂.left)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.F_primrec
Proof state before:
μ : Type ?u.22616
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec₂ fun p val => decide (val.1 :: p.1.1.1.1 ∈ p.1.1.1.2)
Tactic:
apply (list_mem (α := List (SyntacticFormula L))).comp₂
  (list_cons.comp₂ (fst.comp₂ Primrec₂.right) (fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ Primrec₂.left))
  (snd.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ Primrec₂.left)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.F_primrec
Proof state before:
μ : Type ?u.22616
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec₂ fun p val => decide (val.2 :: p.1.1.1.1 ∈ p.1.1.1.2)
Tactic:
apply list_mem.comp₂
  (list_cons.comp₂ (snd.comp₂ Primrec₂.right) (fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ Primrec₂.left))
  (snd.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ Primrec₂.left)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.F_primrec
Proof state before:
μ : Type ?u.22616
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec₂ fun p val => decide (val.1 ⋎ val.2 ∈ p.1.1.1.1.1)
Tactic:
apply list_mem.comp₂
  (Semiformula.or_primrec.comp₂ (fst.comp₂ Primrec₂.right) (snd.comp₂ Primrec₂.right))
  (fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ Primrec₂.left)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.F_primrec
Proof state before:
μ : Type ?u.22616
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec₂ fun p val => decide (val.1 :: val.2 :: p.1.1.1.1.1 ∈ p.1.1.1.1.2)
Tactic:
apply list_mem.comp₂
  (by apply list_cons.comp₂ (fst.comp₂ Primrec₂.right) $ list_cons.comp₂
        (snd.comp₂ Primrec₂.right)
        (fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ Primrec₂.left))
  (snd.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ Primrec₂.left)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.F_primrec
Proof state before:
μ : Type ?u.22616
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec₂ fun a b => b.1 :: b.2 :: a.1.1.1.1.1
Tactic:
apply list_cons.comp₂ (fst.comp₂ Primrec₂.right) $ list_cons.comp₂
  (snd.comp₂ Primrec₂.right)
  (fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ Primrec₂.left)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.F_primrec
Proof state before:
μ : Type ?u.22616
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec₂ fun p val => decide (∀' val ∈ p.1.1.1.1.1.1)
Tactic:
apply list_mem.comp₂
  (Semiformula.all_primrec.comp₂ Primrec₂.right)
  (fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ Primrec₂.left)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.F_primrec
Proof state before:
μ : Type ?u.22616
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec₂ fun p val => decide ((Rew.hom Rew.free) val :: List.map (⇑(Rew.hom ⇑)) p.1.1.1.1.1.1 ∈ p.1.1.1.1.1.2)
Tactic:
apply list_mem.comp₂
  (list_cons.comp₂
    (Semiformula.free_primrec.comp₂ Primrec₂.right)
    (to₂' <| by apply list_map
                  (fst.comp $ fst.comp $ fst.comp $ fst.comp $ fst.comp $ fst.comp $ fst)
                  (Semiformula.shift_primrec.comp₂ Primrec₂.right)))
  (snd.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ Primrec₂.left)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.F_primrec
Proof state before:
μ : Type ?u.22616
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec fun p => List.map (⇑(Rew.hom ⇑)) p.1.1.1.1.1.1.1
Tactic:
apply list_map
  (fst.comp $ fst.comp $ fst.comp $ fst.comp $ fst.comp $ fst.comp $ fst)
  (Semiformula.shift_primrec.comp₂ Primrec₂.right)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.F_primrec
Proof state before:
μ : Type ?u.22616
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec₂ fun p val => decide (∃' val.1 ∈ p.1.1.1.1.1.1.1)
Tactic:
apply list_mem.comp₂
  (Semiformula.ex_primrec.comp₂ $ fst.comp₂ Primrec₂.right)
  (fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ Primrec₂.left)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.F_primrec
Proof state before:
μ : Type ?u.22616
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec₂ fun p val => decide ([→ val.2].hom val.1 :: p.1.1.1.1.1.1.1 ∈ p.1.1.1.1.1.1.2)
Tactic:
apply list_mem.comp₂
  (by apply list_cons.comp₂
        (by apply Semiformula.substs₁_primrec.comp₂ (snd.comp₂ Primrec₂.right) (fst.comp₂ Primrec₂.right))
        (by apply fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ Primrec₂.left))
  (snd.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ Primrec₂.left)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.F_primrec
Proof state before:
μ : Type ?u.22616
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec₂ fun a b => [→ b.2].hom b.1 :: a.1.1.1.1.1.1.1
Tactic:
apply list_cons.comp₂
  (by apply Semiformula.substs₁_primrec.comp₂ (snd.comp₂ Primrec₂.right) (fst.comp₂ Primrec₂.right))
  (by apply fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ Primrec₂.left)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.F_primrec
Proof state before:
μ : Type ?u.22616
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec₂ fun a b => [→ b.2].hom b.1
Tactic:
apply Semiformula.substs₁_primrec.comp₂ (snd.comp₂ Primrec₂.right) (fst.comp₂ Primrec₂.right)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.F_primrec
Proof state before:
μ : Type ?u.22616
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec₂ fun a b => a.1.1.1.1.1.1.1
Tactic:
apply fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ Primrec₂.left
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.F_primrec
Proof state before:
μ : Type ?u.22616
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec₂ fun p val => decide (val ⊆ p.1.1.1.1.1.1.1)
Tactic:
apply list_subset.comp₂
  Primrec₂.right
  (fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ Primrec₂.left)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.F_primrec
Proof state before:
μ : Type ?u.22616
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec₂ fun p val => decide (val ∈ p.1.1.1.1.1.1.2)
Tactic:
apply list_mem.comp₂
  Primrec₂.right
  (by apply snd.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ Primrec₂.left)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.F_primrec
Proof state before:
μ : Type ?u.22616
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec₂ fun a b => a.1.1.1.1.1.1.2
Tactic:
apply snd.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ Primrec₂.left
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_primrec
Proof state before:
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec isProper
Tactic:
have : Primrec₂ (fun _ p => p.2.2 && F p.1.2 (sequents p.2.1) p.1.1
  : ProofList L → (Code L × List (SyntacticFormula L)) × (List (Code L × List (SyntacticFormula L))) × Bool → Bool) :=
  (dom_bool₂ _).comp₂ (snd.comp₂ $ snd.comp₂ Primrec₂.right)
  (F_primrec.comp₂
      ((Primrec₂.pair.comp (snd.comp fst) (list_map (fst.comp snd) (snd.comp₂ Primrec₂.right))).comp₂ Primrec₂.right)
      (fst.comp₂ $ fst.comp₂ Primrec₂.right))
Proof state after:
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this : Primrec₂ fun x p => p.2.2 && LO.FirstOrder.Derivation.ProofList.F p.1.2 (sequents p.2.1) p.1.1
⊢ Primrec isProper
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_primrec
Proof state before:
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this : Primrec₂ fun x p => p.2.2 && LO.FirstOrder.Derivation.ProofList.F p.1.2 (sequents p.2.1) p.1.1
⊢ Primrec isProper
Tactic:
have : Primrec (fun l => l.rec true (fun c l' ih => ih && F c.2 (sequents l') c.1) : ProofList L → Bool) :=
  list_rec Primrec.id (const true) this
Proof state after:
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this✝ : Primrec₂ fun x p => p.2.2 && LO.FirstOrder.Derivation.ProofList.F p.1.2 (sequents p.2.1) p.1.1
this :
  Primrec fun l => List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l
⊢ Primrec isProper
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_primrec
Proof state before:
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this✝ : Primrec₂ fun x p => p.2.2 && LO.FirstOrder.Derivation.ProofList.F p.1.2 (sequents p.2.1) p.1.1
this :
  Primrec fun l => List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l
⊢ Primrec isProper
Tactic:
exact this.of_eq <| by
  intro l; induction' l with c l ih <;> simp[isProper]
  rw[ih]; rcases c with ⟨⟨⟩, Γ⟩ <;> simp[isProper, F, Code.equiv, Bool.and_assoc]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_primrec
Proof state before:
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this✝ : Primrec₂ fun x p => p.2.2 && LO.FirstOrder.Derivation.ProofList.F p.1.2 (sequents p.2.1) p.1.1
this :
  Primrec fun l => List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l
⊢ ∀ (n : ProofList L),
    List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) n = n.isProper
Tactic:
intro l
Proof state after:
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this✝ : Primrec₂ fun x p => p.2.2 && LO.FirstOrder.Derivation.ProofList.F p.1.2 (sequents p.2.1) p.1.1
this :
  Primrec fun l => List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l
l : ProofList L
⊢ List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l = l.isProper
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_primrec
Proof state before:
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this✝ : Primrec₂ fun x p => p.2.2 && LO.FirstOrder.Derivation.ProofList.F p.1.2 (sequents p.2.1) p.1.1
this :
  Primrec fun l => List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l
l : ProofList L
⊢ List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l = l.isProper
Tactic:
induction' l with c l ih <;> simp[isProper]
Proof state after:
case cons
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this✝ : Primrec₂ fun x p => p.2.2 && LO.FirstOrder.Derivation.ProofList.F p.1.2 (sequents p.2.1) p.1.1
this :
  Primrec fun l => List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l
c : Code L × List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
ih : List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l = isProper l
⊢ (List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l &&
      LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l) c.1) =
    isProper (c :: l)
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_primrec
Proof state before:
case cons
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this✝ : Primrec₂ fun x p => p.2.2 && LO.FirstOrder.Derivation.ProofList.F p.1.2 (sequents p.2.1) p.1.1
this :
  Primrec fun l => List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l
c : Code L × List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
ih : List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l = isProper l
⊢ (List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l &&
      LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l) c.1) =
    isProper (c :: l)
Tactic:
rw[ih]
Proof state after:
case cons
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this✝ : Primrec₂ fun x p => p.2.2 && LO.FirstOrder.Derivation.ProofList.F p.1.2 (sequents p.2.1) p.1.1
this :
  Primrec fun l => List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l
c : Code L × List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
ih : List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l = isProper l
⊢ (isProper l && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l) c.1) = isProper (c :: l)
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_primrec
Proof state before:
case cons
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this✝ : Primrec₂ fun x p => p.2.2 && LO.FirstOrder.Derivation.ProofList.F p.1.2 (sequents p.2.1) p.1.1
this :
  Primrec fun l => List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l
c : Code L × List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
ih : List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l = isProper l
⊢ (isProper l && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l) c.1) = isProper (c :: l)
Tactic:
rcases c with ⟨⟨⟩, Γ⟩ <;> simp[isProper, F, Code.equiv, Bool.and_assoc]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.sequents_append
Proof state before:
μ : Type ?u.465354
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
l₁ l₂ : ProofList L
⊢ (l₁ ++ l₂).sequents = l₁.sequents ++ l₂.sequents
Tactic:
simp[sequents]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_append
Proof state before:
μ : Type ?u.466511
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
l₁ l₂ : ProofList L
h₁ : l₁.isProper = true
h₂ : l₂.isProper = true
⊢ (l₁ ++ l₂).isProper = true
Tactic:
induction' l₁ with c l₁ ih
Proof state after:
case nil
μ : Type ?u.466511
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
l₂ : ProofList L
h₂ : l₂.isProper = true
h₁ : isProper [] = true
⊢ ([] ++ l₂).isProper = true

case cons
μ : Type ?u.466511
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
l₂ : ProofList L
h₂ : l₂.isProper = true
c : Code L × List (SyntacticFormula L)
l₁ : List (Code L × List (SyntacticFormula L))
ih : isProper l₁ = true → (l₁ ++ l₂).isProper = true
h₁ : isProper (c :: l₁) = true
⊢ (c :: l₁ ++ l₂).isProper = true
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_append
Proof state before:
case nil
μ : Type ?u.466511
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
l₂ : ProofList L
h₂ : l₂.isProper = true
h₁ : isProper [] = true
⊢ ([] ++ l₂).isProper = true
Tactic:
simpa
Proof state after:
no goals