internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅
    ((eq_ r s).imp_
      ((eq_ (args_u 0) (args_v 0)).and_
        (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ)))))
Tactic:
apply
  IsDeduct.mp_
    ((eq_ r s).imp_
      (List.foldr and_ true_
        (List.ofFn fun (i : Fin n) => eq_ (args_u i.succ) (args_v i.succ))))
Proof state after:
case a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅
    (((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ)))).imp_
      ((eq_ r s).imp_
        ((eq_ (args_u 0) (args_v 0)).and_
          (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ))))))

case a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ))))
Theorem: FOL.NV.T_21_8
Proof state before:
case a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅
    (((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ)))).imp_
      ((eq_ r s).imp_
        ((eq_ (args_u 0) (args_v 0)).and_
          (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ))))))
Tactic:
apply IsDeduct.mp_ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))
Proof state after:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅
    (((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0))).imp_
      (((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ)))).imp_
        ((eq_ r s).imp_
          ((eq_ (args_u 0) (args_v 0)).and_
            (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ)))))))

case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))
Theorem: FOL.NV.T_21_8
Proof state before:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅
    (((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0))).imp_
      (((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ)))).imp_
        ((eq_ r s).imp_
          ((eq_ (args_u 0) (args_v 0)).and_
            (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ)))))))
Tactic:
simp only [def_and_]
Proof state after:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅
    (((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0))).imp_
      (((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ)))).imp_
        ((eq_ r s).imp_
          ((eq_ (args_u 0) (args_v 0)).imp_
              (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ))).not_).not_)))
Theorem: FOL.NV.T_21_8
Proof state before:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅
    (((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0))).imp_
      (((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ)))).imp_
        ((eq_ r s).imp_
          ((eq_ (args_u 0) (args_v 0)).imp_
              (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ))).not_).not_)))
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof state before:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))
Tactic:
specialize h1_1 0
Proof state after:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : args_u 0 = args_v 0 ∨ args_u 0 = r ∧ args_v 0 = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))
Theorem: FOL.NV.T_21_8
Proof state before:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : args_u 0 = args_v 0 ∨ args_u 0 = r ∧ args_v 0 = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))
Tactic:
cases h1_1
Proof state after:
case a.a.inl
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h✝ : args_u 0 = args_v 0
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))

case a.a.inr
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h✝ : args_u 0 = r ∧ args_v 0 = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))
Tactic:
case _ c1 =>
  apply IsDeduct.mp_ (eq_ (args_u 0) (args_v 0))
  case _ =>
    SC
  case _ =>
    simp only [c1]
    apply specId (args_v 0)
    apply IsDeduct.axiom_
    apply IsAxiom.eq_1_
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = r ∧ args_v 0 = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))
Tactic:
case _ c1 =>
  cases c1
  case _ c1_left c1_right =>
    subst c1_left
    subst c1_right
    SC
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))
Tactic:
apply IsDeduct.mp_ (eq_ (args_u 0) (args_v 0))
Proof state after:
case a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ ((eq_ (args_u 0) (args_v 0)).imp_ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0))))

case a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ (eq_ (args_u 0) (args_v 0))
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ ((eq_ (args_u 0) (args_v 0)).imp_ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0))))
Tactic:
case _ =>
  SC
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ (eq_ (args_u 0) (args_v 0))
Tactic:
case _ =>
  simp only [c1]
  apply specId (args_v 0)
  apply IsDeduct.axiom_
  apply IsAxiom.eq_1_
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ ((eq_ (args_u 0) (args_v 0)).imp_ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0))))
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ (eq_ (args_u 0) (args_v 0))
Tactic:
simp only [c1]
Proof state after:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ (eq_ (args_v 0) (args_v 0))
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ (eq_ (args_v 0) (args_v 0))
Tactic:
apply specId (args_v 0)
Proof state after:
case h1
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ (forall_ (args_v 0) (eq_ (args_v 0) (args_v 0)))
Theorem: FOL.NV.T_21_8
Proof state before:
case h1
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ (forall_ (args_v 0) (eq_ (args_v 0) (args_v 0)))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case h1.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsAxiom (forall_ (args_v 0) (eq_ (args_v 0) (args_v 0)))
Theorem: FOL.NV.T_21_8
Proof state before:
case h1.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsAxiom (forall_ (args_v 0) (eq_ (args_v 0) (args_v 0)))
Tactic:
apply IsAxiom.eq_1_
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = r ∧ args_v 0 = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))
Tactic:
cases c1
Proof state after:
case intro
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
left✝ : args_u 0 = r
right✝ : args_v 0 = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1_left : args_u 0 = r
c1_right : args_v 0 = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))
Tactic:
case _ c1_left c1_right =>
  subst c1_left
  subst c1_right
  SC
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1_left : args_u 0 = r
c1_right : args_v 0 = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))
Tactic:
subst c1_left
Proof state after:
P_r P_s : Formula
s : VarName
name : PredName
n : ℕ
args_u args_v : Fin (n + 1) → VarName
c1_right : args_v 0 = s
ih :
  ∀ (args_u_1 args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u_1 i = args_v i ∨ args_u_1 i = args_u 0 ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ (args_u 0) s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u_1 i) (args_v i))))
⊢ IsDeduct ∅ ((eq_ (args_u 0) s).imp_ (eq_ (args_u 0) (args_v 0)))
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
s : VarName
name : PredName
n : ℕ
args_u args_v : Fin (n + 1) → VarName
c1_right : args_v 0 = s
ih :
  ∀ (args_u_1 args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u_1 i = args_v i ∨ args_u_1 i = args_u 0 ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ (args_u 0) s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u_1 i) (args_v i))))
⊢ IsDeduct ∅ ((eq_ (args_u 0) s).imp_ (eq_ (args_u 0) (args_v 0)))
Tactic:
subst c1_right
Proof state after:
P_r P_s : Formula
name : PredName
n : ℕ
args_u args_v : Fin (n + 1) → VarName
ih :
  ∀ (args_u_1 args_v_1 : Fin n → VarName),
    (∀ (i : Fin n), args_u_1 i = args_v_1 i ∨ args_u_1 i = args_u 0 ∧ args_v_1 i = args_v 0) →
      IsDeduct ∅
        ((eq_ (args_u 0) (args_v 0)).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u_1 i) (args_v_1 i))))
⊢ IsDeduct ∅ ((eq_ (args_u 0) (args_v 0)).imp_ (eq_ (args_u 0) (args_v 0)))
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
name : PredName
n : ℕ
args_u args_v : Fin (n + 1) → VarName
ih :
  ∀ (args_u_1 args_v_1 : Fin n → VarName),
    (∀ (i : Fin n), args_u_1 i = args_v_1 i ∨ args_u_1 i = args_u 0 ∧ args_v_1 i = args_v 0) →
      IsDeduct ∅
        ((eq_ (args_u 0) (args_v 0)).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u_1 i) (args_v_1 i))))
⊢ IsDeduct ∅ ((eq_ (args_u 0) (args_v 0)).imp_ (eq_ (args_u 0) (args_v 0)))
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof state before:
case a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ))))
Tactic:
apply ih
Proof state after:
case a.h1_1
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ ∀ (i : Fin n), args_u i.succ = args_v i.succ ∨ args_u i.succ = r ∧ args_v i.succ = s
Theorem: FOL.NV.T_21_8
Proof state before:
case a.h1_1
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ ∀ (i : Fin n), args_u i.succ = args_v i.succ ∨ args_u i.succ = r ∧ args_v i.succ = s
Tactic:
intro i
Proof state after:
case a.h1_1
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
i : Fin n
⊢ args_u i.succ = args_v i.succ ∨ args_u i.succ = r ∧ args_v i.succ = s
Theorem: FOL.NV.T_21_8
Proof state before:
case a.h1_1
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
i : Fin n
⊢ args_u i.succ = args_v i.succ ∨ args_u i.succ = r ∧ args_v i.succ = s
Tactic:
apply h1_1
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2 : ¬isBoundIn r P_u.not_
h3 : ¬isBoundIn s P_u.not_
⊢ IsProof ((eq_ r s).imp_ (P_u.not_.iff_ P_v.not_))
Tactic:
simp only [isBoundIn] at h2
Proof state after:
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u.not_
⊢ IsProof ((eq_ r s).imp_ (P_u.not_.iff_ P_v.not_))
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u.not_
⊢ IsProof ((eq_ r s).imp_ (P_u.not_.iff_ P_v.not_))
Tactic:
simp only [isBoundIn] at h3
Proof state after:
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
⊢ IsProof ((eq_ r s).imp_ (P_u.not_.iff_ P_v.not_))