Theorem: AIG.LawfulStreamOperator.lt_size (LeanSAT/AIG/LawfulStreamOperator.lean)

State before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
entry : Entrypoint α
input : β entry.aig len
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size
Tactic:
have h1 := entry.ref.hgate
State after:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
entry : Entrypoint α
input : β entry.aig len
h1 : entry.ref.gate < entry.aig.decls.size
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size

State before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
entry : Entrypoint α
input : β entry.aig len
h1 : entry.ref.gate < entry.aig.decls.size
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size
Tactic:
have h2 : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size := by
  apply le_size
State after:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
entry : Entrypoint α
input : β entry.aig len
h1 : entry.ref.gate < entry.aig.decls.size
h2 : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size

State before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
entry : Entrypoint α
input : β entry.aig len
h1 : entry.ref.gate < entry.aig.decls.size
h2 : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size
Tactic:
omega
State after:
no goals

State before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
entry : Entrypoint α
input : β entry.aig len
h1 : entry.ref.gate < entry.aig.decls.size
⊢ entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size
Tactic:
apply le_size
State after:
no goals