Negations only at primary inputs

The ambient unbounded AND/OR signature permits a negation on any argument. This predicate restricts a CSLib circuit to the paper's convention: only primary input wires may be negated. The layer compiler preserves it.

def Complexity.Shallow.ProgramInputNegationsOnly {n g : ℕ} : Cslib.Circuits.Program Basis.unboundedAndOr.signature n g → Prop

Every negated argument in a program reads a primary input.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.Shallow.ProgramInputNegationsOnly Cslib.Circuits.Program.empty = True

def Complexity.Shallow.InputNegationsOnly {n m : ℕ} (c : Cslib.Circuits.Circuit Basis.unboundedAndOr.signature n m) : Prop

A CSLib circuit in negation normal form, with negations only at inputs.

Equations

• Complexity.Shallow.InputNegationsOnly c = Complexity.Shallow.ProgramInputNegationsOnly c.program

theorem Complexity.Shallow.ProgramInputNegationsOnly.append {n g h : ℕ} {p : Cslib.Circuits.Program Basis.unboundedAndOr.signature n g} {q : Cslib.Circuits.Program Basis.unboundedAndOr.signature n h} (hp : ProgramInputNegationsOnly p) (hq : ProgramInputNegationsOnly q) : ProgramInputNegationsOnly (p.append Cslib.Circuits.Wire.input q)

Parallel continuation preserves input-only negations.

theorem Complexity.Shallow.InputNegationsOnly.append {n m r : ℕ} {c : Cslib.Circuits.Circuit Basis.unboundedAndOr.signature n m} {e : Cslib.Circuits.Circuit Basis.unboundedAndOr.signature n r} (hc : InputNegationsOnly c) (he : InputNegationsOnly e) : InputNegationsOnly (c.append e)

Parallel circuits preserve input-only negations.