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 kl llt) (Vector.get' right kl llt) (Vector.get' top kl llt)
Tactic:
rw [leftLem, rightLem, topLem]
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 : ¬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))