class
Std.Sat.AIG.LawfulVecOperator
(α : Type)
[Hashable α]
[DecidableEq α]
(β : AIG α → Nat → Type)
(f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len)
:
Instances
theorem
Std.Sat.AIG.LawfulVecOperator.isPrefix_aig
{α : Type}
[Hashable α]
[DecidableEq α]
{β : AIG α → Nat → Type}
{f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len}
[LawfulVecOperator α β fun {len : Nat} => f]
{len : Nat}
(aig : AIG α)
(input : β aig len)
:
theorem
Std.Sat.AIG.LawfulVecOperator.lt_size
{α : Type}
[Hashable α]
[DecidableEq α]
{β : AIG α → Nat → Type}
{f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len}
[LawfulVecOperator α β fun {len : Nat} => f]
{len : Nat}
(entry : Entrypoint α)
(input : β entry.aig len)
:
theorem
Std.Sat.AIG.LawfulVecOperator.lt_size_of_lt_aig_size
{α : Type}
[Hashable α]
[DecidableEq α]
{β : AIG α → Nat → Type}
{f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len}
[LawfulVecOperator α β fun {len : Nat} => f]
{len x : Nat}
(aig : AIG α)
(input : β aig len)
(h : x < aig.decls.size)
:
theorem
Std.Sat.AIG.LawfulVecOperator.le_size_of_le_aig_size
{α : Type}
[Hashable α]
[DecidableEq α]
{β : AIG α → Nat → Type}
{f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len}
[LawfulVecOperator α β fun {len : Nat} => f]
{len x : Nat}
(aig : AIG α)
(input : β aig len)
(h : x ≤ aig.decls.size)
:
@[simp]
theorem
Std.Sat.AIG.LawfulVecOperator.denote_input_entry
{α : Type}
[Hashable α]
[DecidableEq α]
{β : AIG α → Nat → Type}
{f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len}
[LawfulVecOperator α β fun {len : Nat} => f]
{len : Nat}
{assign : α → Bool}
(entry : Entrypoint α)
{input : β entry.aig len}
{h : entry.ref.gate < (f entry.aig input).aig.decls.size}
:
@[simp]
theorem
Std.Sat.AIG.LawfulVecOperator.denote_cast_entry
{α : Type}
[Hashable α]
[DecidableEq α]
{β : AIG α → Nat → Type}
{f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len}
[LawfulVecOperator α β fun {len : Nat} => f]
{len : Nat}
{assign : α → Bool}
(entry : Entrypoint α)
{input : β entry.aig len}
{h : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size}
:
theorem
Std.Sat.AIG.LawfulVecOperator.denote_mem_prefix
{α : Type}
[Hashable α]
[DecidableEq α]
{β : AIG α → Nat → Type}
{f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len}
[LawfulVecOperator α β fun {len : Nat} => f]
{len : Nat}
{assign : α → Bool}
{start : Nat}
{aig : AIG α}
{input : β aig len}
(h : start < aig.decls.size)
:
@[simp]
theorem
Std.Sat.AIG.LawfulVecOperator.denote_input_vec
{α : Type}
[Hashable α]
[DecidableEq α]
{β : AIG α → Nat → Type}
{f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len}
[LawfulVecOperator α β fun {len : Nat} => f]
{len : Nat}
{assign : α → Bool}
{idx : Nat}
{hidx : idx < len}
(s : RefVecEntry α len)
{input : β s.aig len}
{hcast : s.aig.decls.size ≤ (f s.aig input).aig.decls.size}
: