Theorem: PosResClause.reverseResolve (Saturn/PosRestClause.lean)

State before:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
⊢ ∀ (rc : ReductionClauses branch focus focusLt clauses) (head : Clause (n + 1))
    (pos : Vector.get' head focus focusLt = some branch) (l : ℕ) (w : l < rc.num_reducedClauses),
    ReductionClauses.reverse (addPositiveClause branch focus focusLt clauses rc head pos) l w =
      ReductionClauses.reverse rc l w + 1
Tactic:
intro rc head neg l w
State after:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
⊢ ReductionClauses.reverse (addPositiveClause branch focus focusLt clauses rc head neg) l w =
    ReductionClauses.reverse rc l w + 1

State before:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
⊢ ReductionClauses.reverse (addPositiveClause branch focus focusLt clauses rc head neg) l w =
    ReductionClauses.reverse rc l w + 1
Tactic:
let rcN := addPositiveClause  branch focus focusLt clauses rc head neg
State after:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
⊢ ReductionClauses.reverse (addPositiveClause branch focus focusLt clauses rc head neg) l w =
    ReductionClauses.reverse rc l w + 1

State before:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
⊢ ReductionClauses.reverse (addPositiveClause branch focus focusLt clauses rc head neg) l w =
    ReductionClauses.reverse rc l w + 1
Tactic:
have res1 : rcN.reverse l w =
                          rcN.reverseVec.get' l w := by rfl
State after:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
⊢ ReductionClauses.reverse (addPositiveClause branch focus focusLt clauses rc head neg) l w =
    ReductionClauses.reverse rc l w + 1

State before:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
⊢ ReductionClauses.reverse (addPositiveClause branch focus focusLt clauses rc head neg) l w =
    ReductionClauses.reverse rc l w + 1
Tactic:
have res2 : rc.reverse l w =
        rc.reverseVec.get' l w := by rfl
State after:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
res2 : ReductionClauses.reverse rc l w = Vector.get' rc.reverseVec l w
⊢ ReductionClauses.reverse (addPositiveClause branch focus focusLt clauses rc head neg) l w =
    ReductionClauses.reverse rc l w + 1

State before:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
res2 : ReductionClauses.reverse rc l w = Vector.get' rc.reverseVec l w
⊢ ReductionClauses.reverse (addPositiveClause branch focus focusLt clauses rc head neg) l w =
    ReductionClauses.reverse rc l w + 1
Tactic:
rw [res1]
State after:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
res2 : ReductionClauses.reverse rc l w = Vector.get' rc.reverseVec l w
⊢ Vector.get' rcN.reverseVec l w = ReductionClauses.reverse rc l w + 1

State before:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
res2 : ReductionClauses.reverse rc l w = Vector.get' rc.reverseVec l w
⊢ Vector.get' rcN.reverseVec l w = ReductionClauses.reverse rc l w + 1
Tactic:
rw [res2]
State after:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
res2 : ReductionClauses.reverse rc l w = Vector.get' rc.reverseVec l w
⊢ Vector.get' rcN.reverseVec l w = Vector.get' rc.reverseVec l w + 1

State before:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
res2 : ReductionClauses.reverse rc l w = Vector.get' rc.reverseVec l w
⊢ Vector.get' rcN.reverseVec l w = Vector.get' rc.reverseVec l w + 1
Tactic:
have res3 :rcN.reverseVec =
  (rc.reverseVec.map (. + 1)) := by rfl
State after:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
res2 : ReductionClauses.reverse rc l w = Vector.get' rc.reverseVec l w
res3 : rcN.reverseVec = Vector.map (fun x => x + 1) rc.reverseVec
⊢ Vector.get' rcN.reverseVec l w = Vector.get' rc.reverseVec l w + 1

State before:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
res2 : ReductionClauses.reverse rc l w = Vector.get' rc.reverseVec l w
res3 : rcN.reverseVec = Vector.map (fun x => x + 1) rc.reverseVec
⊢ Vector.get' rcN.reverseVec l w = Vector.get' rc.reverseVec l w + 1
Tactic:
rw [res3]
State after:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
res2 : ReductionClauses.reverse rc l w = Vector.get' rc.reverseVec l w
res3 : rcN.reverseVec = Vector.map (fun x => x + 1) rc.reverseVec
⊢ Vector.get' (Vector.map (fun x => x + 1) rc.reverseVec) l w = Vector.get' rc.reverseVec l w + 1

State before:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
res2 : ReductionClauses.reverse rc l w = Vector.get' rc.reverseVec l w
res3 : rcN.reverseVec = Vector.map (fun x => x + 1) rc.reverseVec
⊢ Vector.get' (Vector.map (fun x => x + 1) rc.reverseVec) l w = Vector.get' rc.reverseVec l w + 1
Tactic:
have res4 :
    ( (rc.reverseVec.map (. + 1)) ).get' l w =
      (zero +:
      (rc.reverseVec.map (. + 1)) ).get'
      (l + 1) (Nat.succ_le_succ w) := by rfl
State after:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
res2 : ReductionClauses.reverse rc l w = Vector.get' rc.reverseVec l w
res3 : rcN.reverseVec = Vector.map (fun x => x + 1) rc.reverseVec
res4 :
  Vector.get' (Vector.map (fun x => x + 1) rc.reverseVec) l w =
    Vector.get' (zero ::ᵥ Vector.map (fun x => x + 1) rc.reverseVec) (l + 1)
      (_ : succ (l + 1) ≤ succ rc.num_reducedClauses)
⊢ Vector.get' (Vector.map (fun x => x + 1) rc.reverseVec) l w = Vector.get' rc.reverseVec l w + 1

State before:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
res2 : ReductionClauses.reverse rc l w = Vector.get' rc.reverseVec l w
res3 : rcN.reverseVec = Vector.map (fun x => x + 1) rc.reverseVec
res4 :
  Vector.get' (Vector.map (fun x => x + 1) rc.reverseVec) l w =
    Vector.get' (zero ::ᵥ Vector.map (fun x => x + 1) rc.reverseVec) (l + 1)
      (_ : succ (l + 1) ≤ succ rc.num_reducedClauses)
⊢ Vector.get' (Vector.map (fun x => x + 1) rc.reverseVec) l w = Vector.get' rc.reverseVec l w + 1
Tactic:
rw [res4]
State after:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
res2 : ReductionClauses.reverse rc l w = Vector.get' rc.reverseVec l w
res3 : rcN.reverseVec = Vector.map (fun x => x + 1) rc.reverseVec
res4 :
  Vector.get' (Vector.map (fun x => x + 1) rc.reverseVec) l w =
    Vector.get' (zero ::ᵥ Vector.map (fun x => x + 1) rc.reverseVec) (l + 1)
      (_ : succ (l + 1) ≤ succ rc.num_reducedClauses)
⊢ Vector.get' (zero ::ᵥ Vector.map (fun x => x + 1) rc.reverseVec) (l + 1)
      (_ : succ (l + 1) ≤ succ rc.num_reducedClauses) =
    Vector.get' rc.reverseVec l w + 1

State before:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
res2 : ReductionClauses.reverse rc l w = Vector.get' rc.reverseVec l w
res3 : rcN.reverseVec = Vector.map (fun x => x + 1) rc.reverseVec
res4 :
  Vector.get' (Vector.map (fun x => x + 1) rc.reverseVec) l w =
    Vector.get' (zero ::ᵥ Vector.map (fun x => x + 1) rc.reverseVec) (l + 1)
      (_ : succ (l + 1) ≤ succ rc.num_reducedClauses)
⊢ Vector.get' (zero ::ᵥ Vector.map (fun x => x + 1) rc.reverseVec) (l + 1)
      (_ : succ (l + 1) ≤ succ rc.num_reducedClauses) =
    Vector.get' rc.reverseVec l w + 1
Tactic:
rw [(get'_cons_succ
    zero (rc.reverseVec.map (. + 1)))]
State after:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
res2 : ReductionClauses.reverse rc l w = Vector.get' rc.reverseVec l w
res3 : rcN.reverseVec = Vector.map (fun x => x + 1) rc.reverseVec
res4 :
  Vector.get' (Vector.map (fun x => x + 1) rc.reverseVec) l w =
    Vector.get' (zero ::ᵥ Vector.map (fun x => x + 1) rc.reverseVec) (l + 1)
      (_ : succ (l + 1) ≤ succ rc.num_reducedClauses)
⊢ Vector.get' (Vector.map (fun x => x + 1) rc.reverseVec) l ?iw = Vector.get' rc.reverseVec l w + 1

case iw
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
res2 : ReductionClauses.reverse rc l w = Vector.get' rc.reverseVec l w
res3 : rcN.reverseVec = Vector.map (fun x => x + 1) rc.reverseVec
res4 :
  Vector.get' (Vector.map (fun x => x + 1) rc.reverseVec) l w =
    Vector.get' (zero ::ᵥ Vector.map (fun x => x + 1) rc.reverseVec) (l + 1)
      (_ : succ (l + 1) ≤ succ rc.num_reducedClauses)
⊢ l < rc.num_reducedClauses

State before:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
res2 : ReductionClauses.reverse rc l w = Vector.get' rc.reverseVec l w
res3 : rcN.reverseVec = Vector.map (fun x => x + 1) rc.reverseVec
res4 :
  Vector.get' (Vector.map (fun x => x + 1) rc.reverseVec) l w =
    Vector.get' (zero ::ᵥ Vector.map (fun x => x + 1) rc.reverseVec) (l + 1)
      (_ : succ (l + 1) ≤ succ rc.num_reducedClauses)
⊢ Vector.get' (Vector.map (fun x => x + 1) rc.reverseVec) l ?iw = Vector.get' rc.reverseVec l w + 1

case iw
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
res2 : ReductionClauses.reverse rc l w = Vector.get' rc.reverseVec l w
res3 : rcN.reverseVec = Vector.map (fun x => x + 1) rc.reverseVec
res4 :
  Vector.get' (Vector.map (fun x => x + 1) rc.reverseVec) l w =
    Vector.get' (zero ::ᵥ Vector.map (fun x => x + 1) rc.reverseVec) (l + 1)
      (_ : succ (l + 1) ≤ succ rc.num_reducedClauses)
⊢ l < rc.num_reducedClauses
Tactic:
rw [get'_map]
State after:
no goals

State before:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
⊢ ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
Tactic:
rfl
State after:
no goals

State before:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
⊢ ReductionClauses.reverse rc l w = Vector.get' rc.reverseVec l w
Tactic:
rfl
State after:
no goals

State before:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
res2 : ReductionClauses.reverse rc l w = Vector.get' rc.reverseVec l w
⊢ rcN.reverseVec = Vector.map (fun x => x + 1) rc.reverseVec
Tactic:
rfl
State after:
no goals

State before:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
res1 : ReductionClauses.reverse rcN l w = Vector.get' rcN.reverseVec l w
res2 : ReductionClauses.reverse rc l w = Vector.get' rc.reverseVec l w
res3 : rcN.reverseVec = Vector.map (fun x => x + 1) rc.reverseVec
⊢ Vector.get' (Vector.map (fun x => x + 1) rc.reverseVec) l w =
    Vector.get' (zero ::ᵥ Vector.map (fun x => x + 1) rc.reverseVec) (l + 1)
      (_ : succ (l + 1) ≤ succ rc.num_reducedClauses)
Tactic:
rfl
State after:
no goals