internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.T_18_1_right
Proof state before:
case h1.h1.h1.a.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v Q, forall_ v ((P.imp_ Q).and_ (Q.imp_ P))} ((P.imp_ Q).and_ (Q.imp_ P))
Tactic:
apply specId v
Proof state after:
case h1.h1.h1.a.a.h1
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v Q, forall_ v ((P.imp_ Q).and_ (Q.imp_ P))} (forall_ v ((P.imp_ Q).and_ (Q.imp_ P)))
Theorem: FOL.NV.T_18_1_right
Proof state before:
case h1.h1.h1.a.a.h1
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v Q, forall_ v ((P.imp_ Q).and_ (Q.imp_ P))} (forall_ v ((P.imp_ Q).and_ (Q.imp_ P)))
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.h1.h1.a.a.h1.a
P Q : Formula
v : VarName
⊢ forall_ v ((P.imp_ Q).and_ (Q.imp_ P)) ∈ {forall_ v Q, forall_ v ((P.imp_ Q).and_ (Q.imp_ P))}
Theorem: FOL.NV.T_18_1_right
Proof state before:
case h1.h1.h1.a.a.h1.a
P Q : Formula
v : VarName
⊢ forall_ v ((P.imp_ Q).and_ (Q.imp_ P)) ∈ {forall_ v Q, forall_ v ((P.imp_ Q).and_ (Q.imp_ P))}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_18_1_right
Proof state before:
case h1.h1.h1.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v Q, forall_ v ((P.imp_ Q).and_ (Q.imp_ P))} Q
Tactic:
apply specId v
Proof state after:
case h1.h1.h1.a.h1
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v Q, forall_ v ((P.imp_ Q).and_ (Q.imp_ P))} (forall_ v Q)
Theorem: FOL.NV.T_18_1_right
Proof state before:
case h1.h1.h1.a.h1
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v Q, forall_ v ((P.imp_ Q).and_ (Q.imp_ P))} (forall_ v Q)
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.h1.h1.a.h1.a
P Q : Formula
v : VarName
⊢ forall_ v Q ∈ {forall_ v Q, forall_ v ((P.imp_ Q).and_ (Q.imp_ P))}
Theorem: FOL.NV.T_18_1_right
Proof state before:
case h1.h1.h1.a.h1.a
P Q : Formula
v : VarName
⊢ forall_ v Q ∈ {forall_ v Q, forall_ v ((P.imp_ Q).and_ (Q.imp_ P))}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_18_1_right
Proof state before:
case h1.h1.h2
P Q : Formula
v : VarName
⊢ ∀ H ∈ {forall_ v Q, forall_ v ((P.imp_ Q).and_ (Q.imp_ P))}, ¬isFreeIn v H
Tactic:
simp
Proof state after:
case h1.h1.h2
P Q : Formula
v : VarName
⊢ ¬isFreeIn v (forall_ v Q) ∧ ¬isFreeIn v (forall_ v ((P.imp_ Q).and_ (Q.imp_ P)))
Theorem: FOL.NV.T_18_1_right
Proof state before:
case h1.h1.h2
P Q : Formula
v : VarName
⊢ ¬isFreeIn v (forall_ v Q) ∧ ¬isFreeIn v (forall_ v ((P.imp_ Q).and_ (Q.imp_ P)))
Tactic:
simp only [isFreeIn]
Proof state after:
case h1.h1.h2
P Q : Formula
v : VarName
⊢ ¬(¬True ∧ isFreeIn v Q) ∧ ¬(¬True ∧ ((isFreeIn v P ∨ isFreeIn v Q) ∨ isFreeIn v Q ∨ isFreeIn v P))
Theorem: FOL.NV.T_18_1_right
Proof state before:
case h1.h1.h2
P Q : Formula
v : VarName
⊢ ¬(¬True ∧ isFreeIn v Q) ∧ ¬(¬True ∧ ((isFreeIn v P ∨ isFreeIn v Q) ∨ isFreeIn v Q ∨ isFreeIn v P))
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_18_1
Proof state before:
P Q : Formula
v : VarName
⊢ IsProof ((forall_ v (P.iff_ Q)).imp_ ((forall_ v P).iff_ (forall_ v Q)))
Tactic:
apply IsDeduct.mp_ ((forall_ v (P.iff_ Q)).imp_ ((forall_ v Q).imp_ (forall_ v P)))
Proof state after:
case a
P Q : Formula
v : VarName
⊢ IsDeduct ∅
    (((forall_ v (P.iff_ Q)).imp_ ((forall_ v Q).imp_ (forall_ v P))).imp_
      ((forall_ v (P.iff_ Q)).imp_ ((forall_ v P).iff_ (forall_ v Q))))

case a
P Q : Formula
v : VarName
⊢ IsDeduct ∅ ((forall_ v (P.iff_ Q)).imp_ ((forall_ v Q).imp_ (forall_ v P)))
Theorem: FOL.NV.T_18_1
Proof state before:
case a
P Q : Formula
v : VarName
⊢ IsDeduct ∅
    (((forall_ v (P.iff_ Q)).imp_ ((forall_ v Q).imp_ (forall_ v P))).imp_
      ((forall_ v (P.iff_ Q)).imp_ ((forall_ v P).iff_ (forall_ v Q))))
Tactic:
apply IsDeduct.mp_ ((forall_ v (P.iff_ Q)).imp_ ((forall_ v P).imp_ (forall_ v Q)))
Proof state after:
case a.a
P Q : Formula
v : VarName
⊢ IsDeduct ∅
    (((forall_ v (P.iff_ Q)).imp_ ((forall_ v P).imp_ (forall_ v Q))).imp_
      (((forall_ v (P.iff_ Q)).imp_ ((forall_ v Q).imp_ (forall_ v P))).imp_
        ((forall_ v (P.iff_ Q)).imp_ ((forall_ v P).iff_ (forall_ v Q)))))

case a.a
P Q : Formula
v : VarName
⊢ IsDeduct ∅ ((forall_ v (P.iff_ Q)).imp_ ((forall_ v P).imp_ (forall_ v Q)))
Theorem: FOL.NV.T_18_1
Proof state before:
case a.a
P Q : Formula
v : VarName
⊢ IsDeduct ∅
    (((forall_ v (P.iff_ Q)).imp_ ((forall_ v P).imp_ (forall_ v Q))).imp_
      (((forall_ v (P.iff_ Q)).imp_ ((forall_ v Q).imp_ (forall_ v P))).imp_
        ((forall_ v (P.iff_ Q)).imp_ ((forall_ v P).iff_ (forall_ v Q)))))
Tactic:
simp only [def_iff_]
Proof state after:
case a.a
P Q : Formula
v : VarName
⊢ IsDeduct ∅
    (((forall_ v ((P.imp_ Q).and_ (Q.imp_ P))).imp_ ((forall_ v P).imp_ (forall_ v Q))).imp_
      (((forall_ v ((P.imp_ Q).and_ (Q.imp_ P))).imp_ ((forall_ v Q).imp_ (forall_ v P))).imp_
        ((forall_ v ((P.imp_ Q).and_ (Q.imp_ P))).imp_
          (((forall_ v P).imp_ (forall_ v Q)).and_ ((forall_ v Q).imp_ (forall_ v P))))))
Theorem: FOL.NV.T_18_1
Proof state before:
case a.a
P Q : Formula
v : VarName
⊢ IsDeduct ∅
    (((forall_ v ((P.imp_ Q).and_ (Q.imp_ P))).imp_ ((forall_ v P).imp_ (forall_ v Q))).imp_
      (((forall_ v ((P.imp_ Q).and_ (Q.imp_ P))).imp_ ((forall_ v Q).imp_ (forall_ v P))).imp_
        ((forall_ v ((P.imp_ Q).and_ (Q.imp_ P))).imp_
          (((forall_ v P).imp_ (forall_ v Q)).and_ ((forall_ v Q).imp_ (forall_ v P))))))
Tactic:
simp only [def_and_]
Proof state after:
case a.a
P Q : Formula
v : VarName
⊢ IsDeduct ∅
    (((forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_ ((forall_ v P).imp_ (forall_ v Q))).imp_
      (((forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_ ((forall_ v Q).imp_ (forall_ v P))).imp_
        ((forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_
          (((forall_ v P).imp_ (forall_ v Q)).imp_ ((forall_ v Q).imp_ (forall_ v P)).not_).not_)))
Theorem: FOL.NV.T_18_1
Proof state before:
case a.a
P Q : Formula
v : VarName
⊢ IsDeduct ∅
    (((forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_ ((forall_ v P).imp_ (forall_ v Q))).imp_
      (((forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_ ((forall_ v Q).imp_ (forall_ v P))).imp_
        ((forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_
          (((forall_ v P).imp_ (forall_ v Q)).imp_ ((forall_ v Q).imp_ (forall_ v P)).not_).not_)))
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_18_1
Proof state before:
case a.a
P Q : Formula
v : VarName
⊢ IsDeduct ∅ ((forall_ v (P.iff_ Q)).imp_ ((forall_ v P).imp_ (forall_ v Q)))
Tactic:
apply T_18_1_left
Proof state after:
no goals
Theorem: FOL.NV.T_18_1
Proof state before:
case a
P Q : Formula
v : VarName
⊢ IsDeduct ∅ ((forall_ v (P.iff_ Q)).imp_ ((forall_ v Q).imp_ (forall_ v P)))
Tactic:
apply T_18_1_right
Proof state after:
no goals
Theorem: FOL.NV.Forall_spec_id
Proof state before:
xs : List VarName
P : Formula
⊢ IsProof ((Forall_ xs P).imp_ P)
Tactic:
induction xs
Proof state after:
case nil
P : Formula
⊢ IsProof ((Forall_ [] P).imp_ P)

case cons
P : Formula
head✝ : VarName
tail✝ : List VarName
tail_ih✝ : IsProof ((Forall_ tail✝ P).imp_ P)
⊢ IsProof ((Forall_ (head✝ :: tail✝) P).imp_ P)
Theorem: FOL.NV.Forall_spec_id
Proof state before:
P : Formula
⊢ IsProof ((Forall_ [] P).imp_ P)
Tactic:
case nil =>
  simp only [Forall_]
  apply prop_id
Proof state after:
no goals
Theorem: FOL.NV.Forall_spec_id
Proof state before:
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsProof ((Forall_ (xs_hd :: xs_tl) P).imp_ P)
Tactic:
case cons xs_hd xs_tl xs_ih =>
  simp only [Forall_]
  apply deduction_theorem
  simp
  apply IsDeduct.mp_ (Forall_ xs_tl P)
  apply proof_imp_deduct
  exact xs_ih
  apply specId xs_hd
  apply IsDeduct.assume_
  simp
  rfl
Proof state after:
no goals
Theorem: FOL.NV.Forall_spec_id
Proof state before:
P : Formula
⊢ IsProof ((Forall_ [] P).imp_ P)
Tactic:
simp only [Forall_]
Proof state after:
P : Formula
⊢ IsProof ((List.foldr forall_ P []).imp_ P)
Theorem: FOL.NV.Forall_spec_id
Proof state before:
P : Formula
⊢ IsProof ((List.foldr forall_ P []).imp_ P)
Tactic:
apply prop_id
Proof state after:
no goals
Theorem: FOL.NV.Forall_spec_id
Proof state before:
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsProof ((Forall_ (xs_hd :: xs_tl) P).imp_ P)
Tactic:
simp only [Forall_]
Proof state after:
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsProof ((List.foldr forall_ P (xs_hd :: xs_tl)).imp_ P)
Theorem: FOL.NV.Forall_spec_id
Proof state before:
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsProof ((List.foldr forall_ P (xs_hd :: xs_tl)).imp_ P)
Tactic:
apply deduction_theorem
Proof state after:
case h1
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct (∅ ∪ {List.foldr forall_ P (xs_hd :: xs_tl)}) P
Theorem: FOL.NV.Forall_spec_id
Proof state before:
case h1
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct (∅ ∪ {List.foldr forall_ P (xs_hd :: xs_tl)}) P
Tactic:
simp
Proof state after:
case h1
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} P
Theorem: FOL.NV.Forall_spec_id
Proof state before:
case h1
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} P
Tactic:
apply IsDeduct.mp_ (Forall_ xs_tl P)
Proof state after:
case h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} ((Forall_ xs_tl P).imp_ P)

case h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} (Forall_ xs_tl P)
Theorem: FOL.NV.Forall_spec_id
Proof state before:
case h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} ((Forall_ xs_tl P).imp_ P)

case h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} (Forall_ xs_tl P)
Tactic:
apply proof_imp_deduct
Proof state after:
case h1.a.h1
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsProof ((Forall_ xs_tl P).imp_ P)

case h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} (Forall_ xs_tl P)
Theorem: FOL.NV.Forall_spec_id
Proof state before:
case h1.a.h1
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsProof ((Forall_ xs_tl P).imp_ P)

case h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} (Forall_ xs_tl P)
Tactic:
exact xs_ih
Proof state after:
case h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} (Forall_ xs_tl P)
Theorem: FOL.NV.Forall_spec_id
Proof state before:
case h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} (Forall_ xs_tl P)
Tactic:
apply specId xs_hd
Proof state after:
case h1.a.h1
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} (forall_ xs_hd (Forall_ xs_tl P))
Theorem: FOL.NV.Forall_spec_id
Proof state before:
case h1.a.h1
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} (forall_ xs_hd (Forall_ xs_tl P))
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.a.h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ forall_ xs_hd (Forall_ xs_tl P) ∈ {forall_ xs_hd (List.foldr forall_ P xs_tl)}
Theorem: FOL.NV.Forall_spec_id
Proof state before:
case h1.a.h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ forall_ xs_hd (Forall_ xs_tl P) ∈ {forall_ xs_hd (List.foldr forall_ P xs_tl)}
Tactic:
simp
Proof state after:
case h1.a.h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ Forall_ xs_tl P = List.foldr forall_ P xs_tl
Theorem: FOL.NV.Forall_spec_id
Proof state before:
case h1.a.h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ Forall_ xs_tl P = List.foldr forall_ P xs_tl
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.Forall_spec_id'
Proof state before:
xs : List VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (Forall_ xs P)
⊢ IsDeduct Δ P
Tactic:
induction xs
Proof state after:
case nil
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (Forall_ [] P)
⊢ IsDeduct Δ P

case cons
P : Formula
Δ : Set Formula
head✝ : VarName
tail✝ : List VarName
tail_ih✝ : IsDeduct Δ (Forall_ tail✝ P) → IsDeduct Δ P
h1 : IsDeduct Δ (Forall_ (head✝ :: tail✝) P)
⊢ IsDeduct Δ P
Theorem: FOL.NV.Forall_spec_id'
Proof state before:
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (Forall_ [] P)
⊢ IsDeduct Δ P
Tactic:
case nil =>
  simp only [Forall_] at h1
  simp at h1
  exact h1
Proof state after:
no goals
Theorem: FOL.NV.Forall_spec_id'
Proof state before:
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (Forall_ (xs_hd :: xs_tl) P)
⊢ IsDeduct Δ P
Tactic:
case cons xs_hd xs_tl xs_ih =>
  simp only [Forall_] at h1
  simp at h1
  apply xs_ih
  simp only [Forall_]
  apply specId xs_hd
  exact h1
Proof state after:
no goals
Theorem: FOL.NV.Forall_spec_id'
Proof state before:
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (Forall_ [] P)
⊢ IsDeduct Δ P
Tactic:
simp only [Forall_] at h1
Proof state after:
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (List.foldr forall_ P [])
⊢ IsDeduct Δ P
Theorem: FOL.NV.Forall_spec_id'
Proof state before:
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (List.foldr forall_ P [])
⊢ IsDeduct Δ P
Tactic:
simp at h1
Proof state after:
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ P
⊢ IsDeduct Δ P
Theorem: FOL.NV.Forall_spec_id'
Proof state before:
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ P
⊢ IsDeduct Δ P
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.Forall_spec_id'
Proof state before:
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (Forall_ (xs_hd :: xs_tl) P)
⊢ IsDeduct Δ P
Tactic:
simp only [Forall_] at h1
Proof state after:
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (List.foldr forall_ P (xs_hd :: xs_tl))
⊢ IsDeduct Δ P
Theorem: FOL.NV.Forall_spec_id'
Proof state before:
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (List.foldr forall_ P (xs_hd :: xs_tl))
⊢ IsDeduct Δ P
Tactic:
simp at h1
Proof state after:
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (forall_ xs_hd (List.foldr forall_ P xs_tl))
⊢ IsDeduct Δ P
Theorem: FOL.NV.Forall_spec_id'
Proof state before:
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (forall_ xs_hd (List.foldr forall_ P xs_tl))
⊢ IsDeduct Δ P
Tactic:
apply xs_ih
Proof state after:
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (forall_ xs_hd (List.foldr forall_ P xs_tl))
⊢ IsDeduct Δ (Forall_ xs_tl P)
Theorem: FOL.NV.Forall_spec_id'
Proof state before:
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (forall_ xs_hd (List.foldr forall_ P xs_tl))
⊢ IsDeduct Δ (Forall_ xs_tl P)
Tactic:
simp only [Forall_]
Proof state after:
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (forall_ xs_hd (List.foldr forall_ P xs_tl))
⊢ IsDeduct Δ (List.foldr forall_ P xs_tl)
Theorem: FOL.NV.Forall_spec_id'
Proof state before:
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (forall_ xs_hd (List.foldr forall_ P xs_tl))
⊢ IsDeduct Δ (List.foldr forall_ P xs_tl)
Tactic:
apply specId xs_hd
Proof state after:
case h1
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (forall_ xs_hd (List.foldr forall_ P xs_tl))
⊢ IsDeduct Δ (forall_ xs_hd (List.foldr forall_ P xs_tl))
Theorem: FOL.NV.Forall_spec_id'
Proof state before:
case h1
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (forall_ xs_hd (List.foldr forall_ P xs_tl))
⊢ IsDeduct Δ (forall_ xs_hd (List.foldr forall_ P xs_tl))
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.Forall_isBoundIn
Proof state before:
P : Formula
xs : List VarName
x : VarName
⊢ isBoundIn x (Forall_ xs P) ↔ x ∈ xs ∨ isBoundIn x P
Tactic:
simp only [Formula.Forall_]
Proof state after:
P : Formula
xs : List VarName
x : VarName
⊢ isBoundIn x (List.foldr forall_ P xs) ↔ x ∈ xs ∨ isBoundIn x P
Theorem: FOL.NV.Forall_isBoundIn
Proof state before:
P : Formula
xs : List VarName
x : VarName
⊢ isBoundIn x (List.foldr forall_ P xs) ↔ x ∈ xs ∨ isBoundIn x P
Tactic:
induction xs
Proof state after:
case nil
P : Formula
x : VarName
⊢ isBoundIn x (List.foldr forall_ P []) ↔ x ∈ [] ∨ isBoundIn x P

case cons
P : Formula
x head✝ : VarName
tail✝ : List VarName
tail_ih✝ : isBoundIn x (List.foldr forall_ P tail✝) ↔ x ∈ tail✝ ∨ isBoundIn x P
⊢ isBoundIn x (List.foldr forall_ P (head✝ :: tail✝)) ↔ x ∈ head✝ :: tail✝ ∨ isBoundIn x P
Theorem: FOL.NV.Forall_isBoundIn
Proof state before:
P : Formula
x : VarName
⊢ isBoundIn x (List.foldr forall_ P []) ↔ x ∈ [] ∨ isBoundIn x P
Tactic:
case nil =>
  simp
Proof state after:
no goals
Theorem: FOL.NV.Forall_isBoundIn
Proof state before:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isBoundIn x (List.foldr forall_ P xs_tl) ↔ x ∈ xs_tl ∨ isBoundIn x P
⊢ isBoundIn x (List.foldr forall_ P (xs_hd :: xs_tl)) ↔ x ∈ xs_hd :: xs_tl ∨ isBoundIn x P
Tactic:
case cons xs_hd xs_tl xs_ih =>
  simp
  simp only [isBoundIn]
  simp only [xs_ih]
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Forall_isBoundIn
Proof state before:
P : Formula
x : VarName
⊢ isBoundIn x (List.foldr forall_ P []) ↔ x ∈ [] ∨ isBoundIn x P
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Forall_isBoundIn
Proof state before:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isBoundIn x (List.foldr forall_ P xs_tl) ↔ x ∈ xs_tl ∨ isBoundIn x P
⊢ isBoundIn x (List.foldr forall_ P (xs_hd :: xs_tl)) ↔ x ∈ xs_hd :: xs_tl ∨ isBoundIn x P
Tactic:
simp
Proof state after:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isBoundIn x (List.foldr forall_ P xs_tl) ↔ x ∈ xs_tl ∨ isBoundIn x P
⊢ isBoundIn x (forall_ xs_hd (List.foldr forall_ P xs_tl)) ↔ (x = xs_hd ∨ x ∈ xs_tl) ∨ isBoundIn x P
Theorem: FOL.NV.Forall_isBoundIn
Proof state before:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isBoundIn x (List.foldr forall_ P xs_tl) ↔ x ∈ xs_tl ∨ isBoundIn x P
⊢ isBoundIn x (forall_ xs_hd (List.foldr forall_ P xs_tl)) ↔ (x = xs_hd ∨ x ∈ xs_tl) ∨ isBoundIn x P
Tactic:
simp only [isBoundIn]
Proof state after:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isBoundIn x (List.foldr forall_ P xs_tl) ↔ x ∈ xs_tl ∨ isBoundIn x P
⊢ x = xs_hd ∨ isBoundIn x (List.foldr forall_ P xs_tl) ↔ (x = xs_hd ∨ x ∈ xs_tl) ∨ isBoundIn x P
Theorem: FOL.NV.Forall_isBoundIn
Proof state before:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isBoundIn x (List.foldr forall_ P xs_tl) ↔ x ∈ xs_tl ∨ isBoundIn x P
⊢ x = xs_hd ∨ isBoundIn x (List.foldr forall_ P xs_tl) ↔ (x = xs_hd ∨ x ∈ xs_tl) ∨ isBoundIn x P
Tactic:
simp only [xs_ih]
Proof state after:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isBoundIn x (List.foldr forall_ P xs_tl) ↔ x ∈ xs_tl ∨ isBoundIn x P
⊢ x = xs_hd ∨ x ∈ xs_tl ∨ isBoundIn x P ↔ (x = xs_hd ∨ x ∈ xs_tl) ∨ isBoundIn x P
Theorem: FOL.NV.Forall_isBoundIn
Proof state before:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isBoundIn x (List.foldr forall_ P xs_tl) ↔ x ∈ xs_tl ∨ isBoundIn x P
⊢ x = xs_hd ∨ x ∈ xs_tl ∨ isBoundIn x P ↔ (x = xs_hd ∨ x ∈ xs_tl) ∨ isBoundIn x P
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Forall_isFreeIn
Proof state before:
P : Formula
xs : List VarName
x : VarName
⊢ isFreeIn x (Forall_ xs P) ↔ x ∉ xs ∧ isFreeIn x P
Tactic:
simp only [Formula.Forall_]
Proof state after:
P : Formula
xs : List VarName
x : VarName
⊢ isFreeIn x (List.foldr forall_ P xs) ↔ x ∉ xs ∧ isFreeIn x P
Theorem: FOL.NV.Forall_isFreeIn
Proof state before:
P : Formula
xs : List VarName
x : VarName
⊢ isFreeIn x (List.foldr forall_ P xs) ↔ x ∉ xs ∧ isFreeIn x P
Tactic:
induction xs
Proof state after:
case nil
P : Formula
x : VarName
⊢ isFreeIn x (List.foldr forall_ P []) ↔ x ∉ [] ∧ isFreeIn x P

case cons
P : Formula
x head✝ : VarName
tail✝ : List VarName
tail_ih✝ : isFreeIn x (List.foldr forall_ P tail✝) ↔ x ∉ tail✝ ∧ isFreeIn x P
⊢ isFreeIn x (List.foldr forall_ P (head✝ :: tail✝)) ↔ x ∉ head✝ :: tail✝ ∧ isFreeIn x P
Theorem: FOL.NV.Forall_isFreeIn
Proof state before:
P : Formula
x : VarName
⊢ isFreeIn x (List.foldr forall_ P []) ↔ x ∉ [] ∧ isFreeIn x P
Tactic:
case nil =>
  simp
Proof state after:
no goals
Theorem: FOL.NV.Forall_isFreeIn
Proof state before:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isFreeIn x (List.foldr forall_ P xs_tl) ↔ x ∉ xs_tl ∧ isFreeIn x P
⊢ isFreeIn x (List.foldr forall_ P (xs_hd :: xs_tl)) ↔ x ∉ xs_hd :: xs_tl ∧ isFreeIn x P
Tactic:
case cons xs_hd xs_tl xs_ih =>
  simp
  simp only [isFreeIn]
  simp only [xs_ih]
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Forall_isFreeIn
Proof state before:
P : Formula
x : VarName
⊢ isFreeIn x (List.foldr forall_ P []) ↔ x ∉ [] ∧ isFreeIn x P
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Forall_isFreeIn
Proof state before:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isFreeIn x (List.foldr forall_ P xs_tl) ↔ x ∉ xs_tl ∧ isFreeIn x P
⊢ isFreeIn x (List.foldr forall_ P (xs_hd :: xs_tl)) ↔ x ∉ xs_hd :: xs_tl ∧ isFreeIn x P
Tactic:
simp
Proof state after:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isFreeIn x (List.foldr forall_ P xs_tl) ↔ x ∉ xs_tl ∧ isFreeIn x P
⊢ isFreeIn x (forall_ xs_hd (List.foldr forall_ P xs_tl)) ↔ (¬x = xs_hd ∧ x ∉ xs_tl) ∧ isFreeIn x P
Theorem: FOL.NV.Forall_isFreeIn
Proof state before:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isFreeIn x (List.foldr forall_ P xs_tl) ↔ x ∉ xs_tl ∧ isFreeIn x P
⊢ isFreeIn x (forall_ xs_hd (List.foldr forall_ P xs_tl)) ↔ (¬x = xs_hd ∧ x ∉ xs_tl) ∧ isFreeIn x P
Tactic:
simp only [isFreeIn]
Proof state after:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isFreeIn x (List.foldr forall_ P xs_tl) ↔ x ∉ xs_tl ∧ isFreeIn x P
⊢ ¬x = xs_hd ∧ isFreeIn x (List.foldr forall_ P xs_tl) ↔ (¬x = xs_hd ∧ x ∉ xs_tl) ∧ isFreeIn x P
Theorem: FOL.NV.Forall_isFreeIn
Proof state before:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isFreeIn x (List.foldr forall_ P xs_tl) ↔ x ∉ xs_tl ∧ isFreeIn x P
⊢ ¬x = xs_hd ∧ isFreeIn x (List.foldr forall_ P xs_tl) ↔ (¬x = xs_hd ∧ x ∉ xs_tl) ∧ isFreeIn x P
Tactic:
simp only [xs_ih]
Proof state after:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isFreeIn x (List.foldr forall_ P xs_tl) ↔ x ∉ xs_tl ∧ isFreeIn x P
⊢ ¬x = xs_hd ∧ x ∉ xs_tl ∧ isFreeIn x P ↔ (¬x = xs_hd ∧ x ∉ xs_tl) ∧ isFreeIn x P