Polynomial-time case analysis on circuit gates

Unlike formula nodes, AND and OR gates carry two binary wire indices and NOT carries one. Dispatch retains those payloads and charges for copying them.

def MIPRE.SAT.GateDispatch.callPayload (d : ℕ) (F : Cost.Prog) : Cost.Prog

Equations

• MIPRE.SAT.GateDispatch.callPayload d F = ((MIPRE.Cost.Prog.var (d + 2)).cons (MIPRE.Cost.Prog.var (d + 1))).let_ F

def MIPRE.SAT.GateDispatch.rest4 (Fn : Cost.Prog) : Cost.Prog

Equations

• MIPRE.SAT.GateDispatch.rest4 Fn = MIPRE.Cost.Prog.elim 1 (MIPRE.SAT.GateDispatch.callPayload 8 Fn) MIPRE.Cost.Prog.nil

def MIPRE.SAT.GateDispatch.rest3 (Fo Fn : Cost.Prog) : Cost.Prog

Equations

• MIPRE.SAT.GateDispatch.rest3 Fo Fn = MIPRE.Cost.Prog.elim 1 (MIPRE.SAT.GateDispatch.callPayload 6 Fo) (MIPRE.SAT.GateDispatch.rest4 Fn)

def MIPRE.SAT.GateDispatch.rest2 (Fa Fo Fn : Cost.Prog) : Cost.Prog

Equations

• MIPRE.SAT.GateDispatch.rest2 Fa Fo Fn = MIPRE.Cost.Prog.elim 1 (MIPRE.SAT.GateDispatch.callPayload 4 Fa) (MIPRE.SAT.GateDispatch.rest3 Fo Fn)

def MIPRE.SAT.GateDispatch.rest1 (Fc Fa Fo Fn : Cost.Prog) : Cost.Prog

Equations

• MIPRE.SAT.GateDispatch.rest1 Fc Fa Fo Fn = MIPRE.Cost.Prog.elim 1 (MIPRE.SAT.GateDispatch.callPayload 2 Fc) (MIPRE.SAT.GateDispatch.rest2 Fa Fo Fn)

def MIPRE.SAT.GateDispatch.tag (Fi Fc Fa Fo Fn : Cost.Prog) : Cost.Prog

Equations

• MIPRE.SAT.GateDispatch.tag Fi Fc Fa Fo Fn = MIPRE.Cost.Prog.elim 0 (MIPRE.SAT.GateDispatch.callPayload 0 Fi) (MIPRE.SAT.GateDispatch.rest1 Fc Fa Fo Fn)

def MIPRE.SAT.GateDispatch.program (Fi Fc Fa Fo Fn : Cost.Prog) : Cost.Prog

Equations

• MIPRE.SAT.GateDispatch.program Fi Fc Fa Fo Fn = MIPRE.Cost.Prog.elim 0 MIPRE.Cost.Prog.nil (MIPRE.Cost.Prog.elim 1 MIPRE.Cost.Prog.nil (MIPRE.SAT.GateDispatch.tag Fi Fc Fa Fo Fn))

theorem MIPRE.SAT.GateDispatch.program_closed {Fi Fc Fa Fo Fn : Cost.Prog} (hi : Cost.Prog.WellScoped 1 Fi) (hc : Cost.Prog.WellScoped 1 Fc) (ha : Cost.Prog.WellScoped 1 Fa) (ho : Cost.Prog.WellScoped 1 Fo) (hn : Cost.Prog.WellScoped 1 Fn) : Cost.Prog.WellScoped 1 (program Fi Fc Fa Fo Fn)

theorem MIPRE.SAT.GateDispatch.program_input {Fi Fc Fa Fo Fn : Cost.Prog} (hf : Cost.Prog.WellScoped 1 Fi) (ea : Cost.Data) (i : ℕ) {r : Cost.Data} {t : ℕ} (h : Cost.Eval [ea.cons (Cost.encode i)] Fi r t) : Cost.Eval [ea.cons (Cost.encode (Gate.input i))] (program Fi Fc Fa Fo Fn) r (ea.size + Cost.esize i + t + 7)

theorem MIPRE.SAT.GateDispatch.program_const {Fi Fc Fa Fo Fn : Cost.Prog} (hf : Cost.Prog.WellScoped 1 Fc) (ea : Cost.Data) (b : Bool) {r : Cost.Data} {t : ℕ} (h : Cost.Eval [ea.cons (Cost.encode b)] Fc r t) : Cost.Eval [ea.cons (Cost.encode (Gate.const b))] (program Fi Fc Fa Fo Fn) r (ea.size + Cost.esize b + t + 8)

theorem MIPRE.SAT.GateDispatch.program_and {Fi Fc Fa Fo Fn : Cost.Prog} (hf : Cost.Prog.WellScoped 1 Fa) (ea : Cost.Data) (u v : ℕ) {r : Cost.Data} {t : ℕ} (h : Cost.Eval [ea.cons (Cost.encode (u, v))] Fa r t) : Cost.Eval [ea.cons (Cost.encode (Gate.and u v))] (program Fi Fc Fa Fo Fn) r (ea.size + Cost.esize (u, v) + t + 9)

theorem MIPRE.SAT.GateDispatch.program_or {Fi Fc Fa Fo Fn : Cost.Prog} (hf : Cost.Prog.WellScoped 1 Fo) (ea : Cost.Data) (u v : ℕ) {r : Cost.Data} {t : ℕ} (h : Cost.Eval [ea.cons (Cost.encode (u, v))] Fo r t) : Cost.Eval [ea.cons (Cost.encode (Gate.or u v))] (program Fi Fc Fa Fo Fn) r (ea.size + Cost.esize (u, v) + t + 10)

theorem MIPRE.SAT.GateDispatch.program_not {Fi Fc Fa Fo Fn : Cost.Prog} (hf : Cost.Prog.WellScoped 1 Fn) (ea : Cost.Data) (u : ℕ) {r : Cost.Data} {t : ℕ} (h : Cost.Eval [ea.cons (Cost.encode u)] Fn r t) : Cost.Eval [ea.cons (Cost.encode (Gate.not u))] (program Fi Fc Fa Fo Fn) r (ea.size + Cost.esize u + t + 11)

def MIPRE.SAT.PolyTimeFun.casesGateFun {α : Type u_1} {β : Type u_2} (Fi Fn : α × ℕ → β) (Fc : α × Bool → β) (Fa Fo : α × ℕ × ℕ → β) : α × Gate → β

The mathematical branch dispatcher, retaining every gate's payload.

Equations

• MIPRE.SAT.PolyTimeFun.casesGateFun Fi Fn Fc Fa Fo (a, MIPRE.SAT.Gate.input i) = Fi (a, i)
• MIPRE.SAT.PolyTimeFun.casesGateFun Fi Fn Fc Fa Fo (a, MIPRE.SAT.Gate.const b) = Fc (a, b)
• MIPRE.SAT.PolyTimeFun.casesGateFun Fi Fn Fc Fa Fo (a, MIPRE.SAT.Gate.and u v) = Fa (a, u, v)
• MIPRE.SAT.PolyTimeFun.casesGateFun Fi Fn Fc Fa Fo (a, MIPRE.SAT.Gate.or u v) = Fo (a, u, v)
• MIPRE.SAT.PolyTimeFun.casesGateFun Fi Fn Fc Fa Fo (a, MIPRE.SAT.Gate.not u) = Fn (a, u)

noncomputable def MIPRE.SAT.PolyTimeFun.casesGate {α : Type u_1} {β : Type u_2} [Cost.SizedEncoding α] [Cost.SizedEncoding β] (Fi : Cost.PolyTimeFun (α × ℕ) β) (Fc : Cost.PolyTimeFun (α × Bool) β) (Fa Fo : Cost.PolyTimeFun (α × ℕ × ℕ) β) (Fn : Cost.PolyTimeFun (α × ℕ) β) : Cost.PolyTimeFun (α × Gate) β

Uniform ambient case analysis on a circuit gate.

Equations

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