internlm/Lean-Github huggingface dataset:
Theorem: PosResClause.reverseResolve
Proof 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
Proof 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
Theorem: PosResClause.reverseResolve
Proof 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
Proof 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
Theorem: PosResClause.reverseResolve
Proof 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]
Proof 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
Theorem: PosResClause.reverseResolve
Proof 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]
Proof 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
Theorem: PosResClause.reverseResolve
Proof 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
Proof 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
Theorem: PosResClause.reverseResolve
Proof 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]
Proof 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
Theorem: PosResClause.reverseResolve
Proof 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
Proof 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
Theorem: PosResClause.reverseResolve
Proof 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]
Proof 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
Theorem: PosResClause.reverseResolve
Proof 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)))]
Proof 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
Theorem: PosResClause.reverseResolve
Proof 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]
Proof state after:
no goals
Theorem: PosResClause.reverseResolve
Proof 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
Proof state after:
no goals
Theorem: PosResClause.reverseResolve
Proof 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
Proof state after:
no goals
Theorem: PosResClause.reverseResolve
Proof 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
Proof state after:
no goals
Theorem: PosResClause.reverseResolve
Proof 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
Proof state after:
no goals
Theorem: none_mapsto_none
Proof state before:
α β : Type
fn : α → β
⊢ none = none
Tactic:
rfl
Proof state after:
no goals
Theorem: map_plusone_not_somezero
Proof state before:
n : Option ℕ
j : ℕ
hyp : some (j + 1) = some zero
⊢ j + 1 = zero
Tactic:
injection hyp
Proof state after:
no goals
Theorem: map_plusone_pred
Proof state before:
n : Option ℕ
m j : ℕ
hyp : some (j + 1) = some (m + 1)
⊢ j + 1 = m + 1
Tactic:
injection hyp
Proof state after:
no goals
Theorem: map_plusone_pred
Proof state before:
n : Option ℕ
m j : ℕ
hyp : some (j + 1) = some (m + 1)
lem1 : j + 1 = m + 1 := Option.noConfusion hyp fun val_eq => val_eq
⊢ j = m
Tactic:
injection lem1
Proof state after:
no goals
Theorem: PrependClause.forwardResolve
Proof 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 : ¬get' head focus focusLt = some branch) (l : ℕ) (w : l + 1 < num_clauses + 1),
    ReductionClauses.forward (prependClause branch focus focusLt clauses rc head neg) (l + 1) w =
      Option.map (fun x => x + 1) (ReductionClauses.forward rc l (_ : succ l ≤ num_clauses))
Tactic:
intro rc head _ l w
Proof 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✝ : ¬get' head focus focusLt = some branch
l : ℕ
w : l + 1 < num_clauses + 1
⊢ ReductionClauses.forward (prependClause branch focus focusLt clauses rc head neg✝) (l + 1) w =
    Option.map (fun x => x + 1) (ReductionClauses.forward rc l (_ : succ l ≤ num_clauses))
Theorem: PrependClause.forwardResolve
Proof 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✝ : ¬get' head focus focusLt = some branch
l : ℕ
w : l + 1 < num_clauses + 1
⊢ ReductionClauses.forward (prependClause branch focus focusLt clauses rc head neg✝) (l + 1) w =
    Option.map (fun x => x + 1) (ReductionClauses.forward rc l (_ : succ l ≤ num_clauses))
Tactic:
simp [ReductionClauses.forward, ReductionClauses.forwardVec, prependClause]
Proof 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✝ : ¬get' head focus focusLt = some branch
l : ℕ
w : l + 1 < num_clauses + 1
⊢ get' (some 0 ::ᵥ map (fun nop => Option.map (fun x => x + 1) nop) rc.forwardVec) (l + 1) w =
    Option.map (fun x => x + 1) (get' rc.forwardVec l (_ : succ l ≤ num_clauses))
Theorem: PrependClause.forwardResolve
Proof 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✝ : ¬get' head focus focusLt = some branch
l : ℕ
w : l + 1 < num_clauses + 1
⊢ get' (some 0 ::ᵥ map (fun nop => Option.map (fun x => x + 1) nop) rc.forwardVec) (l + 1) w =
    Option.map (fun x => x + 1) (get' rc.forwardVec l (_ : succ l ≤ num_clauses))
Tactic:
simp [Vector.get']
Proof 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✝ : ¬get' head focus focusLt = some branch
l : ℕ
w : l + 1 < num_clauses + 1
⊢ Vector.get (some 0 ::ᵥ map (fun nop => Option.map (fun x => x + 1) nop) rc.forwardVec) { val := l + 1, isLt := w } =
    Option.map (fun x => x + 1) (Vector.get rc.forwardVec { val := l, isLt := (_ : succ l ≤ num_clauses) })