Theorem: pureTail_at_end (Saturn/Clause.lean)

State before:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
m : ℕ
le : num_clauses ≤ m
⊢ HasPureTail clauses index bound parity m
Tactic:
intro k
State after:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
m : ℕ
le : num_clauses ≤ m
k : ℕ
⊢ ∀ (lt : k < num_clauses),
    m ≤ k → get' (get' clauses k lt) index bound = none ∨ get' (get' clauses k lt) index bound = some parity

State before:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
m : ℕ
le : num_clauses ≤ m
k : ℕ
⊢ ∀ (lt : k < num_clauses),
    m ≤ k → get' (get' clauses k lt) index bound = none ∨ get' (get' clauses k lt) index bound = some parity
Tactic:
intro kw
State after:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
m : ℕ
le : num_clauses ≤ m
k : ℕ
kw : k < num_clauses
⊢ m ≤ k → get' (get' clauses k kw) index bound = none ∨ get' (get' clauses k kw) index bound = some parity

State before:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
m : ℕ
le : num_clauses ≤ m
k : ℕ
kw : k < num_clauses
⊢ m ≤ k → get' (get' clauses k kw) index bound = none ∨ get' (get' clauses k kw) index bound = some parity
Tactic:
intro ineq
State after:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
m : ℕ
le : num_clauses ≤ m
k : ℕ
kw : k < num_clauses
ineq : m ≤ k
⊢ get' (get' clauses k kw) index bound = none ∨ get' (get' clauses k kw) index bound = some parity

State before:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
m : ℕ
le : num_clauses ≤ m
k : ℕ
kw : k < num_clauses
ineq : m ≤ k
⊢ get' (get' clauses k kw) index bound = none ∨ get' (get' clauses k kw) index bound = some parity
Tactic:
let inq := Nat.le_trans le ineq
State after:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
m : ℕ
le : num_clauses ≤ m
k : ℕ
kw : k < num_clauses
ineq : m ≤ k
inq : num_clauses ≤ k := Nat.le_trans le ineq
⊢ get' (get' clauses k kw) index bound = none ∨ get' (get' clauses k kw) index bound = some parity

State before:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
m : ℕ
le : num_clauses ≤ m
k : ℕ
kw : k < num_clauses
ineq : m ≤ k
inq : num_clauses ≤ k := Nat.le_trans le ineq
⊢ get' (get' clauses k kw) index bound = none ∨ get' (get' clauses k kw) index bound = some parity
Tactic:
let inq2 := Nat.lt_of_lt_of_le kw inq
State after:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
m : ℕ
le : num_clauses ≤ m
k : ℕ
kw : k < num_clauses
ineq : m ≤ k
inq : num_clauses ≤ k := Nat.le_trans le ineq
inq2 : k < k := Nat.lt_of_lt_of_le kw inq
⊢ get' (get' clauses k kw) index bound = none ∨ get' (get' clauses k kw) index bound = some parity

State before:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
m : ℕ
le : num_clauses ≤ m
k : ℕ
kw : k < num_clauses
ineq : m ≤ k
inq : num_clauses ≤ k := Nat.le_trans le ineq
inq2 : k < k := Nat.lt_of_lt_of_le kw inq
⊢ get' (get' clauses k kw) index bound = none ∨ get' (get' clauses k kw) index bound = some parity
Tactic:
exact (False.elim (Nat.lt_irrefl k inq2))
State after:
no goals