The transcription: SAT ≤ᶠᵒ[≤] NTMAccept

The first-order half of the reduction. The machine of a CNF formula was built semantically in DescriptiveComplexity.Problems.Machine.Hardness – plain predicates on tagged tuples, with its correctness DescriptiveComplexity.satMachine_accepts_iff_satisfiable proved there. This file writes the defining formulas of an interpretation of Language.turing in ordered CNF instances, shows each formula realizes exactly the corresponding predicate of the machine, and bundles the result as the ordered first-order reduction DescriptiveComplexity.SatTM.sat_ordered_fo_reduction_ntmAccept.

Method

Everything is arranged so that no simp call ever faces a tag match:

• the binary symbols' formulas are written through two shape helpers – cstF s (“the second argument is the constant element pinned to the minima”) and oneF s x (“the second argument carries the tag s and the payload held by the variable x”) – matching the two shapes DescriptiveComplexity.cst and DescriptiveComplexity.one every state, symbol and transition of the machine has; each has one realization lemma, so each defining formula needs a match on its first tag only;
• realization lemmas take the valuation abstractly, with the values of the needed variables as equation hypotheses; at the call sites these are discharged by rfl, since the interpreted valuation reduces definitionally on concrete tags.

The transfer to DescriptiveComplexity.NTMAccept is then a fieldwise DescriptiveComplexity.TMData.Agree along the identity equivalence: the machine the interpreted structure describes agrees with DescriptiveComplexity.satMachine, so acceptance and well-formedness transport, and correctness is inherited from the semantic layer.

Formulas for the clause order

noncomputable def DescriptiveComplexity.SatTM.minClF {α : Type} (c : α) : SatOcc.satOrd.Formula α

c is the lowest clause, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.SatTM.maxClF {α : Type} (c : α) : SatOcc.satOrd.Formula α

c is the highest clause, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.SatTM.nextClF {α : Type} (c c' : α) : SatOcc.satOrd.Formula α

c' is the clause immediately above c, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.SatTM.noClF {α : Type} : SatOcc.satOrd.Formula α

There is no clause at all, as a formula.

Equations

• DescriptiveComplexity.SatTM.noClF = FirstOrder.Language.Formula.iAlls Unit (FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.SatOcc.clF (Sum.inr ())))

theorem DescriptiveComplexity.SatTM.realize_minClF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {x : α} {c : A} (h : v x = c) : (minClF x).Realize v ↔ SatMinCl c

theorem DescriptiveComplexity.SatTM.realize_maxClF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {x : α} {c : A} (h : v x = c) : (maxClF x).Realize v ↔ SatMaxCl c

theorem DescriptiveComplexity.SatTM.realize_nextClF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {x y : α} {c c' : A} (hx : v x = c) (hy : v y = c') : (nextClF x y).Realize v ↔ SatNextCl c c'

theorem DescriptiveComplexity.SatTM.realize_noClF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} : noClF.Realize v ↔ ∀ (e : A), ¬SatCl e

The two shapes of the machine's elements, as formulas

noncomputable def DescriptiveComplexity.SatTM.cstF (s t' : SatTag) : SatOcc.satOrd.Formula (Fin 2 × Fin 2)

The second argument of a binary symbol is the constant element cst s: its tag is s – checked statically – and its payload is the pair of minima.

Equations

• DescriptiveComplexity.SatTM.cstF s t' = if t' = s then DescriptiveComplexity.minF (1, 0) ⊓ DescriptiveComplexity.minF (1, 1) else ⊥

noncomputable def DescriptiveComplexity.SatTM.oneF (s : SatTag) (x : Fin 2 × Fin 2) (t' : SatTag) : SatOcc.satOrd.Formula (Fin 2 × Fin 2)

The second argument of a binary symbol is one s (v x): its tag is s, its payload carries the value of the variable x and the minimum.

Equations

• DescriptiveComplexity.SatTM.oneF s x t' = if t' = s then DescriptiveComplexity.SatOcc.eqF (1, 0) x ⊓ DescriptiveComplexity.minF (1, 1) else ⊥

theorem DescriptiveComplexity.SatTM.realize_cstF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {v : Fin 2 × Fin 2 → A} {s : SatTag} {q : SatV A} (h0 : v (1, 0) = q.2 0) (h1 : v (1, 1) = q.2 1) : (cstF s q.1).Realize v ↔ q = cst s

theorem DescriptiveComplexity.SatTM.realize_oneF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {v : Fin 2 × Fin 2 → A} {s : SatTag} {x : Fin 2 × Fin 2} {q : SatV A} (h0 : v (1, 0) = q.2 0) (h1 : v (1, 1) = q.2 1) : (oneF s x q.1).Realize v ↔ q = one s (v x)

The defining formulas

noncomputable def DescriptiveComplexity.SatTM.chkLitF (b : Bool) : SatOcc.satOrd.Formula (Fin 2 × Fin 2)

The literal test on the source structure, for the statically known truth value v: this is where the transition relation reads the input formula.

Equations

• DescriptiveComplexity.SatTM.chkLitF b = if b = true then DescriptiveComplexity.SatOcc.posF (0, 0) (0, 1) else DescriptiveComplexity.SatOcc.negF (0, 0) (0, 1)

noncomputable def DescriptiveComplexity.SatTM.posnF : SatTag → SatOcc.satOrd.Formula (Fin 1 × Fin 2)

Defining formula for posn.

Equations

• DescriptiveComplexity.SatTM.posnF DescriptiveComplexity.SatTag.pStart = DescriptiveComplexity.minF (0, 0) ⊓ DescriptiveComplexity.minF (0, 1)
• DescriptiveComplexity.SatTM.posnF DescriptiveComplexity.SatTag.pCell = DescriptiveComplexity.minF (0, 1)
• DescriptiveComplexity.SatTM.posnF DescriptiveComplexity.SatTag.pEnd = DescriptiveComplexity.minF (0, 0) ⊓ DescriptiveComplexity.minF (0, 1)
• DescriptiveComplexity.SatTM.posnF (DescriptiveComplexity.SatTag.pFill i) = ⊤
• DescriptiveComplexity.SatTM.posnF x✝ = ⊥

noncomputable def DescriptiveComplexity.SatTM.trF : SatTag → SatOcc.satOrd.Formula (Fin 1 × Fin 2)

Defining formula for tr: the payload promises of DescriptiveComplexity.SatTr.

Equations

• DescriptiveComplexity.SatTM.trF DescriptiveComplexity.SatTag.tGuessStart = DescriptiveComplexity.minF (0, 0) ⊓ DescriptiveComplexity.minF (0, 1)
• DescriptiveComplexity.SatTM.trF (DescriptiveComplexity.SatTag.tGuessVal b) = DescriptiveComplexity.minF (0, 1)
• DescriptiveComplexity.SatTM.trF DescriptiveComplexity.SatTag.tGuessEndAcc = DescriptiveComplexity.minF (0, 0) ⊓ DescriptiveComplexity.minF (0, 1) ⊓ DescriptiveComplexity.SatTM.noClF
• DescriptiveComplexity.SatTM.trF DescriptiveComplexity.SatTag.tGuessEndChk = DescriptiveComplexity.minF (0, 1) ⊓ DescriptiveComplexity.SatTM.minClF (0, 0)
• DescriptiveComplexity.SatTM.trF (DescriptiveComplexity.SatTag.tChk b f d) = DescriptiveComplexity.SatOcc.clF (0, 0)
• DescriptiveComplexity.SatTM.trF (DescriptiveComplexity.SatTag.tTurnNext d) = DescriptiveComplexity.SatTM.nextClF (0, 0) (0, 1)
• DescriptiveComplexity.SatTM.trF (DescriptiveComplexity.SatTag.tTurnAcc d) = DescriptiveComplexity.minF (0, 1) ⊓ DescriptiveComplexity.SatTM.maxClF (0, 0)
• DescriptiveComplexity.SatTM.trF x✝ = ⊥

noncomputable def DescriptiveComplexity.SatTM.startF : SatTag → SatOcc.satOrd.Formula (Fin 1 × Fin 2)

Defining formula for start.

Equations

• DescriptiveComplexity.SatTM.startF DescriptiveComplexity.SatTag.qGuess = DescriptiveComplexity.minF (0, 0) ⊓ DescriptiveComplexity.minF (0, 1)
• DescriptiveComplexity.SatTM.startF x✝ = ⊥

noncomputable def DescriptiveComplexity.SatTM.accF : SatTag → SatOcc.satOrd.Formula (Fin 1 × Fin 2)

Defining formula for acc: any payload – acceptance is read off the tag alone, exactly as DescriptiveComplexity.SatAcc does.

Equations

• DescriptiveComplexity.SatTM.accF DescriptiveComplexity.SatTag.qAcc = ⊤
• DescriptiveComplexity.SatTM.accF x✝ = ⊥

noncomputable def DescriptiveComplexity.SatTM.blankF : SatTag → SatOcc.satOrd.Formula (Fin 1 × Fin 2)

Defining formula for blank.

Equations

• DescriptiveComplexity.SatTM.blankF DescriptiveComplexity.SatTag.sBlank = DescriptiveComplexity.minF (0, 0) ⊓ DescriptiveComplexity.minF (0, 1)
• DescriptiveComplexity.SatTM.blankF x✝ = ⊥

noncomputable def DescriptiveComplexity.SatTM.rightF : SatTag → SatOcc.satOrd.Formula (Fin 1 × Fin 2)

Defining formula for right: a static condition on the tag.

Equations

• DescriptiveComplexity.SatTM.rightF DescriptiveComplexity.SatTag.tGuessStart = ⊤
• DescriptiveComplexity.SatTM.rightF (DescriptiveComplexity.SatTag.tGuessVal b) = ⊤
• DescriptiveComplexity.SatTM.rightF (DescriptiveComplexity.SatTag.tChk b f d) = if d = true then ⊤ else ⊥
• DescriptiveComplexity.SatTM.rightF (DescriptiveComplexity.SatTag.tTurnNext d) = if d = true then ⊥ else ⊤
• DescriptiveComplexity.SatTM.rightF (DescriptiveComplexity.SatTag.tTurnAcc d) = if d = true then ⊥ else ⊤
• DescriptiveComplexity.SatTM.rightF x✝ = ⊥

noncomputable def DescriptiveComplexity.SatTM.inpF : SatTag → SatTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

Defining formula for inp, the initial tape.

Equations

• DescriptiveComplexity.SatTM.inpF DescriptiveComplexity.SatTag.pStart x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.sStart x✝
• DescriptiveComplexity.SatTM.inpF DescriptiveComplexity.SatTag.pCell x✝ = DescriptiveComplexity.SatTM.oneF DescriptiveComplexity.SatTag.sU (0, 0) x✝
• DescriptiveComplexity.SatTM.inpF DescriptiveComplexity.SatTag.pEnd x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.sEnd x✝
• DescriptiveComplexity.SatTM.inpF x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.SatTM.tsrcF : SatTag → SatTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

Defining formula for tsrc.

Equations

• DescriptiveComplexity.SatTM.tsrcF DescriptiveComplexity.SatTag.tGuessStart x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.qGuess x✝
• DescriptiveComplexity.SatTM.tsrcF (DescriptiveComplexity.SatTag.tGuessVal b) x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.qGuess x✝
• DescriptiveComplexity.SatTM.tsrcF DescriptiveComplexity.SatTag.tGuessEndAcc x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.qGuess x✝
• DescriptiveComplexity.SatTM.tsrcF DescriptiveComplexity.SatTag.tGuessEndChk x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.qGuess x✝
• DescriptiveComplexity.SatTM.tsrcF (DescriptiveComplexity.SatTag.tChk b f d) x✝ = DescriptiveComplexity.SatTM.oneF (DescriptiveComplexity.SatTag.qChk f d) (0, 0) x✝
• DescriptiveComplexity.SatTM.tsrcF (DescriptiveComplexity.SatTag.tTurnNext d) x✝ = DescriptiveComplexity.SatTM.oneF (DescriptiveComplexity.SatTag.qChk true d) (0, 0) x✝
• DescriptiveComplexity.SatTM.tsrcF (DescriptiveComplexity.SatTag.tTurnAcc d) x✝ = DescriptiveComplexity.SatTM.oneF (DescriptiveComplexity.SatTag.qChk true d) (0, 0) x✝
• DescriptiveComplexity.SatTM.tsrcF x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.SatTM.treadF : SatTag → SatTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

Defining formula for tread.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SatTM.treadF DescriptiveComplexity.SatTag.tGuessStart x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.sStart x✝
• DescriptiveComplexity.SatTM.treadF (DescriptiveComplexity.SatTag.tGuessVal b) x✝ = DescriptiveComplexity.SatTM.oneF DescriptiveComplexity.SatTag.sU (0, 0) x✝
• DescriptiveComplexity.SatTM.treadF DescriptiveComplexity.SatTag.tGuessEndAcc x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.sEnd x✝
• DescriptiveComplexity.SatTM.treadF DescriptiveComplexity.SatTag.tGuessEndChk x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.sEnd x✝
• DescriptiveComplexity.SatTM.treadF x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.SatTM.tdstF : SatTag → SatTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

Defining formula for tdst: the one place the instance is consulted, in the check clause, through DescriptiveComplexity.SatTM.chkLitF.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SatTM.tdstF DescriptiveComplexity.SatTag.tGuessStart x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.qGuess x✝
• DescriptiveComplexity.SatTM.tdstF (DescriptiveComplexity.SatTag.tGuessVal b) x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.qGuess x✝
• DescriptiveComplexity.SatTM.tdstF DescriptiveComplexity.SatTag.tGuessEndAcc x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.qAcc x✝
• DescriptiveComplexity.SatTM.tdstF DescriptiveComplexity.SatTag.tGuessEndChk x✝ = DescriptiveComplexity.SatTM.oneF (DescriptiveComplexity.SatTag.qChk false false) (0, 0) x✝
• DescriptiveComplexity.SatTM.tdstF (DescriptiveComplexity.SatTag.tTurnNext d) x✝ = DescriptiveComplexity.SatTM.oneF (DescriptiveComplexity.SatTag.qChk false !d) (0, 1) x✝
• DescriptiveComplexity.SatTM.tdstF (DescriptiveComplexity.SatTag.tTurnAcc d) x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.qAcc x✝
• DescriptiveComplexity.SatTM.tdstF x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.SatTM.twriteF : SatTag → SatTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

Defining formula for twrite.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SatTM.twriteF DescriptiveComplexity.SatTag.tGuessStart x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.sStart x✝
• DescriptiveComplexity.SatTM.twriteF DescriptiveComplexity.SatTag.tGuessEndAcc x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.sEnd x✝
• DescriptiveComplexity.SatTM.twriteF DescriptiveComplexity.SatTag.tGuessEndChk x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.sEnd x✝
• DescriptiveComplexity.SatTM.twriteF x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.SatTM.satTuringInterp : FOInterpretation SatOcc.satOrd FirstOrder.Language.turing SatTag 2

The interpretation of machine instances in ordered CNF instances. The order is DescriptiveComplexity.lexLeF, so its linearity comes from DescriptiveComplexity.tagTupleOrder with no tag-pair analysis; every other symbol matches on its first tag only, the shape of the second being delegated to DescriptiveComplexity.SatTM.cstF and DescriptiveComplexity.SatTM.oneF.

Equations

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

The realization lemmas

One per symbol of Language.turing, each saying its defining formula defines the corresponding predicate of DescriptiveComplexity.satMachine. The universe of the interpreted structure is definitionally DescriptiveComplexity.SatV A; DescriptiveComplexity.SatTM.satMapEquiv names the identity equivalence, along which the machines will be shown to agree.

def DescriptiveComplexity.SatTM.satMapEquiv {A : Type} : SatV A ≃ satTuringInterp.Map A

The identity equivalence between the tagged tuples and the interpreted universe.

Equations

• DescriptiveComplexity.SatTM.satMapEquiv = Equiv.refl (DescriptiveComplexity.SatV A)

theorem DescriptiveComplexity.SatTM.relMap_posn {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : SatV A) : TMPosn (satMapEquiv p) ↔ SatPosn p

theorem DescriptiveComplexity.SatTM.relMap_tr {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : SatV A) : TMTr (satMapEquiv p) ↔ SatTr p

theorem DescriptiveComplexity.SatTM.relMap_start {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : SatV A) : TMStart (satMapEquiv p) ↔ SatStart p

theorem DescriptiveComplexity.SatTM.relMap_acc {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : SatV A) : TMAcc (satMapEquiv p) ↔ SatAcc p

theorem DescriptiveComplexity.SatTM.relMap_blank {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : SatV A) : TMBlank (satMapEquiv p) ↔ SatBlank p

theorem DescriptiveComplexity.SatTM.relMap_right {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : SatV A) : TMRight (satMapEquiv p) ↔ SatRight p

theorem DescriptiveComplexity.SatTM.relMap_le {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p q : SatV A) : TMLe (satMapEquiv p) (satMapEquiv q) ↔ tagTupleLe p q

theorem DescriptiveComplexity.SatTM.satInp_pStart_iff {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {w : Fin 2 → A} {a : SatV A} : SatInp (SatTag.pStart, w) a ↔ a = symStart

The three shapes of the initial tape, per tag of the cell.

theorem DescriptiveComplexity.SatTM.satInp_pCell_iff {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {w : Fin 2 → A} {a : SatV A} : SatInp (SatTag.pCell, w) a ↔ a = one SatTag.sU (w 0)

theorem DescriptiveComplexity.SatTM.satInp_pEnd_iff {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {w : Fin 2 → A} {a : SatV A} : SatInp (SatTag.pEnd, w) a ↔ a = symEnd

theorem DescriptiveComplexity.SatTM.relMap_inp {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (p q : SatV A) : TMInp (satMapEquiv p) (satMapEquiv q) ↔ SatInp p q

theorem DescriptiveComplexity.SatTM.relMap_tsrc {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (p q : SatV A) : TMSrc (satMapEquiv p) (satMapEquiv q) ↔ SatSrc p q

theorem DescriptiveComplexity.SatTM.relMap_tread {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (p q : SatV A) : TMRead (satMapEquiv p) (satMapEquiv q) ↔ SatRead p q

theorem DescriptiveComplexity.SatTM.relMap_twrite {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (p q : SatV A) : TMWrite (satMapEquiv p) (satMapEquiv q) ↔ SatWrite p q

theorem DescriptiveComplexity.SatTM.realize_chkLitF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {b : Bool} {c x : A} {v : Fin 2 × Fin 2 → A} (h0 : v (0, 0) = c) (h1 : v (0, 1) = x) : (chkLitF b).Realize v ↔ SatLit c x b

The check clause's new flag, realized: the literal test on the source.

theorem DescriptiveComplexity.SatTM.relMap_tdst {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (p q : SatV A) : TMDst (satMapEquiv p) (satMapEquiv q) ↔ SatDst p q

The machines agree, and the reduction

theorem DescriptiveComplexity.SatTM.agree_satMachine {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : TMData.Agree satMapEquiv (satMachine A) (tmData (satTuringInterp.Map A))

The interpreted structure describes the machine of the instance: every field of DescriptiveComplexity.tmData on the interpreted structure agrees, along the identity equivalence, with DescriptiveComplexity.satMachine.

theorem DescriptiveComplexity.SatTM.ntmAccept_map_iff_satisfiable {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : NTMAccept.Holds (satTuringInterp.Map A) ↔ Satisfiable A

Correctness of the interpretation: the interpreted structure is a yes-instance of machine acceptance exactly when the CNF instance is satisfiable. Well-formedness holds unconditionally (DescriptiveComplexity.satMachine_wellFormed), and acceptance is DescriptiveComplexity.satMachine_accepts_iff_satisfiable, both transported along the agreement.

noncomputable def DescriptiveComplexity.SatTM.sat_ordered_fo_reduction_ntmAccept : OrderedFOReduction SAT NTMAccept

SAT reduces to acceptance by a nondeterministic machine: the ordered first-order reduction building M_φ inside the instance.

Equations

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