Theorem: trees_preserve_notsomebranch (Saturn/Resolution.lean)

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)
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

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
State after:
no goals

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]
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

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)
State after:
no goals

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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
State after:
no goals