Theorem: AIG.ofBoolExprCached.go_decl_eq (LeanSAT/AIG/BoolExprCached.lean)

State before:
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
idx : Nat
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr aig atomHandler).val.aig.decls.size
⊢ (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
induction expr generalizing aig with
| const =>
  simp only [go]
  rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)]
| literal =>
  simp only [go]
  rw [AIG.LawfulOperator.decl_eq (f := atomHandler)]
| not expr ih =>
  simp only [go]
  have := go_decls_size_le atomHandler expr aig
  specialize ih aig (by omega) (by omega)
  rw [AIG.LawfulOperator.decl_eq (f := mkNotCached)]
  assumption
| gate g lhs rhs lih rih =>
  have := go_decls_size_le atomHandler lhs aig
  have := go_decls_size_le atomHandler rhs (go lhs aig atomHandler).val.aig
  specialize lih aig (by omega) (by omega)
  specialize rih (go lhs aig atomHandler).val.aig (by omega) (by omega)
  cases g with
  | and =>
    simp only [go]
    rw [AIG.LawfulOperator.decl_eq (f := mkAndCached)]
    rw [rih, lih]
  | or =>
    simp only [go]
    rw [AIG.LawfulOperator.decl_eq (f := mkOrCached)]
    rw [rih, lih]
  | xor =>
    simp only [go]
    rw [AIG.LawfulOperator.decl_eq (f := mkXorCached)]
    rw [rih, lih]
  | beq =>
    simp only [go]
    rw [AIG.LawfulOperator.decl_eq (f := mkBEqCached)]
    rw [rih, lih]
  | imp =>
    simp only [go]
    rw [AIG.LawfulOperator.decl_eq (f := mkImpCached)]
    rw [rih, lih]
State after:
no goals

State before:
case const
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
a✝ : Bool
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.const a✝) aig atomHandler).val.aig.decls.size
⊢ (go (BoolExpr.const a✝) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [go]
State after:
case const
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
a✝ : Bool
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.const a✝) aig atomHandler).val.aig.decls.size
⊢ (aig.mkConstCached a✝).aig.decls[idx] = aig.decls[idx]

State before:
case const
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
a✝ : Bool
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.const a✝) aig atomHandler).val.aig.decls.size
⊢ (aig.mkConstCached a✝).aig.decls[idx] = aig.decls[idx]
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)]
State after:
no goals

State before:
case literal
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
a✝ : α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.literal a✝) aig atomHandler).val.aig.decls.size
⊢ (go (BoolExpr.literal a✝) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [go]
State after:
case literal
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
a✝ : α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.literal a✝) aig atomHandler).val.aig.decls.size
⊢ (atomHandler aig a✝).aig.decls[idx] = aig.decls[idx]

State before:
case literal
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
a✝ : α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.literal a✝) aig atomHandler).val.aig.decls.size
⊢ (atomHandler aig a✝).aig.decls[idx] = aig.decls[idx]
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := atomHandler)]
State after:
no goals

State before:
case not
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
ih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go expr aig atomHandler).val.aig.decls.size),
    (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
⊢ (go expr.not aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [go]
State after:
case not
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
ih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go expr aig atomHandler).val.aig.decls.size),
    (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
⊢ ((go expr aig atomHandler).1.aig.mkNotCached (go expr aig atomHandler).1.ref).aig.decls[idx] = aig.decls[idx]

State before:
case not
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
ih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go expr aig atomHandler).val.aig.decls.size),
    (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
⊢ ((go expr aig atomHandler).1.aig.mkNotCached (go expr aig atomHandler).1.ref).aig.decls[idx] = aig.decls[idx]
Tactic:
have := go_decls_size_le atomHandler expr aig
State after:
case not
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
ih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go expr aig atomHandler).val.aig.decls.size),
    (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
⊢ ((go expr aig atomHandler).1.aig.mkNotCached (go expr aig atomHandler).1.ref).aig.decls[idx] = aig.decls[idx]

State before:
case not
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
ih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go expr aig atomHandler).val.aig.decls.size),
    (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
⊢ ((go expr aig atomHandler).1.aig.mkNotCached (go expr aig atomHandler).1.ref).aig.decls[idx] = aig.decls[idx]
Tactic:
specialize ih aig (by omega) (by omega)
State after:
case not
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
ih : (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ ((go expr aig atomHandler).1.aig.mkNotCached (go expr aig atomHandler).1.ref).aig.decls[idx] = aig.decls[idx]

State before:
case not
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
ih : (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ ((go expr aig atomHandler).1.aig.mkNotCached (go expr aig atomHandler).1.ref).aig.decls[idx] = aig.decls[idx]
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := mkNotCached)]
State after:
case not
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
ih : (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ (go expr aig atomHandler).1.aig.decls[idx] = aig.decls[idx]

case not.h1
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
ih : (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ idx < (go expr aig atomHandler).1.aig.decls.size

State before:
case not
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
ih : (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ (go expr aig atomHandler).1.aig.decls[idx] = aig.decls[idx]

case not.h1
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
ih : (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ idx < (go expr aig atomHandler).1.aig.decls.size
Tactic:
assumption
State after:
no goals

State before:
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
ih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go expr aig atomHandler).val.aig.decls.size),
    (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
⊢ idx < aig.decls.size
Tactic:
omega
State after:
no goals

State before:
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
ih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go expr aig atomHandler).val.aig.decls.size),
    (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
⊢ idx < (go expr aig atomHandler).val.aig.decls.size
Tactic:
omega
State after:
no goals

State before:
case gate
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
lih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go lhs aig atomHandler).val.aig.decls.size),
    (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
⊢ (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
have := go_decls_size_le atomHandler lhs aig
State after:
case gate
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
lih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go lhs aig atomHandler).val.aig.decls.size),
    (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
⊢ (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]

State before:
case gate
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
lih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go lhs aig atomHandler).val.aig.decls.size),
    (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
⊢ (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
have := go_decls_size_le atomHandler rhs (go lhs aig atomHandler).val.aig
State after:
case gate
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
lih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go lhs aig atomHandler).val.aig.decls.size),
    (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
⊢ (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]

State before:
case gate
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
lih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go lhs aig atomHandler).val.aig.decls.size),
    (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
⊢ (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
specialize lih aig (by omega) (by omega)
State after:
case gate
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]

State before:
case gate
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
specialize rih (go lhs aig atomHandler).val.aig (by omega) (by omega)
State after:
case gate
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]

State before:
case gate
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
cases g with
| and =>
  simp only [go]
  rw [AIG.LawfulOperator.decl_eq (f := mkAndCached)]
  rw [rih, lih]
| or =>
  simp only [go]
  rw [AIG.LawfulOperator.decl_eq (f := mkOrCached)]
  rw [rih, lih]
| xor =>
  simp only [go]
  rw [AIG.LawfulOperator.decl_eq (f := mkXorCached)]
  rw [rih, lih]
| beq =>
  simp only [go]
  rw [AIG.LawfulOperator.decl_eq (f := mkBEqCached)]
  rw [rih, lih]
| imp =>
  simp only [go]
  rw [AIG.LawfulOperator.decl_eq (f := mkImpCached)]
  rw [rih, lih]
State after:
no goals

State before:
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
lih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go lhs aig atomHandler).val.aig.decls.size),
    (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
⊢ idx < aig.decls.size
Tactic:
omega
State after:
no goals

State before:
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
lih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go lhs aig atomHandler).val.aig.decls.size),
    (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
⊢ idx < (go lhs aig atomHandler).val.aig.decls.size
Tactic:
omega
State after:
no goals

State before:
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ idx < (go lhs aig atomHandler).val.aig.decls.size
Tactic:
omega
State after:
no goals

State before:
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ idx < (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
Tactic:
omega
State after:
no goals

State before:
case gate.and
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.and lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go (BoolExpr.gate Gate.and lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [go]
State after:
case gate.and
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.and lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ ((go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.mkAndCached
            { lhs := (go lhs aig atomHandler).1.ref.cast ⋯,
              rhs := (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.ref }).aig.decls[idx] =
    aig.decls[idx]

State before:
case gate.and
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.and lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ ((go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.mkAndCached
            { lhs := (go lhs aig atomHandler).1.ref.cast ⋯,
              rhs := (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.ref }).aig.decls[idx] =
    aig.decls[idx]
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := mkAndCached)]
State after:
case gate.and
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.and lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls[idx] = aig.decls[idx]

case gate.and.h1
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.and lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ idx < (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls.size

State before:
case gate.and
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.and lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls[idx] = aig.decls[idx]

case gate.and.h1
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.and lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ idx < (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls.size
Tactic:
rw [rih, lih]
State after:
no goals

State before:
case gate.or
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.or lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go (BoolExpr.gate Gate.or lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [go]
State after:
case gate.or
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.or lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ ((go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.mkOrCached
            { lhs := (go lhs aig atomHandler).1.ref.cast ⋯,
              rhs := (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.ref }).aig.decls[idx] =
    aig.decls[idx]

State before:
case gate.or
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.or lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ ((go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.mkOrCached
            { lhs := (go lhs aig atomHandler).1.ref.cast ⋯,
              rhs := (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.ref }).aig.decls[idx] =
    aig.decls[idx]
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := mkOrCached)]
State after:
case gate.or
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.or lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls[idx] = aig.decls[idx]

case gate.or.h1
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.or lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ idx < (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls.size

State before:
case gate.or
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.or lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls[idx] = aig.decls[idx]

case gate.or.h1
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.or lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ idx < (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls.size
Tactic:
rw [rih, lih]
State after:
no goals

State before:
case gate.xor
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.xor lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go (BoolExpr.gate Gate.xor lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [go]
State after:
case gate.xor
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.xor lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ ((go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.mkXorCached
            { lhs := (go lhs aig atomHandler).1.ref.cast ⋯,
              rhs := (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.ref }).aig.decls[idx] =
    aig.decls[idx]

State before:
case gate.xor
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.xor lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ ((go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.mkXorCached
            { lhs := (go lhs aig atomHandler).1.ref.cast ⋯,
              rhs := (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.ref }).aig.decls[idx] =
    aig.decls[idx]
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := mkXorCached)]
State after:
case gate.xor
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.xor lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls[idx] = aig.decls[idx]

case gate.xor.h1
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.xor lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ idx < (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls.size

State before:
case gate.xor
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.xor lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls[idx] = aig.decls[idx]

case gate.xor.h1
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.xor lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ idx < (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls.size
Tactic:
rw [rih, lih]
State after:
no goals

State before:
case gate.beq
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.beq lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go (BoolExpr.gate Gate.beq lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [go]
State after:
case gate.beq
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.beq lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ ((go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.mkBEqCached
            { lhs := (go lhs aig atomHandler).1.ref.cast ⋯,
              rhs := (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.ref }).aig.decls[idx] =
    aig.decls[idx]

State before:
case gate.beq
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.beq lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ ((go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.mkBEqCached
            { lhs := (go lhs aig atomHandler).1.ref.cast ⋯,
              rhs := (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.ref }).aig.decls[idx] =
    aig.decls[idx]
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := mkBEqCached)]
State after:
case gate.beq
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.beq lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls[idx] = aig.decls[idx]

case gate.beq.h1
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.beq lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ idx < (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls.size

State before:
case gate.beq
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.beq lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls[idx] = aig.decls[idx]

case gate.beq.h1
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.beq lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ idx < (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls.size
Tactic:
rw [rih, lih]
State after:
no goals

State before:
case gate.imp
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.imp lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go (BoolExpr.gate Gate.imp lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [go]
State after:
case gate.imp
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.imp lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ ((go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.mkImpCached
            { lhs := (go lhs aig atomHandler).1.ref.cast ⋯,
              rhs := (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.ref }).aig.decls[idx] =
    aig.decls[idx]

State before:
case gate.imp
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.imp lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ ((go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.mkImpCached
            { lhs := (go lhs aig atomHandler).1.ref.cast ⋯,
              rhs := (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.ref }).aig.decls[idx] =
    aig.decls[idx]
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := mkImpCached)]
State after:
case gate.imp
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.imp lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls[idx] = aig.decls[idx]

case gate.imp.h1
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.imp lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ idx < (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls.size

State before:
case gate.imp
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.imp lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls[idx] = aig.decls[idx]

case gate.imp.h1
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.imp lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ idx < (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls.size
Tactic:
rw [rih, lih]
State after:
no goals