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

State before:
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ IsPrefix aig.decls (go expr aig atomHandler).val.aig.decls
Tactic:
apply IsPrefix.of
State after:
case idx_eq
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ ∀ (idx : Nat) (h : idx < aig.decls.size), (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]

case size_le
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size

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

case size_le
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
Tactic:
. intro idx h
  apply ofBoolExprCached.go_decl_eq
State after:
case size_le
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size

State before:
case size_le
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
Tactic:
. apply ofBoolExprCached.go_decls_size_le
State after:
no goals

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

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

State before:
case size_le
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
Tactic:
apply ofBoolExprCached.go_decls_size_le
State after:
no goals