-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVecOperator/Zip.lean
theorem go_denote_mem_prefix {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len)
    (s : RefVec aig curr) (lhs rhs : RefVec aig len)
    (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput f]
    [chainable : LawfulZipOperator α f] (start : Nat) (hstart) :
    ⟦
      (go aig curr s hcurr lhs rhs f).aig,
      ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
      assign
    ⟧
      =
    ⟦aig, ⟨start, hstart⟩, assign⟧

Proof state:
case a
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
start : Nat
hstart : start < aig.decls.size
⊢ aig.decls.size ≤ (go aig curr s hcurr lhs rhs f).aig.decls.size

Tactic:
apply go_le_size

Result:
no goals

Proof state:
case hprefix.idx_eq
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
start : Nat
hstart : start < aig.decls.size
idx✝ : Nat
h✝ : idx✝ < { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size
⊢ (go aig curr s hcurr lhs rhs f).aig.decls[idx✝] =
    { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls[idx✝]

Tactic:
apply go_decl_eq

Result:
no goals

Proof state:
case hprefix.idx_eq
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
start : Nat
hstart : start < aig.decls.size
⊢ ∀ (idx : Nat) (h : idx < { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size),
    (go aig curr s hcurr lhs rhs f).aig.decls[idx] =
      { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls[idx]

Tactic:
intros

Result:
case hprefix.idx_eq
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
start : Nat
hstart : start < aig.decls.size
idx✝ : Nat
h✝ : idx✝ < { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size
⊢ (go aig curr s hcurr lhs rhs f).aig.decls[idx✝] =
    { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls[idx✝]

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
start : Nat
hstart : start < aig.decls.size
⊢ start < (go aig curr s hcurr lhs rhs f).aig.decls.size

Tactic:
apply Nat.lt_of_lt_of_le

Result:
case a
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
start : Nat
hstart : start < aig.decls.size
⊢ start < ?m

case a
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
start : Nat
hstart : start < aig.decls.size
⊢ ?m ≤ (go aig curr s hcurr lhs rhs f).aig.decls.size

case m
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
start : Nat
hstart : start < aig.decls.size
⊢ Nat

Proof state:
case a
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
start : Nat
hstart : start < aig.decls.size
⊢ start < ?m

case a
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
start : Nat
hstart : start < aig.decls.size
⊢ ?m ≤ (go aig curr s hcurr lhs rhs f).aig.decls.size

case m
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
start : Nat
hstart : start < aig.decls.size
⊢ Nat

Tactic:
exact hstart

Result:
case a
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
start : Nat
hstart : start < aig.decls.size
⊢ aig.decls.size ≤ (go aig curr s hcurr lhs rhs f).aig.decls.size

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
start : Nat
hstart : start < aig.decls.size
⊢ ⟦assign, { aig := (go aig curr s hcurr lhs rhs f).aig, ref := { gate := start, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧

Tactic:
apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)

Result:
case hprefix
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
start : Nat
hstart : start < aig.decls.size
⊢ IsPrefix { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls (go aig curr s hcurr lhs rhs f).aig.decls

Proof state:
case hprefix.size_le
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
start : Nat
hstart : start < aig.decls.size
⊢ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size ≤
    (go aig curr s hcurr lhs rhs f).aig.decls.size

Tactic:
apply go_le_size

Result:
no goals