internlm/Lean-Github huggingface dataset:
Theorem: resolutionToProof
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
top✝ : Clause (n + 1)
j : ℕ
jw : j < num_clauses
top : Clause (n + 1)
eqn : Vector.get' clauses j jw = top
valuation : Valuation (n + 1)
base : ∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation
⊢ ClauseSat (Vector.get' clauses j jw) valuation
Tactic:
apply base
Proof state after:
no goals
Theorem: resolutionToProof
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
top left right top' : Clause (n + 1)
leftTree✝ : ResolutionTree clauses left
rightTree✝ : ResolutionTree clauses right
triple : ResolutionTriple left right top'
lih :
  ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat left valuation
rih :
  ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat right valuation
⊢ ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat top' valuation
Tactic:
intro valuation base
Proof state after:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
top left right top' : Clause (n + 1)
leftTree✝ : ResolutionTree clauses left
rightTree✝ : ResolutionTree clauses right
triple : ResolutionTriple left right top'
lih :
  ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat left valuation
rih :
  ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat right valuation
valuation : Valuation (n + 1)
base : ∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation
⊢ ClauseSat top' valuation
Theorem: resolutionToProof
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
top left right top' : Clause (n + 1)
leftTree✝ : ResolutionTree clauses left
rightTree✝ : ResolutionTree clauses right
triple : ResolutionTriple left right top'
lih :
  ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat left valuation
rih :
  ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat right valuation
valuation : Valuation (n + 1)
base : ∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation
⊢ ClauseSat top' valuation
Tactic:
let leftBase : ClauseSat left valuation := by
  apply lih valuation base
Proof state after:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
top left right top' : Clause (n + 1)
leftTree✝ : ResolutionTree clauses left
rightTree✝ : ResolutionTree clauses right
triple : ResolutionTriple left right top'
lih :
  ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat left valuation
rih :
  ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat right valuation
valuation : Valuation (n + 1)
base : ∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation
leftBase : ClauseSat left valuation := lih valuation base
⊢ ClauseSat top' valuation
Theorem: resolutionToProof
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
top left right top' : Clause (n + 1)
leftTree✝ : ResolutionTree clauses left
rightTree✝ : ResolutionTree clauses right
triple : ResolutionTriple left right top'
lih :
  ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat left valuation
rih :
  ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat right valuation
valuation : Valuation (n + 1)
base : ∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation
leftBase : ClauseSat left valuation := lih valuation base
⊢ ClauseSat top' valuation
Tactic:
let rightBase : ClauseSat right valuation := by
  apply rih valuation base
Proof state after:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
top left right top' : Clause (n + 1)
leftTree✝ : ResolutionTree clauses left
rightTree✝ : ResolutionTree clauses right
triple : ResolutionTriple left right top'
lih :
  ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat left valuation
rih :
  ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat right valuation
valuation : Valuation (n + 1)
base : ∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation
leftBase : ClauseSat left valuation := lih valuation base
rightBase : ClauseSat right valuation := rih valuation base
⊢ ClauseSat top' valuation
Theorem: resolutionToProof
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
top left right top' : Clause (n + 1)
leftTree✝ : ResolutionTree clauses left
rightTree✝ : ResolutionTree clauses right
triple : ResolutionTriple left right top'
lih :
  ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat left valuation
rih :
  ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat right valuation
valuation : Valuation (n + 1)
base : ∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation
leftBase : ClauseSat left valuation := lih valuation base
rightBase : ClauseSat right valuation := rih valuation base
⊢ ClauseSat top' valuation
Tactic:
exact triple_step left right top' triple valuation leftBase rightBase
Proof state after:
no goals
Theorem: resolutionToProof
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
top left right top' : Clause (n + 1)
leftTree✝ : ResolutionTree clauses left
rightTree✝ : ResolutionTree clauses right
triple : ResolutionTriple left right top'
lih :
  ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat left valuation
rih :
  ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat right valuation
valuation : Valuation (n + 1)
base : ∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation
⊢ ClauseSat left valuation
Tactic:
apply lih valuation base
Proof state after:
no goals
Theorem: resolutionToProof
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
top left right top' : Clause (n + 1)
leftTree✝ : ResolutionTree clauses left
rightTree✝ : ResolutionTree clauses right
triple : ResolutionTriple left right top'
lih :
  ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat left valuation
rih :
  ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat right valuation
valuation : Valuation (n + 1)
base : ∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation
leftBase : ClauseSat left valuation := lih valuation base
⊢ ClauseSat right valuation
Tactic:
apply rih valuation base
Proof state after:
no goals
Theorem: trees_preserve_notsomebranch
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
bf : Bool
k : ℕ
kw : k < n + 1
base : ∀ (j : ℕ) (lt : j < num_clauses), ¬Vector.get' (Vector.get' clauses j lt) k kw = some bf
top : Clause (n + 1)
tree : ResolutionTree clauses top
ind : ℕ
bd : ind < num_clauses
chk : Vector.get' clauses ind bd = top
hyp : Vector.get' top k kw = some bf
⊢ False
Tactic:
have lem1 : Not (top.get' k kw = some bf) := by
        rw [←  chk]
        exact (base ind bd)
Proof state after:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
bf : Bool
k : ℕ
kw : k < n + 1
base : ∀ (j : ℕ) (lt : j < num_clauses), ¬Vector.get' (Vector.get' clauses j lt) k kw = some bf
top : Clause (n + 1)
tree : ResolutionTree clauses top
ind : ℕ
bd : ind < num_clauses
chk : Vector.get' clauses ind bd = top
hyp : Vector.get' top k kw = some bf
lem1 : ¬Vector.get' top k kw = some bf
⊢ False
Theorem: trees_preserve_notsomebranch
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
bf : Bool
k : ℕ
kw : k < n + 1
base : ∀ (j : ℕ) (lt : j < num_clauses), ¬Vector.get' (Vector.get' clauses j lt) k kw = some bf
top : Clause (n + 1)
tree : ResolutionTree clauses top
ind : ℕ
bd : ind < num_clauses
chk : Vector.get' clauses ind bd = top
hyp : Vector.get' top k kw = some bf
lem1 : ¬Vector.get' top k kw = some bf
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: trees_preserve_notsomebranch
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
bf : Bool
k : ℕ
kw : k < n + 1
base : ∀ (j : ℕ) (lt : j < num_clauses), ¬Vector.get' (Vector.get' clauses j lt) k kw = some bf
top : Clause (n + 1)
tree : ResolutionTree clauses top
ind : ℕ
bd : ind < num_clauses
chk : Vector.get' clauses ind bd = top
hyp : Vector.get' top k kw = some bf
⊢ ¬Vector.get' top k kw = some bf
Tactic:
rw [←  chk]
Proof state after:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
bf : Bool
k : ℕ
kw : k < n + 1
base : ∀ (j : ℕ) (lt : j < num_clauses), ¬Vector.get' (Vector.get' clauses j lt) k kw = some bf
top : Clause (n + 1)
tree : ResolutionTree clauses top
ind : ℕ
bd : ind < num_clauses
chk : Vector.get' clauses ind bd = top
hyp : Vector.get' top k kw = some bf
⊢ ¬Vector.get' (Vector.get' clauses ind bd) k kw = some bf
Theorem: trees_preserve_notsomebranch
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
bf : Bool
k : ℕ
kw : k < n + 1
base : ∀ (j : ℕ) (lt : j < num_clauses), ¬Vector.get' (Vector.get' clauses j lt) k kw = some bf
top : Clause (n + 1)
tree : ResolutionTree clauses top
ind : ℕ
bd : ind < num_clauses
chk : Vector.get' clauses ind bd = top
hyp : Vector.get' top k kw = some bf
⊢ ¬Vector.get' (Vector.get' clauses ind bd) k kw = some bf
Tactic:
exact (base ind bd)
Proof state after:
no goals
Theorem: trees_preserve_notsomebranch
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
bf : Bool
k : ℕ
kw : k < n + 1
base : ∀ (j : ℕ) (lt : j < num_clauses), ¬Vector.get' (Vector.get' clauses j lt) k kw = some bf
top : Clause (n + 1)
tree : ResolutionTree clauses top
left right : Clause (n + 1)
leftTree : ResolutionTree clauses left
rightTree : ResolutionTree clauses right
triple : ResolutionTriple left right top
hyp : Vector.get' top k kw = some bf
leftLem : ¬Vector.get' left k kw = some bf := trees_preserve_notsomebranch bf k kw base left leftTree
rightLem : ¬Vector.get' right k kw = some bf := trees_preserve_notsomebranch bf k kw base right rightTree
c : ¬k = triple.pivot
⊢ False
Tactic:
let j := skipInverse triple.pivot k c
Proof state after:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
bf : Bool
k : ℕ
kw : k < n + 1
base : ∀ (j : ℕ) (lt : j < num_clauses), ¬Vector.get' (Vector.get' clauses j lt) k kw = some bf
top : Clause (n + 1)
tree : ResolutionTree clauses top
left right : Clause (n + 1)
leftTree : ResolutionTree clauses left
rightTree : ResolutionTree clauses right
triple : ResolutionTriple left right top
hyp : Vector.get' top k kw = some bf
leftLem : ¬Vector.get' left k kw = some bf := trees_preserve_notsomebranch bf k kw base left leftTree
rightLem : ¬Vector.get' right k kw = some bf := trees_preserve_notsomebranch bf k kw base right rightTree
c : ¬k = triple.pivot
j : ℕ := skipInverse triple.pivot k c
⊢ False
Theorem: trees_preserve_notsomebranch
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
bf : Bool
k : ℕ
kw : k < n + 1
base : ∀ (j : ℕ) (lt : j < num_clauses), ¬Vector.get' (Vector.get' clauses j lt) k kw = some bf
top : Clause (n + 1)
tree : ResolutionTree clauses top
left right : Clause (n + 1)
leftTree : ResolutionTree clauses left
rightTree : ResolutionTree clauses right
triple : ResolutionTriple left right top
hyp : Vector.get' top k kw = some bf
leftLem : ¬Vector.get' left k kw = some bf := trees_preserve_notsomebranch bf k kw base left leftTree
rightLem : ¬Vector.get' right k kw = some bf := trees_preserve_notsomebranch bf k kw base right rightTree
c : ¬k = triple.pivot
j : ℕ := skipInverse triple.pivot k c
⊢ False
Tactic:
let eqn  := skipInverse_eq triple.pivot k c
Proof state after:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
bf : Bool
k : ℕ
kw : k < n + 1
base : ∀ (j : ℕ) (lt : j < num_clauses), ¬Vector.get' (Vector.get' clauses j lt) k kw = some bf
top : Clause (n + 1)
tree : ResolutionTree clauses top
left right : Clause (n + 1)
leftTree : ResolutionTree clauses left
rightTree : ResolutionTree clauses right
triple : ResolutionTriple left right top
hyp : Vector.get' top k kw = some bf
leftLem : ¬Vector.get' left k kw = some bf := trees_preserve_notsomebranch bf k kw base left leftTree
rightLem : ¬Vector.get' right k kw = some bf := trees_preserve_notsomebranch bf k kw base right rightTree
c : ¬k = triple.pivot
j : ℕ := skipInverse triple.pivot k c
eqn : skip triple.pivot (skipInverse triple.pivot k c) = k := skipInverse_eq triple.pivot k c
⊢ False
Theorem: trees_preserve_notsomebranch
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
bf : Bool
k : ℕ
kw : k < n + 1
base : ∀ (j : ℕ) (lt : j < num_clauses), ¬Vector.get' (Vector.get' clauses j lt) k kw = some bf
top : Clause (n + 1)
tree : ResolutionTree clauses top
left right : Clause (n + 1)
leftTree : ResolutionTree clauses left
rightTree : ResolutionTree clauses right
triple : ResolutionTriple left right top
hyp : Vector.get' top k kw = some bf
leftLem : ¬Vector.get' left k kw = some bf := trees_preserve_notsomebranch bf k kw base left leftTree
rightLem : ¬Vector.get' right k kw = some bf := trees_preserve_notsomebranch bf k kw base right rightTree
c : ¬k = triple.pivot
j : ℕ := skipInverse triple.pivot k c
eqn : skip triple.pivot (skipInverse triple.pivot k c) = k := skipInverse_eq triple.pivot k c
⊢ False
Tactic:
let jw := skip_preimage_lt triple.pivotLt kw eqn
Proof state after:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
bf : Bool
k : ℕ
kw : k < n + 1
base : ∀ (j : ℕ) (lt : j < num_clauses), ¬Vector.get' (Vector.get' clauses j lt) k kw = some bf
top : Clause (n + 1)
tree : ResolutionTree clauses top
left right : Clause (n + 1)
leftTree : ResolutionTree clauses left
rightTree : ResolutionTree clauses right
triple : ResolutionTriple left right top
hyp : Vector.get' top k kw = some bf
leftLem : ¬Vector.get' left k kw = some bf := trees_preserve_notsomebranch bf k kw base left leftTree
rightLem : ¬Vector.get' right k kw = some bf := trees_preserve_notsomebranch bf k kw base right rightTree
c : ¬k = triple.pivot
j : ℕ := skipInverse triple.pivot k c
eqn : skip triple.pivot (skipInverse triple.pivot k c) = k := skipInverse_eq triple.pivot k c
jw : skipInverse triple.pivot k c < n := skip_preimage_lt triple.pivotLt kw eqn
⊢ False
Theorem: trees_preserve_notsomebranch
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
bf : Bool
k : ℕ
kw : k < n + 1
base : ∀ (j : ℕ) (lt : j < num_clauses), ¬Vector.get' (Vector.get' clauses j lt) k kw = some bf
top : Clause (n + 1)
tree : ResolutionTree clauses top
left right : Clause (n + 1)
leftTree : ResolutionTree clauses left
rightTree : ResolutionTree clauses right
triple : ResolutionTriple left right top
hyp : Vector.get' top k kw = some bf
leftLem : ¬Vector.get' left k kw = some bf := trees_preserve_notsomebranch bf k kw base left leftTree
rightLem : ¬Vector.get' right k kw = some bf := trees_preserve_notsomebranch bf k kw base right rightTree
c : ¬k = triple.pivot
j : ℕ := skipInverse triple.pivot k c
eqn : skip triple.pivot (skipInverse triple.pivot k c) = k := skipInverse_eq triple.pivot k c
jw : skipInverse triple.pivot k c < n := skip_preimage_lt triple.pivotLt kw eqn
⊢ False
Tactic:
let joinIm := triple.joinRest j jw
Proof state after:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
bf : Bool
k : ℕ
kw : k < n + 1
base : ∀ (j : ℕ) (lt : j < num_clauses), ¬Vector.get' (Vector.get' clauses j lt) k kw = some bf
top : Clause (n + 1)
tree : ResolutionTree clauses top
left right : Clause (n + 1)
leftTree : ResolutionTree clauses left
rightTree : ResolutionTree clauses right
triple : ResolutionTriple left right top
hyp : Vector.get' top k kw = some bf
leftLem : ¬Vector.get' left k kw = some bf := trees_preserve_notsomebranch bf k kw base left leftTree
rightLem : ¬Vector.get' right k kw = some bf := trees_preserve_notsomebranch bf k kw base right rightTree
c : ¬k = triple.pivot
j : ℕ := skipInverse triple.pivot k c
eqn : skip triple.pivot (skipInverse triple.pivot k c) = k := skipInverse_eq triple.pivot k c
jw : skipInverse triple.pivot k c < n := skip_preimage_lt triple.pivotLt kw eqn
joinIm : IsJoin (Vector.get' left (skip triple.pivot j) (_ : skip triple.pivot j < n + 1))
  (Vector.get' right (skip triple.pivot j) (_ : skip triple.pivot j < n + 1))
  (Vector.get' top (skip triple.pivot j) (_ : skip triple.pivot j < n + 1)) :=
  triple.joinRest j jw
⊢ False
Theorem: trees_preserve_notsomebranch
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
bf : Bool
k : ℕ
kw : k < n + 1
base : ∀ (j : ℕ) (lt : j < num_clauses), ¬Vector.get' (Vector.get' clauses j lt) k kw = some bf
top : Clause (n + 1)
tree : ResolutionTree clauses top
left right : Clause (n + 1)
leftTree : ResolutionTree clauses left
rightTree : ResolutionTree clauses right
triple : ResolutionTriple left right top
hyp : Vector.get' top k kw = some bf
leftLem : ¬Vector.get' left k kw = some bf := trees_preserve_notsomebranch bf k kw base left leftTree
rightLem : ¬Vector.get' right k kw = some bf := trees_preserve_notsomebranch bf k kw base right rightTree
c : ¬k = triple.pivot
j : ℕ := skipInverse triple.pivot k c
eqn : skip triple.pivot (skipInverse triple.pivot k c) = k := skipInverse_eq triple.pivot k c
jw : skipInverse triple.pivot k c < n := skip_preimage_lt triple.pivotLt kw eqn
joinIm : IsJoin (Vector.get' left (skip triple.pivot j) (_ : skip triple.pivot j < n + 1))
  (Vector.get' right (skip triple.pivot j) (_ : skip triple.pivot j < n + 1))
  (Vector.get' top (skip triple.pivot j) (_ : skip triple.pivot j < n + 1)) :=
  triple.joinRest j jw
⊢ False
Tactic:
match (skip triple.pivot j), eqn, (skip_le_succ jw), joinIm with
| .(k), rfl, .(kw), join =>
  apply top_of_join_not_positive bf
      (left.get' k kw) (right.get' k kw) (top.get' k kw) join
        leftLem rightLem
  exact hyp
Proof state after:
no goals
Theorem: trees_preserve_notsomebranch
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
bf : Bool
k : ℕ
kw : k < n + 1
base : ∀ (j : ℕ) (lt : j < num_clauses), ¬Vector.get' (Vector.get' clauses j lt) k kw = some bf
top : Clause (n + 1)
tree : ResolutionTree clauses top
left right : Clause (n + 1)
leftTree : ResolutionTree clauses left
rightTree : ResolutionTree clauses right
triple : ResolutionTriple left right top
hyp : Vector.get' top k kw = some bf
leftLem : ¬Vector.get' left k kw = some bf := trees_preserve_notsomebranch bf k kw base left leftTree
rightLem : ¬Vector.get' right k kw = some bf := trees_preserve_notsomebranch bf k kw base right rightTree
c : ¬k = triple.pivot
j : ℕ := skipInverse triple.pivot k c
eqn : skip triple.pivot (skipInverse triple.pivot k c) = k := skipInverse_eq triple.pivot k c
jw : skipInverse triple.pivot k c < n := skip_preimage_lt triple.pivotLt kw eqn
joinIm : IsJoin (Vector.get' left (skip triple.pivot j) (_ : skip triple.pivot j < n + 1))
  (Vector.get' right (skip triple.pivot j) (_ : skip triple.pivot j < n + 1))
  (Vector.get' top (skip triple.pivot j) (_ : skip triple.pivot j < n + 1)) :=
  triple.joinRest j jw
join : IsJoin (Vector.get' left k kw) (Vector.get' right k kw) (Vector.get' top k kw)
⊢ False
Tactic:
apply top_of_join_not_positive bf
    (left.get' k kw) (right.get' k kw) (top.get' k kw) join
      leftLem rightLem
Proof state after:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
bf : Bool
k : ℕ
kw : k < n + 1
base : ∀ (j : ℕ) (lt : j < num_clauses), ¬Vector.get' (Vector.get' clauses j lt) k kw = some bf
top : Clause (n + 1)
tree : ResolutionTree clauses top
left right : Clause (n + 1)
leftTree : ResolutionTree clauses left
rightTree : ResolutionTree clauses right
triple : ResolutionTriple left right top
hyp : Vector.get' top k kw = some bf
leftLem : ¬Vector.get' left k kw = some bf := trees_preserve_notsomebranch bf k kw base left leftTree
rightLem : ¬Vector.get' right k kw = some bf := trees_preserve_notsomebranch bf k kw base right rightTree
c : ¬k = triple.pivot
j : ℕ := skipInverse triple.pivot k c
eqn : skip triple.pivot (skipInverse triple.pivot k c) = k := skipInverse_eq triple.pivot k c
jw : skipInverse triple.pivot k c < n := skip_preimage_lt triple.pivotLt kw eqn
joinIm : IsJoin (Vector.get' left (skip triple.pivot j) (_ : skip triple.pivot j < n + 1))
  (Vector.get' right (skip triple.pivot j) (_ : skip triple.pivot j < n + 1))
  (Vector.get' top (skip triple.pivot j) (_ : skip triple.pivot j < n + 1)) :=
  triple.joinRest j jw
join : IsJoin (Vector.get' left k kw) (Vector.get' right k kw) (Vector.get' top k kw)
⊢ Vector.get' top k kw = some bf
Theorem: trees_preserve_notsomebranch
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
bf : Bool
k : ℕ
kw : k < n + 1
base : ∀ (j : ℕ) (lt : j < num_clauses), ¬Vector.get' (Vector.get' clauses j lt) k kw = some bf
top : Clause (n + 1)
tree : ResolutionTree clauses top
left right : Clause (n + 1)
leftTree : ResolutionTree clauses left
rightTree : ResolutionTree clauses right
triple : ResolutionTriple left right top
hyp : Vector.get' top k kw = some bf
leftLem : ¬Vector.get' left k kw = some bf := trees_preserve_notsomebranch bf k kw base left leftTree
rightLem : ¬Vector.get' right k kw = some bf := trees_preserve_notsomebranch bf k kw base right rightTree
c : ¬k = triple.pivot
j : ℕ := skipInverse triple.pivot k c
eqn : skip triple.pivot (skipInverse triple.pivot k c) = k := skipInverse_eq triple.pivot k c
jw : skipInverse triple.pivot k c < n := skip_preimage_lt triple.pivotLt kw eqn
joinIm : IsJoin (Vector.get' left (skip triple.pivot j) (_ : skip triple.pivot j < n + 1))
  (Vector.get' right (skip triple.pivot j) (_ : skip triple.pivot j < n + 1))
  (Vector.get' top (skip triple.pivot j) (_ : skip triple.pivot j < n + 1)) :=
  triple.joinRest j jw
join : IsJoin (Vector.get' left k kw) (Vector.get' right k kw) (Vector.get' top k kw)
⊢ Vector.get' top k kw = some bf
Tactic:
exact hyp
Proof state after:
no goals
Theorem: Vector.ext'
Proof state before:
α : Type
n : ℕ
v1 v2 : Vector α n
⊢ get' v1 = get' v2 → v1 = v2
Tactic:
intro h
Proof state after:
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
⊢ v1 = v2
Theorem: Vector.ext'
Proof state before:
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
⊢ v1 = v2
Tactic:
apply Vector.ext
Proof state after:
case x
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
⊢ ∀ (m : Fin n), get v1 m = get v2 m
Theorem: Vector.ext'
Proof state before:
case x
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
⊢ ∀ (m : Fin n), get v1 m = get v2 m
Tactic:
intro ⟨i, iw⟩
Proof state after:
case x
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
i : ℕ
iw : i < n
⊢ get v1 { val := i, isLt := iw } = get v2 { val := i, isLt := iw }
Theorem: Vector.ext'
Proof state before:
case x
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
i : ℕ
iw : i < n
⊢ get v1 { val := i, isLt := iw } = get v2 { val := i, isLt := iw }
Tactic:
show get' v1 i iw = get' v2 i iw
Proof state after:
case x
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
i : ℕ
iw : i < n
⊢ get' v1 i iw = get' v2 i iw