internlm/Lean-Github huggingface dataset:
Theorem: AIG.RefStream.fold.denote_go_and
Proof state before:
case isTrue.mp.intro.intro.right.inr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
h1 : ⟦{ aig := aig, ref := acc }, assign⟧ = true
h2 : ⟦{ aig := aig, ref := input.getRef curr h✝ }, assign⟧ = true
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
hlt : curr < idx
h3 :
  ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig, ref := (input.getRef idx hidx1).cast ⋯ },
      assign⟧ =
    true
⊢ ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ =
    ⟦{ aig := aig,
        ref := { gate := ((input.getRef idx hidx1).cast ⋯).gate, hgate := ?isTrue.mp.intro.intro.right.inr } },
      assign⟧

case isTrue.mp.intro.intro.right.inr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
h1 : ⟦{ aig := aig, ref := acc }, assign⟧ = true
h2 : ⟦{ aig := aig, ref := input.getRef curr h✝ }, assign⟧ = true
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
hlt : curr < idx
h3 :
  ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig, ref := (input.getRef idx hidx1).cast ⋯ },
      assign⟧ =
    true
⊢ ((input.getRef idx hidx1).cast ⋯).gate < aig.decls.size
Tactic:
. simp
Proof state after:
case isTrue.mp.intro.intro.right.inr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
h1 : ⟦{ aig := aig, ref := acc }, assign⟧ = true
h2 : ⟦{ aig := aig, ref := input.getRef curr h✝ }, assign⟧ = true
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
hlt : curr < idx
h3 :
  ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig, ref := (input.getRef idx hidx1).cast ⋯ },
      assign⟧ =
    true
⊢ ((input.getRef idx hidx1).cast ⋯).gate < aig.decls.size
Theorem: AIG.RefStream.fold.denote_go_and
Proof state before:
case isTrue.mp.intro.intro.right.inr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
h1 : ⟦{ aig := aig, ref := acc }, assign⟧ = true
h2 : ⟦{ aig := aig, ref := input.getRef curr h✝ }, assign⟧ = true
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
hlt : curr < idx
h3 :
  ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig, ref := (input.getRef idx hidx1).cast ⋯ },
      assign⟧ =
    true
⊢ ((input.getRef idx hidx1).cast ⋯).gate < aig.decls.size
Tactic:
. simp [Ref.hgate]
Proof state after:
no goals
Theorem: AIG.RefStream.fold.denote_go_and
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
h3 :
  ∀ (idx : Nat) (hidx1 : idx < len),
    curr + 1 ≤ idx →
      ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig,
            ref := (input.getRef idx hidx1).cast ⋯ },
          assign⟧ =
        true
h1 : ⟦{ aig := aig, ref := acc }, assign⟧ = true
h2 : ⟦{ aig := aig, ref := input.getRef curr h✝ }, assign⟧ = true
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
hlt : curr < idx
⊢ curr + 1 ≤ idx
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.RefStream.fold.denote_go_and
Proof state before:
case isTrue.mp.intro.intro.right.inr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
h1 : ⟦{ aig := aig, ref := acc }, assign⟧ = true
h2 : ⟦{ aig := aig, ref := input.getRef curr h✝ }, assign⟧ = true
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
hlt : curr < idx
h3 :
  ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig, ref := (input.getRef idx hidx1).cast ⋯ },
      assign⟧ =
    true
⊢ ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ =
    ⟦{ aig := aig,
        ref := { gate := ((input.getRef idx hidx1).cast ⋯).gate, hgate := ?isTrue.mp.intro.intro.right.inr } },
      assign⟧
Tactic:
simp
Proof state after:
no goals
Theorem: AIG.RefStream.fold.denote_go_and
Proof state before:
case isTrue.mp.intro.intro.right.inr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
h1 : ⟦{ aig := aig, ref := acc }, assign⟧ = true
h2 : ⟦{ aig := aig, ref := input.getRef curr h✝ }, assign⟧ = true
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
hlt : curr < idx
h3 :
  ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig, ref := (input.getRef idx hidx1).cast ⋯ },
      assign⟧ =
    true
⊢ ((input.getRef idx hidx1).cast ⋯).gate < aig.decls.size
Tactic:
simp [Ref.hgate]
Proof state after:
no goals
Theorem: AIG.RefStream.fold.denote_go_and
Proof state before:
case isTrue.mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
⊢ (⟦{ aig := aig, ref := acc }, assign⟧ = true ∧
      ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true) →
    (⟦{ aig := aig, ref := acc }, assign⟧ = true ∧ ⟦{ aig := aig, ref := input.getRef curr h✝ }, assign⟧ = true) ∧
      ∀ (idx : Nat) (hidx1 : idx < len),
        curr + 1 ≤ idx →
          ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig,
                ref := (input.getRef idx hidx1).cast ⋯ },
              assign⟧ =
            true
Tactic:
simp only [and_imp]
Proof state after:
case isTrue.mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
⊢ ⟦{ aig := aig, ref := acc }, assign⟧ = true →
    (∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true) →
      (⟦{ aig := aig, ref := acc }, assign⟧ = true ∧ ⟦{ aig := aig, ref := input.getRef curr h✝ }, assign⟧ = true) ∧
        ∀ (idx : Nat) (hidx1 : idx < len),
          curr + 1 ≤ idx →
            ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig,
                  ref := (input.getRef idx hidx1).cast ⋯ },
                assign⟧ =
              true
Theorem: AIG.RefStream.fold.denote_go_and
Proof state before:
case isTrue.mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
⊢ ⟦{ aig := aig, ref := acc }, assign⟧ = true →
    (∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true) →
      (⟦{ aig := aig, ref := acc }, assign⟧ = true ∧ ⟦{ aig := aig, ref := input.getRef curr h✝ }, assign⟧ = true) ∧
        ∀ (idx : Nat) (hidx1 : idx < len),
          curr + 1 ≤ idx →
            ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig,
                  ref := (input.getRef idx hidx1).cast ⋯ },
                assign⟧ =
              true
Tactic:
intro hacc hrest
Proof state after:
case isTrue.mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
hacc : ⟦{ aig := aig, ref := acc }, assign⟧ = true
hrest : ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true
⊢ (⟦{ aig := aig, ref := acc }, assign⟧ = true ∧ ⟦{ aig := aig, ref := input.getRef curr h✝ }, assign⟧ = true) ∧
    ∀ (idx : Nat) (hidx1 : idx < len),
      curr + 1 ≤ idx →
        ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig,
              ref := (input.getRef idx hidx1).cast ⋯ },
            assign⟧ =
          true
Theorem: AIG.RefStream.fold.denote_go_and
Proof state before:
case isTrue.mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
hacc : ⟦{ aig := aig, ref := acc }, assign⟧ = true
hrest : ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true
⊢ (⟦{ aig := aig, ref := acc }, assign⟧ = true ∧ ⟦{ aig := aig, ref := input.getRef curr h✝ }, assign⟧ = true) ∧
    ∀ (idx : Nat) (hidx1 : idx < len),
      curr + 1 ≤ idx →
        ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig,
              ref := (input.getRef idx hidx1).cast ⋯ },
            assign⟧ =
          true
Tactic:
constructor
Proof state after:
case isTrue.mpr.left
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
hacc : ⟦{ aig := aig, ref := acc }, assign⟧ = true
hrest : ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true
⊢ ⟦{ aig := aig, ref := acc }, assign⟧ = true ∧ ⟦{ aig := aig, ref := input.getRef curr h✝ }, assign⟧ = true

case isTrue.mpr.right
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
hacc : ⟦{ aig := aig, ref := acc }, assign⟧ = true
hrest : ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true
⊢ ∀ (idx : Nat) (hidx1 : idx < len),
    curr + 1 ≤ idx →
      ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig,
            ref := (input.getRef idx hidx1).cast ⋯ },
          assign⟧ =
        true
Theorem: AIG.RefStream.fold.denote_go_and
Proof state before:
case isTrue.mpr.left
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
hacc : ⟦{ aig := aig, ref := acc }, assign⟧ = true
hrest : ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true
⊢ ⟦{ aig := aig, ref := acc }, assign⟧ = true ∧ ⟦{ aig := aig, ref := input.getRef curr h✝ }, assign⟧ = true

case isTrue.mpr.right
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
hacc : ⟦{ aig := aig, ref := acc }, assign⟧ = true
hrest : ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true
⊢ ∀ (idx : Nat) (hidx1 : idx < len),
    curr + 1 ≤ idx →
      ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig,
            ref := (input.getRef idx hidx1).cast ⋯ },
          assign⟧ =
        true
Tactic:
. simp [hacc, hrest]
Proof state after:
case isTrue.mpr.right
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
hacc : ⟦{ aig := aig, ref := acc }, assign⟧ = true
hrest : ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true
⊢ ∀ (idx : Nat) (hidx1 : idx < len),
    curr + 1 ≤ idx →
      ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig,
            ref := (input.getRef idx hidx1).cast ⋯ },
          assign⟧ =
        true
Theorem: AIG.RefStream.fold.denote_go_and
Proof state before:
case isTrue.mpr.right
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
hacc : ⟦{ aig := aig, ref := acc }, assign⟧ = true
hrest : ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true
⊢ ∀ (idx : Nat) (hidx1 : idx < len),
    curr + 1 ≤ idx →
      ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig,
            ref := (input.getRef idx hidx1).cast ⋯ },
          assign⟧ =
        true
Tactic:
. intro idx hidx1 hidx2
  specialize hrest idx hidx1 (by omega)
  rw [← hrest]
  rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkAndCached)]
  . simp
  . simp [Ref.hgate]
Proof state after:
no goals
Theorem: AIG.RefStream.fold.denote_go_and
Proof state before:
case isTrue.mpr.left
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
hacc : ⟦{ aig := aig, ref := acc }, assign⟧ = true
hrest : ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true
⊢ ⟦{ aig := aig, ref := acc }, assign⟧ = true ∧ ⟦{ aig := aig, ref := input.getRef curr h✝ }, assign⟧ = true
Tactic:
simp [hacc, hrest]
Proof state after:
no goals
Theorem: AIG.RefStream.fold.denote_go_and
Proof state before:
case isTrue.mpr.right
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
hacc : ⟦{ aig := aig, ref := acc }, assign⟧ = true
hrest : ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true
⊢ ∀ (idx : Nat) (hidx1 : idx < len),
    curr + 1 ≤ idx →
      ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig,
            ref := (input.getRef idx hidx1).cast ⋯ },
          assign⟧ =
        true
Tactic:
intro idx hidx1 hidx2
Proof state after:
case isTrue.mpr.right
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
hacc : ⟦{ aig := aig, ref := acc }, assign⟧ = true
hrest : ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true
idx : Nat
hidx1 : idx < len
hidx2 : curr + 1 ≤ idx
⊢ ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig, ref := (input.getRef idx hidx1).cast ⋯ },
      assign⟧ =
    true
Theorem: AIG.RefStream.fold.denote_go_and
Proof state before:
case isTrue.mpr.right
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
hacc : ⟦{ aig := aig, ref := acc }, assign⟧ = true
hrest : ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true
idx : Nat
hidx1 : idx < len
hidx2 : curr + 1 ≤ idx
⊢ ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig, ref := (input.getRef idx hidx1).cast ⋯ },
      assign⟧ =
    true
Tactic:
specialize hrest idx hidx1 (by omega)
Proof state after:
case isTrue.mpr.right
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
hacc : ⟦{ aig := aig, ref := acc }, assign⟧ = true
idx : Nat
hidx1 : idx < len
hidx2 : curr + 1 ≤ idx
hrest : ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true
⊢ ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig, ref := (input.getRef idx hidx1).cast ⋯ },
      assign⟧ =
    true
Theorem: AIG.RefStream.fold.denote_go_and
Proof state before:
case isTrue.mpr.right
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
hacc : ⟦{ aig := aig, ref := acc }, assign⟧ = true
idx : Nat
hidx1 : idx < len
hidx2 : curr + 1 ≤ idx
hrest : ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true
⊢ ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig, ref := (input.getRef idx hidx1).cast ⋯ },
      assign⟧ =
    true
Tactic:
rw [← hrest]
Proof state after:
case isTrue.mpr.right
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
hacc : ⟦{ aig := aig, ref := acc }, assign⟧ = true
idx : Nat
hidx1 : idx < len
hidx2 : curr + 1 ≤ idx
hrest : ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true
⊢ ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig, ref := (input.getRef idx hidx1).cast ⋯ },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧