class Std.Sat.AIG.RefVec.LawfulMapOperator (α : Type) [Hashable α] [DecidableEq α] (f : (aig : AIG α) → aig.Ref → Entrypoint α) [LawfulOperator α Ref f] : Prop

• chainable (aig : AIG α) (input1 input2 : aig.Ref) (h : aig.decls.size ≤ (f aig input1).aig.decls.size) (assign : α → Bool) : ⟦assign, f (f aig input1).aig (input2.cast h)⟧ = ⟦assign, f aig input2⟧

@[deprecated Std.Sat.AIG.RefVec.LawfulMapOperator.chainable (since := "2025-10-29")]

theorem Std.Sat.AIG.RefVec.LawfulMapOperator.denote_prefix_cast_ref {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : AIG α} {input1 input2 : aig.Ref} {f : (aig : AIG α) → aig.Ref → Entrypoint α} [LawfulOperator α Ref f] [LawfulMapOperator α f] {h : aig.decls.size ≤ (f aig input1).aig.decls.size} : ⟦assign, f (f aig input1).aig (input2.cast h)⟧ = ⟦assign, f aig input2⟧

instance Std.Sat.AIG.RefVec.LawfulMapOperator.instMkNotCached {α : Type} [Hashable α] [DecidableEq α] : LawfulMapOperator α mkNotCached

structure Std.Sat.AIG.RefVec.MapTarget {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (len : Nat) : Type

• vec : aig.RefVec len
• func (aig : AIG α) : aig.Ref → Entrypoint α
• lawful : LawfulOperator α Ref self.func
• chainable : LawfulMapOperator α self.func

@[specialize #[]]

def Std.Sat.AIG.RefVec.map {α : Type} [Hashable α] [DecidableEq α] {len : Nat} (aig : AIG α) (target : MapTarget aig len) : RefVecEntry α len

Equations

• Std.Sat.AIG.RefVec.map aig target = Std.Sat.AIG.RefVec.map.go aig 0 ⋯ (Std.Sat.AIG.RefVec.emptyWithCapacity len) target.vec target.func

@[irreducible, specialize #[]]

def Std.Sat.AIG.RefVec.map.go {α : Type} [Hashable α] [DecidableEq α] {len : Nat} (aig : AIG α) (idx : Nat) (hidx : idx ≤ len) (s : aig.RefVec idx) (input : aig.RefVec len) (f : (aig : AIG α) → aig.Ref → Entrypoint α) [LawfulOperator α Ref f] [LawfulMapOperator α f] : RefVecEntry α len

Equations

• One or more equations did not get rendered due to their size.

theorem Std.Sat.AIG.RefVec.map.go_le_size {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : AIG α} (idx : Nat) (hidx : idx ≤ len) (s : aig.RefVec idx) (input : aig.RefVec len) (f : (aig : AIG α) → aig.Ref → Entrypoint α) [LawfulOperator α Ref f] [LawfulMapOperator α f] : aig.decls.size ≤ (go aig idx hidx s input f).aig.decls.size

theorem Std.Sat.AIG.RefVec.map_le_size {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : AIG α} (target : MapTarget aig len) : aig.decls.size ≤ (map aig target).aig.decls.size

theorem Std.Sat.AIG.RefVec.map.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : AIG α} (i : Nat) (hi : i ≤ len) (s : aig.RefVec i) (input : aig.RefVec len) (f : (aig : AIG α) → aig.Ref → Entrypoint α) [LawfulOperator α Ref f] [LawfulMapOperator α f] (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go aig i hi s input f).aig.decls.size) : (go aig i hi s input f).aig.decls[idx] = aig.decls[idx]

theorem Std.Sat.AIG.RefVec.map_decl_eq {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : AIG α} (target : MapTarget aig len) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (map aig target).aig.decls.size) : (map aig target).aig.decls[idx] = aig.decls[idx]

instance Std.Sat.AIG.RefVec.instLawfulVecOperatorMapTargetMap {α : Type} [Hashable α] [DecidableEq α] : LawfulVecOperator α MapTarget fun {len : Nat} => map

theorem Std.Sat.AIG.RefVec.map.go_get_aux {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : aig.RefVec curr) (input : aig.RefVec len) (f : (aig : AIG α) → aig.Ref → Entrypoint α) [LawfulOperator α Ref f] [LawfulMapOperator α f] (idx : Nat) (hidx : idx < curr) (hfoo : aig.decls.size ≤ (go aig curr hcurr s input f).aig.decls.size) : (go aig curr hcurr s input f).vec.get idx ⋯ = (s.get idx hidx).cast hfoo

theorem Std.Sat.AIG.RefVec.map.go_get {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : aig.RefVec curr) (input : aig.RefVec len) (f : (aig : AIG α) → aig.Ref → Entrypoint α) [LawfulOperator α Ref f] [LawfulMapOperator α f] (idx : Nat) (hidx : idx < curr) : (go aig curr hcurr s input f).vec.get idx ⋯ = (s.get idx hidx).cast ⋯

theorem Std.Sat.AIG.RefVec.map.go_denote_mem_prefix {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {assign : α → Bool} {inv : Bool} {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : aig.RefVec curr) (input : aig.RefVec len) (f : (aig : AIG α) → aig.Ref → Entrypoint α) [LawfulOperator α Ref f] [LawfulMapOperator α f] (start : Nat) (hstart : start < aig.decls.size) : ⟦assign, { aig := (go aig curr hcurr s input f).aig, ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ = ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧

theorem Std.Sat.AIG.RefVec.map.denote_go {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {assign : α → Bool} {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : aig.RefVec curr) (input : aig.RefVec len) (f : (aig : AIG α) → aig.Ref → Entrypoint α) [LawfulOperator α Ref f] [LawfulMapOperator α f] (idx : Nat) (hidx1 : idx < len) : curr ≤ idx → ⟦assign, { aig := (go aig curr hcurr s input f).aig, ref := (go aig curr hcurr s input f).vec.get idx hidx1 }⟧ = ⟦assign, f aig (input.get idx hidx1)⟧

@[simp]

theorem Std.Sat.AIG.RefVec.denote_map {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {assign : α → Bool} {aig : AIG α} (target : MapTarget aig len) (idx : Nat) (hidx : idx < len) : ⟦assign, { aig := (map aig target).aig, ref := (map aig target).vec.get idx hidx }⟧ = ⟦assign, target.func aig (target.vec.get idx hidx)⟧