internlm/Lean-Github huggingface dataset:
Theorem: triple_step
Proof state before:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : kl = triple.pivot
⊢ Vector.get' left kl llt = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
Tactic:
apply witness_independent
Proof state after:
case a
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : kl = triple.pivot
⊢ kl = triple.pivot
Theorem: triple_step
Proof state before:
case a
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : kl = triple.pivot
⊢ kl = triple.pivot
Tactic:
apply cc
Proof state after:
no goals
Theorem: triple_step
Proof state before:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : kl = triple.pivot
lem1 : Vector.get' left kl llt = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
⊢ Vector.get' valuation kl llt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
Tactic:
apply witness_independent
Proof state after:
case a
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : kl = triple.pivot
lem1 : Vector.get' left kl llt = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
⊢ kl = triple.pivot
Theorem: triple_step
Proof state before:
case a
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : kl = triple.pivot
lem1 : Vector.get' left kl llt = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
⊢ kl = triple.pivot
Tactic:
apply cc
Proof state after:
no goals
Theorem: triple_step
Proof state before:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : kl = triple.pivot
lem1 : Vector.get left { val := kl, isLt := llt } = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kl llt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
⊢ some true = some false
Tactic:
rw [← c, ← lem2, Vector.get', ← wl, lem1, triple.leftPivot]
Proof state after:
no goals
Theorem: triple_step
Proof state before:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : ¬kl = triple.pivot
i : ℕ := skipInverse triple.pivot kl cc
eql : skip triple.pivot (skipInverse triple.pivot kl cc) = kl := skipInverse_eq triple.pivot kl cc
iw : i < n := skip_preimage_lt triple.pivotLt llt eql
⊢ Vector.get' left kl llt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1)
Tactic:
apply witness_independent
Proof state after:
case a
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : ¬kl = triple.pivot
i : ℕ := skipInverse triple.pivot kl cc
eql : skip triple.pivot (skipInverse triple.pivot kl cc) = kl := skipInverse_eq triple.pivot kl cc
iw : i < n := skip_preimage_lt triple.pivotLt llt eql
⊢ kl = skip triple.pivot i
Theorem: triple_step
Proof state before:
case a
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : ¬kl = triple.pivot
i : ℕ := skipInverse triple.pivot kl cc
eql : skip triple.pivot (skipInverse triple.pivot kl cc) = kl := skipInverse_eq triple.pivot kl cc
iw : i < n := skip_preimage_lt triple.pivotLt llt eql
⊢ kl = skip triple.pivot i
Tactic:
rw [← eql]
Proof state after:
no goals
Theorem: triple_step
Proof state before:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : ¬kl = triple.pivot
i : ℕ := skipInverse triple.pivot kl cc
eql : skip triple.pivot (skipInverse triple.pivot kl cc) = kl := skipInverse_eq triple.pivot kl cc
iw : i < n := skip_preimage_lt triple.pivotLt llt eql
leftLem : Vector.get' left kl llt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' left kl) kl (skip triple.pivot i) llt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kl cc))))
⊢ Vector.get' right kl llt = Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1)
Tactic:
apply witness_independent
Proof state after:
case a
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : ¬kl = triple.pivot
i : ℕ := skipInverse triple.pivot kl cc
eql : skip triple.pivot (skipInverse triple.pivot kl cc) = kl := skipInverse_eq triple.pivot kl cc
iw : i < n := skip_preimage_lt triple.pivotLt llt eql
leftLem : Vector.get' left kl llt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' left kl) kl (skip triple.pivot i) llt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kl cc))))
⊢ kl = skip triple.pivot i
Theorem: triple_step
Proof state before:
case a
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : ¬kl = triple.pivot
i : ℕ := skipInverse triple.pivot kl cc
eql : skip triple.pivot (skipInverse triple.pivot kl cc) = kl := skipInverse_eq triple.pivot kl cc
iw : i < n := skip_preimage_lt triple.pivotLt llt eql
leftLem : Vector.get' left kl llt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' left kl) kl (skip triple.pivot i) llt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kl cc))))
⊢ kl = skip triple.pivot i
Tactic:
rw [← eql]
Proof state after:
no goals
Theorem: triple_step
Proof state before:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : ¬kl = triple.pivot
i : ℕ := skipInverse triple.pivot kl cc
eql : skip triple.pivot (skipInverse triple.pivot kl cc) = kl := skipInverse_eq triple.pivot kl cc
iw : i < n := skip_preimage_lt triple.pivotLt llt eql
leftLem : Vector.get' left kl llt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' left kl) kl (skip triple.pivot i) llt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kl cc))))
rightLem : Vector.get' right kl llt = Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' right kl) kl (skip triple.pivot i) llt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kl cc))))
⊢ Vector.get' top kl llt = Vector.get' top (skip triple.pivot i) (_ : skip triple.pivot i < n + 1)
Tactic:
apply witness_independent
Proof state after:
case a
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : ¬kl = triple.pivot
i : ℕ := skipInverse triple.pivot kl cc
eql : skip triple.pivot (skipInverse triple.pivot kl cc) = kl := skipInverse_eq triple.pivot kl cc
iw : i < n := skip_preimage_lt triple.pivotLt llt eql
leftLem : Vector.get' left kl llt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' left kl) kl (skip triple.pivot i) llt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kl cc))))
rightLem : Vector.get' right kl llt = Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' right kl) kl (skip triple.pivot i) llt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kl cc))))
⊢ kl = skip triple.pivot i
Theorem: triple_step
Proof state before:
case a
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : ¬kl = triple.pivot
i : ℕ := skipInverse triple.pivot kl cc
eql : skip triple.pivot (skipInverse triple.pivot kl cc) = kl := skipInverse_eq triple.pivot kl cc
iw : i < n := skip_preimage_lt triple.pivotLt llt eql
leftLem : Vector.get' left kl llt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' left kl) kl (skip triple.pivot i) llt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kl cc))))
rightLem : Vector.get' right kl llt = Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' right kl) kl (skip triple.pivot i) llt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kl cc))))
⊢ kl = skip triple.pivot i
Tactic:
rw [← eql]
Proof state after:
no goals
Theorem: triple_step
Proof state before:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : ¬kl = triple.pivot
i : ℕ := skipInverse triple.pivot kl cc
eql : skip triple.pivot (skipInverse triple.pivot kl cc) = kl := skipInverse_eq triple.pivot kl cc
iw : i < n := skip_preimage_lt triple.pivotLt llt eql
leftLem : Vector.get' left kl llt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' left kl) kl (skip triple.pivot i) llt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kl cc))))
rightLem : Vector.get' right kl llt = Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' right kl) kl (skip triple.pivot i) llt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kl cc))))
topLem : Vector.get' top kl llt = Vector.get' top (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' top kl) kl (skip triple.pivot i) llt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kl cc))))
⊢ IsJoin (Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1))
    (Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1))
    (Vector.get' top (skip triple.pivot i) (_ : skip triple.pivot i < n + 1))
Tactic:
exact triple.joinRest i iw
Proof state after:
no goals
Theorem: triple_step
Proof state before:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : ¬Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : kr = triple.pivot
⊢ ClauseSat top valuation
Tactic:
have lem1 : right.get' kr rlt =
      right.get' triple.pivot triple.pivotLt := by
      apply witness_independent
      apply ccc
Proof state after:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : ¬Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : kr = triple.pivot
lem1 : Vector.get' right kr rlt = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation
Theorem: triple_step
Proof state before:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : ¬Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : kr = triple.pivot
lem1 : Vector.get' right kr rlt = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation
Tactic:
have lem2 : valuation.get' kr rlt =
      valuation.get' triple.pivot triple.pivotLt := by
      apply witness_independent
      apply ccc
Proof state after:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : ¬Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : kr = triple.pivot
lem1 : Vector.get' right kr rlt = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kr rlt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation
Theorem: triple_step
Proof state before:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : ¬Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : kr = triple.pivot
lem1 : Vector.get' right kr rlt = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kr rlt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation
Tactic:
rw [Vector.get'] at lem1
Proof state after:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : ¬Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : kr = triple.pivot
lem1 : Vector.get right { val := kr, isLt := rlt } = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kr rlt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation