SUCCINCT-REACH is PSPACE-hard

The hardness half: every SO(TC) definable problem admits an ordered first-order reduction to SUCCINCT-REACH (DescriptiveComplexity.succinctReach_hard_of_sotcDefinable). Since DescriptiveComplexity.PSPACE is defined as SO(TC) definability, together with DescriptiveComplexity.succinctReach_mem_PSPACE this makes SUCCINCT-REACH PSPACE-complete.

The discharge, and why it is three Tseitin encodings sharing one block

A DescriptiveComplexity.SOTCSpec is a block B and three first-order sentences: a transition sentence over two copies of B and two endpoint sentences over one. The interpreted SUCCINCT-REACH instance is, group by group, the Tseitin encoding (Tseitin 1968) of those sentences – the very construction that discharges ∃SO into SAT (DescriptiveComplexity.sat_hard_of_sigmaSODefinable), reused wholesale through its semantic interface DescriptiveComplexity.Tseitin.satCond_iff_gates.

The one thing that is not three independent encodings is the block: all three are taken over the doubled block B.double (DescriptiveComplexity.Problems.SuccinctReach.Double), the endpoint sentences being renamed into its first copy. That is forced, and it is the heart of the construction: the propositional variables standing for the atoms of the block must be the same elements in the three clause groups, since they are exactly the state variables the walk carries. So

• an atom (i, x̄) of the first copy is a state variable, marked by stateVar;
• the atom (i, x̄) of the second copy is its next-state copy, paired to it by next;
• the gates of each encoding are auxiliary variables, private to their group.

A state of the interpreted transition system is then a set of atoms of the first copy, i.e. an assignment of B – the state of the SO(TC) walk – and the transition clauses hold of a valuation exactly when the transition sentence holds of the pair it reads and writes. The correspondence between the two walks is a bijection at every step, with no initialization or finalization steps to peel off, which is why the endpoint conditions are kept as two extra clause groups rather than folded into the transition.

Junk

Only the canonically padded tuples carry meaning, as in the SAT discharge: tuples of length DescriptiveComplexity.srDim are padded with minimal elements of the order, and a clause mentions no variable at a non-canonical tuple. But stateVar and next are declared at every tuple, canonical or not. Junk state variables are then free-running copies whose values no clause constrains and no reading of a state ever looks at (DescriptiveComplexity.srPredOf reads the canonical padding only), so they cost nothing and save the canonicity guards.

The three kernels, over the doubled block

noncomputable def DescriptiveComplexity.SuccinctReachHard.stepK {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) : ((L.sum FirstOrder.Language.order).sum B.double.lang).Sentence

The transition sentence, read over the doubled block.

Equations

• DescriptiveComplexity.SuccinctReachHard.stepK B stepS = (DescriptiveComplexity.blockPairLHom B).onSentence stepS

noncomputable def DescriptiveComplexity.SuccinctReachHard.srcK {L : FirstOrder.Language} (B : SOBlock) (srcS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) : ((L.sum FirstOrder.Language.order).sum B.double.lang).Sentence

The source sentence, read over the doubled block (first copy only).

Equations

• DescriptiveComplexity.SuccinctReachHard.srcK B srcS = (DescriptiveComplexity.blockFstLHom B).onSentence srcS

noncomputable def DescriptiveComplexity.SuccinctReachHard.tgtK {L : FirstOrder.Language} (B : SOBlock) (tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) : ((L.sum FirstOrder.Language.order).sum B.double.lang).Sentence

The target sentence, read over the doubled block (first copy only).

Equations

• DescriptiveComplexity.SuccinctReachHard.tgtK B tgtS = (DescriptiveComplexity.blockFstLHom B).onSentence tgtS

noncomputable def DescriptiveComplexity.SuccinctReachHard.srDim {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) : ℕ

The dimension of the interpretation: large enough for every context tuple of the three kernels and every argument tuple of a block variable.

Equations

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

theorem DescriptiveComplexity.SuccinctReachHard.ctx_step {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) : Tseitin.maxCtx (stepK B stepS) ≤ srDim B stepS srcS tgtS

theorem DescriptiveComplexity.SuccinctReachHard.ctx_src {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) : Tseitin.maxCtx (srcK B srcS) ≤ srDim B stepS srcS tgtS

theorem DescriptiveComplexity.SuccinctReachHard.ctx_tgt {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) : Tseitin.maxCtx (tgtK B tgtS) ≤ srDim B stepS srcS tgtS

theorem DescriptiveComplexity.SuccinctReachHard.arity_le_srDim {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) (i : B.double.ι) : B.double.arity i ≤ srDim B stepS srcS tgtS

Tags

@[reducible, inline]

abbrev DescriptiveComplexity.SuccinctReachHard.StepNode {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) : Type

Subformula positions of the transition kernel.

Equations

• DescriptiveComplexity.SuccinctReachHard.StepNode B stepS = ((m : ℕ) × DescriptiveComplexity.Tseitin.NodeAt (DescriptiveComplexity.SuccinctReachHard.stepK B stepS) m)

@[reducible, inline]

abbrev DescriptiveComplexity.SuccinctReachHard.SrcNode {L : FirstOrder.Language} (B : SOBlock) (srcS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) : Type

Subformula positions of the source kernel.

Equations

• DescriptiveComplexity.SuccinctReachHard.SrcNode B srcS = ((m : ℕ) × DescriptiveComplexity.Tseitin.NodeAt (DescriptiveComplexity.SuccinctReachHard.srcK B srcS) m)

@[reducible, inline]

abbrev DescriptiveComplexity.SuccinctReachHard.TgtNode {L : FirstOrder.Language} (B : SOBlock) (tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) : Type

Subformula positions of the target kernel.

Equations

• DescriptiveComplexity.SuccinctReachHard.TgtNode B tgtS = ((m : ℕ) × DescriptiveComplexity.Tseitin.NodeAt (DescriptiveComplexity.SuccinctReachHard.tgtK B tgtS) m)

@[reducible, inline]

abbrev DescriptiveComplexity.SuccinctReachHard.SRTag {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) : Type

The tags of the interpretation: the clauses of the three Tseitin encodings (one per position and kind, plus the top unit clause of each group), then the propositional variables – the shared atoms of the doubled block, and the gates of each group.

Equations

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

instance DescriptiveComplexity.SuccinctReachHard.instNonemptySRTag {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) : Nonempty (SRTag B stepS srcS tgtS)

@[reducible, inline]

abbrev DescriptiveComplexity.SuccinctReachHard.tagStepCl {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} (σp : StepNode B stepS) (k : Fin 3) : SRTag B stepS srcS tgtS

The clause of the transition group at a position and kind.

Equations

• DescriptiveComplexity.SuccinctReachHard.tagStepCl σp k = Sum.inl (Sum.inl (Sum.inl (σp, k)))

@[reducible, inline]

abbrev DescriptiveComplexity.SuccinctReachHard.tagStepTop {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} : SRTag B stepS srcS tgtS

The top unit clause of the transition group.

Equations

• DescriptiveComplexity.SuccinctReachHard.tagStepTop = Sum.inl (Sum.inl (Sum.inr ()))

@[reducible, inline]

abbrev DescriptiveComplexity.SuccinctReachHard.tagSrcCl {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} (σp : SrcNode B srcS) (k : Fin 3) : SRTag B stepS srcS tgtS

The clause of the source group at a position and kind.

Equations

• DescriptiveComplexity.SuccinctReachHard.tagSrcCl σp k = Sum.inl (Sum.inr (Sum.inl (Sum.inl (σp, k))))

@[reducible, inline]

abbrev DescriptiveComplexity.SuccinctReachHard.tagSrcTop {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} : SRTag B stepS srcS tgtS

The top unit clause of the source group.

Equations

• DescriptiveComplexity.SuccinctReachHard.tagSrcTop = Sum.inl (Sum.inr (Sum.inl (Sum.inr ())))

@[reducible, inline]

abbrev DescriptiveComplexity.SuccinctReachHard.tagTgtCl {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} (σp : TgtNode B tgtS) (k : Fin 3) : SRTag B stepS srcS tgtS

The clause of the target group at a position and kind.

Equations

• DescriptiveComplexity.SuccinctReachHard.tagTgtCl σp k = Sum.inl (Sum.inr (Sum.inr (Sum.inl (σp, k))))

@[reducible, inline]

abbrev DescriptiveComplexity.SuccinctReachHard.tagTgtTop {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} : SRTag B stepS srcS tgtS

The top unit clause of the target group.

Equations

• DescriptiveComplexity.SuccinctReachHard.tagTgtTop = Sum.inl (Sum.inr (Sum.inr (Sum.inr ())))

@[reducible, inline]

abbrev DescriptiveComplexity.SuccinctReachHard.tagAtom {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} (i : B.double.ι) : SRTag B stepS srcS tgtS

The propositional variable of an atom of the doubled block: a state variable for the first copy, its next-state copy for the second.

Equations

• DescriptiveComplexity.SuccinctReachHard.tagAtom i = Sum.inr (Sum.inl i)

@[reducible, inline]

abbrev DescriptiveComplexity.SuccinctReachHard.tagStepGate {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} (σp : StepNode B stepS) : SRTag B stepS srcS tgtS

A gate variable of the transition group.

Equations

• DescriptiveComplexity.SuccinctReachHard.tagStepGate σp = Sum.inr (Sum.inr (Sum.inl σp))

@[reducible, inline]

abbrev DescriptiveComplexity.SuccinctReachHard.tagSrcGate {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} (σp : SrcNode B srcS) : SRTag B stepS srcS tgtS

A gate variable of the source group.

Equations

• DescriptiveComplexity.SuccinctReachHard.tagSrcGate σp = Sum.inr (Sum.inr (Sum.inr (Sum.inl σp)))

@[reducible, inline]

abbrev DescriptiveComplexity.SuccinctReachHard.tagTgtGate {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} (σp : TgtNode B tgtS) : SRTag B stepS srcS tgtS

A gate variable of the target group.

Equations

• DescriptiveComplexity.SuccinctReachHard.tagTgtGate σp = Sum.inr (Sum.inr (Sum.inr (Sum.inr σp)))

def DescriptiveComplexity.SuccinctReachHard.stepVar {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} : B.double.ι ⊕ StepNode B stepS → SRTag B stepS srcS tgtS

The Tseitin variable tags of the transition group, as tags of the interpretation.

Equations

• DescriptiveComplexity.SuccinctReachHard.stepVar = Sum.elim DescriptiveComplexity.SuccinctReachHard.tagAtom DescriptiveComplexity.SuccinctReachHard.tagStepGate

def DescriptiveComplexity.SuccinctReachHard.srcVar {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} : B.double.ι ⊕ SrcNode B srcS → SRTag B stepS srcS tgtS

The Tseitin variable tags of the source group, as tags.

Equations

• DescriptiveComplexity.SuccinctReachHard.srcVar = Sum.elim DescriptiveComplexity.SuccinctReachHard.tagAtom DescriptiveComplexity.SuccinctReachHard.tagSrcGate

def DescriptiveComplexity.SuccinctReachHard.tgtVar {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} : B.double.ι ⊕ TgtNode B tgtS → SRTag B stepS srcS tgtS

The Tseitin variable tags of the target group, as tags.

Equations

• DescriptiveComplexity.SuccinctReachHard.tgtVar = Sum.elim DescriptiveComplexity.SuccinctReachHard.tagAtom DescriptiveComplexity.SuccinctReachHard.tagTgtGate

The defining formulas

@[reducible, inline]

abbrev DescriptiveComplexity.SuccinctReachHard.selU {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) : Fin (srDim B stepS srcS tgtS) → Fin 1 × Fin (srDim B stepS srcS tgtS)

The coordinate selector of a unary relation's single argument.

Equations

• DescriptiveComplexity.SuccinctReachHard.selU B stepS srcS tgtS j = (0, j)

@[reducible, inline]

abbrev DescriptiveComplexity.SuccinctReachHard.selA {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) : Fin (srDim B stepS srcS tgtS) → Fin 2 × Fin (srDim B stepS srcS tgtS)

The coordinate selector of a binary relation's first argument.

Equations

• DescriptiveComplexity.SuccinctReachHard.selA B stepS srcS tgtS j = (0, j)

@[reducible, inline]

abbrev DescriptiveComplexity.SuccinctReachHard.selB {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) : Fin (srDim B stepS srcS tgtS) → Fin 2 × Fin (srDim B stepS srcS tgtS)

The coordinate selector of a binary relation's second argument.

Equations

• DescriptiveComplexity.SuccinctReachHard.selB B stepS srcS tgtS j = (1, j)

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.SuccinctReachHard.mrg {L : FirstOrder.Language} {γ : Type} (φ : ((L.sum FirstOrder.Language.order).sum FirstOrder.Language.order).Formula γ) : (L.sum FirstOrder.Language.order).Formula γ

Merging the two order symbols the Tseitin builders leave behind: they add an order to the vocabulary they are given, which here is already ordered.

Equations

• DescriptiveComplexity.SuccinctReachHard.mrg φ = (DescriptiveComplexity.mergeOrdLHom L).onFormula φ

noncomputable def DescriptiveComplexity.SuccinctReachHard.srClFml {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) (t : SRTag B stepS srcS tgtS) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (srDim B stepS srcS tgtS))

The defining formula of stepCl, srcCl or tgtCl, selected by which group's clauses it should recognize: the clause-existence formulas of that group's encoding, plus the canonicity condition of its top unit clause.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SuccinctReachHard.srClFml B stepS srcS tgtS (Sum.inl (Sum.inl (Sum.inr val))) = DescriptiveComplexity.canonF 0 (DescriptiveComplexity.SuccinctReachHard.selU B stepS srcS tgtS)
• DescriptiveComplexity.SuccinctReachHard.srClFml B stepS srcS tgtS t = ⊥

noncomputable def DescriptiveComplexity.SuccinctReachHard.srSrcClFml {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) (t : SRTag B stepS srcS tgtS) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (srDim B stepS srcS tgtS))

The defining formula of srcCl.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SuccinctReachHard.srSrcClFml B stepS srcS tgtS t = ⊥

noncomputable def DescriptiveComplexity.SuccinctReachHard.srTgtClFml {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) (t : SRTag B stepS srcS tgtS) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (srDim B stepS srcS tgtS))

The defining formula of tgtCl.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SuccinctReachHard.srTgtClFml B stepS srcS tgtS t = ⊥

noncomputable def DescriptiveComplexity.SuccinctReachHard.srStateFml {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) (t : SRTag B stepS srcS tgtS) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (srDim B stepS srcS tgtS))

The defining formula of stateVar: the atoms of the first copy of the doubled block, at every tuple.

Equations

• DescriptiveComplexity.SuccinctReachHard.srStateFml B stepS srcS tgtS (Sum.inr (Sum.inl (Sum.inl val))) = ⊤
• DescriptiveComplexity.SuccinctReachHard.srStateFml B stepS srcS tgtS t = ⊥

noncomputable def DescriptiveComplexity.SuccinctReachHard.srNextFml {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) (t₁ t₂ : SRTag B stepS srcS tgtS) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (srDim B stepS srcS tgtS))

The defining formula of next: the atom of the second copy at the same relation variable and the same tuple.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SuccinctReachHard.srNextFml B stepS srcS tgtS t₁ t₂ = ⊥

noncomputable def DescriptiveComplexity.SuccinctReachHard.srLitStep {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) (s : Bool) (σp : StepNode B stepS) (k : Fin 3) (tx : SRTag B stepS srcS tgtS) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (srDim B stepS srcS tgtS))

The literals of a node clause of the transition group: an atom of the block, or a gate of that group.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SuccinctReachHard.srLitStep B stepS srcS tgtS s σp k tx = ⊥

noncomputable def DescriptiveComplexity.SuccinctReachHard.srLitStepTop {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) (s : Bool) (tx : SRTag B stepS srcS tgtS) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (srDim B stepS srcS tgtS))

The literal of the top unit clause of the transition group: its root gate, positively, at fully padded tuples.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SuccinctReachHard.srLitStepTop B stepS srcS tgtS s tx = ⊥

noncomputable def DescriptiveComplexity.SuccinctReachHard.srLitSrc {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) (s : Bool) (σp : SrcNode B srcS) (k : Fin 3) (tx : SRTag B stepS srcS tgtS) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (srDim B stepS srcS tgtS))

The literals of a node clause of the source group.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SuccinctReachHard.srLitSrc B stepS srcS tgtS s σp k tx = ⊥

noncomputable def DescriptiveComplexity.SuccinctReachHard.srLitSrcTop {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) (s : Bool) (tx : SRTag B stepS srcS tgtS) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (srDim B stepS srcS tgtS))

The literal of the top unit clause of the source group.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SuccinctReachHard.srLitSrcTop B stepS srcS tgtS s tx = ⊥

noncomputable def DescriptiveComplexity.SuccinctReachHard.srLitTgt {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) (s : Bool) (σp : TgtNode B tgtS) (k : Fin 3) (tx : SRTag B stepS srcS tgtS) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (srDim B stepS srcS tgtS))

The literals of a node clause of the target group.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SuccinctReachHard.srLitTgt B stepS srcS tgtS s σp k tx = ⊥

noncomputable def DescriptiveComplexity.SuccinctReachHard.srLitTgtTop {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) (s : Bool) (tx : SRTag B stepS srcS tgtS) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (srDim B stepS srcS tgtS))

The literal of the top unit clause of the target group.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SuccinctReachHard.srLitTgtTop B stepS srcS tgtS s tx = ⊥

noncomputable def DescriptiveComplexity.SuccinctReachHard.srLitFml {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) (s : Bool) (tc tx : SRTag B stepS srcS tgtS) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (srDim B stepS srcS tgtS))

The defining formula of posIn (s = true) and negIn (s = false), dispatching on which group's clause the first argument is.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SuccinctReachHard.srLitFml B stepS srcS tgtS s (Sum.inl (Sum.inl (Sum.inl (σp, k)))) tx = DescriptiveComplexity.SuccinctReachHard.srLitStep B stepS srcS tgtS s σp k tx
• DescriptiveComplexity.SuccinctReachHard.srLitFml B stepS srcS tgtS s (Sum.inl (Sum.inl (Sum.inr val))) tx = DescriptiveComplexity.SuccinctReachHard.srLitStepTop B stepS srcS tgtS s tx
• DescriptiveComplexity.SuccinctReachHard.srLitFml B stepS srcS tgtS s (Sum.inl (Sum.inr (Sum.inl (Sum.inr val)))) tx = DescriptiveComplexity.SuccinctReachHard.srLitSrcTop B stepS srcS tgtS s tx
• DescriptiveComplexity.SuccinctReachHard.srLitFml B stepS srcS tgtS s (Sum.inl (Sum.inr (Sum.inr (Sum.inr val)))) tx = DescriptiveComplexity.SuccinctReachHard.srLitTgtTop B stepS srcS tgtS s tx
• DescriptiveComplexity.SuccinctReachHard.srLitFml B stepS srcS tgtS s (Sum.inr val) tx = ⊥

noncomputable def DescriptiveComplexity.SuccinctReachHard.srInterp {L : FirstOrder.Language} (B : SOBlock) (stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) (srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) : FOInterpretation (L.sum FirstOrder.Language.order) FirstOrder.Language.transSys (SRTag B stepS srcS tgtS) (srDim B stepS srcS tgtS)

The interpretation: the SUCCINCT-REACH instance of an SO(TC) specification, defined inside the ordered input structure.

Equations

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

Characterization of the interpreted relations

Each relation of the interpreted instance is characterized by a semantic counterpart of its defining formula, matching on the tags exactly as the formula does – the pattern of DescriptiveComplexity.TseitinLitSem.

def DescriptiveComplexity.SuccinctReachHard.srStateSem {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} (t : SRTag B stepS srcS tgtS) : Prop

Semantic counterpart of DescriptiveComplexity.SuccinctReachHard.srStateFml.

Equations

• DescriptiveComplexity.SuccinctReachHard.srStateSem (Sum.inr (Sum.inl (Sum.inl val))) = True
• DescriptiveComplexity.SuccinctReachHard.srStateSem t = False

def DescriptiveComplexity.SuccinctReachHard.srNextSem {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} (t₁ t₂ : SRTag B stepS srcS tgtS) (u x : Fin (srDim B stepS srcS tgtS) → A) : Prop

Semantic counterpart of DescriptiveComplexity.SuccinctReachHard.srNextFml.

Equations

• DescriptiveComplexity.SuccinctReachHard.srNextSem (Sum.inr (Sum.inl (Sum.inl i))) (Sum.inr (Sum.inl (Sum.inr i'))) u x = (i = i' ∧ x = u)
• DescriptiveComplexity.SuccinctReachHard.srNextSem t₁ t₂ u x = False

def DescriptiveComplexity.SuccinctReachHard.srClSem {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (t : SRTag B stepS srcS tgtS) (u : Fin (srDim B stepS srcS tgtS) → A) : Prop

Semantic counterpart of DescriptiveComplexity.SuccinctReachHard.srClFml.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SuccinctReachHard.srClSem (Sum.inl (Sum.inl (Sum.inr val))) u = DescriptiveComplexity.Canon 0 u
• DescriptiveComplexity.SuccinctReachHard.srClSem t u = False

def DescriptiveComplexity.SuccinctReachHard.srSrcClSem {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (t : SRTag B stepS srcS tgtS) (u : Fin (srDim B stepS srcS tgtS) → A) : Prop

Semantic counterpart of DescriptiveComplexity.SuccinctReachHard.srSrcClFml.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SuccinctReachHard.srSrcClSem (Sum.inl (Sum.inr (Sum.inl (Sum.inr val)))) u = DescriptiveComplexity.Canon 0 u
• DescriptiveComplexity.SuccinctReachHard.srSrcClSem t u = False

def DescriptiveComplexity.SuccinctReachHard.srTgtClSem {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (t : SRTag B stepS srcS tgtS) (u : Fin (srDim B stepS srcS tgtS) → A) : Prop

Semantic counterpart of DescriptiveComplexity.SuccinctReachHard.srTgtClFml.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SuccinctReachHard.srTgtClSem (Sum.inl (Sum.inr (Sum.inr (Sum.inr val)))) u = DescriptiveComplexity.Canon 0 u
• DescriptiveComplexity.SuccinctReachHard.srTgtClSem t u = False

def DescriptiveComplexity.SuccinctReachHard.srLitStepSem {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (s : Bool) (σp : StepNode B stepS) (k : Fin 3) (tx : SRTag B stepS srcS tgtS) (u x : Fin (srDim B stepS srcS tgtS) → A) : Prop

Semantic counterpart of DescriptiveComplexity.SuccinctReachHard.srLitStep.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SuccinctReachHard.srLitStepSem s σp k tx u x = False

def DescriptiveComplexity.SuccinctReachHard.srLitStepTopSem {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [LinearOrder A] (s : Bool) (tx : SRTag B stepS srcS tgtS) (u x : Fin (srDim B stepS srcS tgtS) → A) : Prop

Semantic counterpart of DescriptiveComplexity.SuccinctReachHard.srLitStepTop.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SuccinctReachHard.srLitStepTopSem s tx u x = False

def DescriptiveComplexity.SuccinctReachHard.srLitSrcSem {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (s : Bool) (σp : SrcNode B srcS) (k : Fin 3) (tx : SRTag B stepS srcS tgtS) (u x : Fin (srDim B stepS srcS tgtS) → A) : Prop

Semantic counterpart of DescriptiveComplexity.SuccinctReachHard.srLitSrc.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SuccinctReachHard.srLitSrcSem s σp k tx u x = False

def DescriptiveComplexity.SuccinctReachHard.srLitSrcTopSem {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [LinearOrder A] (s : Bool) (tx : SRTag B stepS srcS tgtS) (u x : Fin (srDim B stepS srcS tgtS) → A) : Prop

Semantic counterpart of DescriptiveComplexity.SuccinctReachHard.srLitSrcTop.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SuccinctReachHard.srLitSrcTopSem s tx u x = False

def DescriptiveComplexity.SuccinctReachHard.srLitTgtSem {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (s : Bool) (σp : TgtNode B tgtS) (k : Fin 3) (tx : SRTag B stepS srcS tgtS) (u x : Fin (srDim B stepS srcS tgtS) → A) : Prop

Semantic counterpart of DescriptiveComplexity.SuccinctReachHard.srLitTgt.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SuccinctReachHard.srLitTgtSem s σp k tx u x = False

def DescriptiveComplexity.SuccinctReachHard.srLitTgtTopSem {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [LinearOrder A] (s : Bool) (tx : SRTag B stepS srcS tgtS) (u x : Fin (srDim B stepS srcS tgtS) → A) : Prop

Semantic counterpart of DescriptiveComplexity.SuccinctReachHard.srLitTgtTop.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SuccinctReachHard.srLitTgtTopSem s tx u x = False

def DescriptiveComplexity.SuccinctReachHard.srLitSem {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (s : Bool) (tc tx : SRTag B stepS srcS tgtS) (u x : Fin (srDim B stepS srcS tgtS) → A) : Prop

Semantic counterpart of DescriptiveComplexity.SuccinctReachHard.srLitFml.

Equations

• DescriptiveComplexity.SuccinctReachHard.srLitSem s (Sum.inl (Sum.inl (Sum.inl (σp, k)))) tx u x = DescriptiveComplexity.SuccinctReachHard.srLitStepSem s σp k tx u x
• DescriptiveComplexity.SuccinctReachHard.srLitSem s (Sum.inl (Sum.inl (Sum.inr val))) tx u x = DescriptiveComplexity.SuccinctReachHard.srLitStepTopSem s tx u x
• DescriptiveComplexity.SuccinctReachHard.srLitSem s (Sum.inl (Sum.inr (Sum.inl (Sum.inl (σp, k))))) tx u x = DescriptiveComplexity.SuccinctReachHard.srLitSrcSem s σp k tx u x
• DescriptiveComplexity.SuccinctReachHard.srLitSem s (Sum.inl (Sum.inr (Sum.inl (Sum.inr val)))) tx u x = DescriptiveComplexity.SuccinctReachHard.srLitSrcTopSem s tx u x
• DescriptiveComplexity.SuccinctReachHard.srLitSem s (Sum.inl (Sum.inr (Sum.inr (Sum.inl (σp, k))))) tx u x = DescriptiveComplexity.SuccinctReachHard.srLitTgtSem s σp k tx u x
• DescriptiveComplexity.SuccinctReachHard.srLitSem s (Sum.inl (Sum.inr (Sum.inr (Sum.inr val)))) tx u x = DescriptiveComplexity.SuccinctReachHard.srLitTgtTopSem s tx u x
• DescriptiveComplexity.SuccinctReachHard.srLitSem s (Sum.inr val) tx u x = False

theorem DescriptiveComplexity.SuccinctReachHard.sr_stateVar_iff {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (t : SRTag B stepS srcS tgtS) (u : Fin (srDim B stepS srcS tgtS) → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsStateVar ![(t, u)] ↔ srStateSem t

theorem DescriptiveComplexity.SuccinctReachHard.sr_next_iff {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (t₁ t₂ : SRTag B stepS srcS tgtS) (u x : Fin (srDim B stepS srcS tgtS) → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsNext ![(t₁, u), (t₂, x)] ↔ srNextSem t₁ t₂ u x

theorem DescriptiveComplexity.SuccinctReachHard.realize_srLitStep {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (s : Bool) (σp : StepNode B stepS) (k : Fin 3) (tx : SRTag B stepS srcS tgtS) (v : Fin 2 × Fin (srDim B stepS srcS tgtS) → A) : (srLitStep B stepS srcS tgtS s σp k tx).Realize v ↔ srLitStepSem s σp k tx (fun (j : Fin (srDim B stepS srcS tgtS)) => v (selA B stepS srcS tgtS j)) fun (j : Fin (srDim B stepS srcS tgtS)) => v (selB B stepS srcS tgtS j)

theorem DescriptiveComplexity.SuccinctReachHard.realize_srLitSrc {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (s : Bool) (σp : SrcNode B srcS) (k : Fin 3) (tx : SRTag B stepS srcS tgtS) (v : Fin 2 × Fin (srDim B stepS srcS tgtS) → A) : (srLitSrc B stepS srcS tgtS s σp k tx).Realize v ↔ srLitSrcSem s σp k tx (fun (j : Fin (srDim B stepS srcS tgtS)) => v (selA B stepS srcS tgtS j)) fun (j : Fin (srDim B stepS srcS tgtS)) => v (selB B stepS srcS tgtS j)

theorem DescriptiveComplexity.SuccinctReachHard.realize_srLitTgt {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (s : Bool) (σp : TgtNode B tgtS) (k : Fin 3) (tx : SRTag B stepS srcS tgtS) (v : Fin 2 × Fin (srDim B stepS srcS tgtS) → A) : (srLitTgt B stepS srcS tgtS s σp k tx).Realize v ↔ srLitTgtSem s σp k tx (fun (j : Fin (srDim B stepS srcS tgtS)) => v (selA B stepS srcS tgtS j)) fun (j : Fin (srDim B stepS srcS tgtS)) => v (selB B stepS srcS tgtS j)

theorem DescriptiveComplexity.SuccinctReachHard.realize_srLitStepTop {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (s : Bool) (tx : SRTag B stepS srcS tgtS) (v : Fin 2 × Fin (srDim B stepS srcS tgtS) → A) : (srLitStepTop B stepS srcS tgtS s tx).Realize v ↔ srLitStepTopSem s tx (fun (j : Fin (srDim B stepS srcS tgtS)) => v (selA B stepS srcS tgtS j)) fun (j : Fin (srDim B stepS srcS tgtS)) => v (selB B stepS srcS tgtS j)

theorem DescriptiveComplexity.SuccinctReachHard.realize_srLitSrcTop {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (s : Bool) (tx : SRTag B stepS srcS tgtS) (v : Fin 2 × Fin (srDim B stepS srcS tgtS) → A) : (srLitSrcTop B stepS srcS tgtS s tx).Realize v ↔ srLitSrcTopSem s tx (fun (j : Fin (srDim B stepS srcS tgtS)) => v (selA B stepS srcS tgtS j)) fun (j : Fin (srDim B stepS srcS tgtS)) => v (selB B stepS srcS tgtS j)

theorem DescriptiveComplexity.SuccinctReachHard.realize_srLitTgtTop {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (s : Bool) (tx : SRTag B stepS srcS tgtS) (v : Fin 2 × Fin (srDim B stepS srcS tgtS) → A) : (srLitTgtTop B stepS srcS tgtS s tx).Realize v ↔ srLitTgtTopSem s tx (fun (j : Fin (srDim B stepS srcS tgtS)) => v (selA B stepS srcS tgtS j)) fun (j : Fin (srDim B stepS srcS tgtS)) => v (selB B stepS srcS tgtS j)

theorem DescriptiveComplexity.SuccinctReachHard.sr_stepCl_iff {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (t : SRTag B stepS srcS tgtS) (u : Fin (srDim B stepS srcS tgtS) → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsStepCl ![(t, u)] ↔ srClSem t u

theorem DescriptiveComplexity.SuccinctReachHard.sr_srcCl_iff {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (t : SRTag B stepS srcS tgtS) (u : Fin (srDim B stepS srcS tgtS) → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsSrcCl ![(t, u)] ↔ srSrcClSem t u

theorem DescriptiveComplexity.SuccinctReachHard.sr_tgtCl_iff {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (t : SRTag B stepS srcS tgtS) (u : Fin (srDim B stepS srcS tgtS) → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsTgtCl ![(t, u)] ↔ srTgtClSem t u

theorem DescriptiveComplexity.SuccinctReachHard.sr_lit_iff {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (s : Bool) (tc tx : SRTag B stepS srcS tgtS) (u x : Fin (srDim B stepS srcS tgtS) → A) : FirstOrder.Language.Structure.RelMap (if s = true then FirstOrder.Language.tsPosIn else FirstOrder.Language.tsNegIn) ![(tc, u), (tx, x)] ↔ srLitSem s tc tx u x

From clause satisfaction to satisfaction of a kernel

One lemma, instantiated once per clause group: a valuation of the interpreted instance satisfies every clause of a group exactly when the Tseitin valuation it induces satisfies every clause of that group's encoding and makes the group's root gate true. The group enters only through the three characterizations passed as hypotheses.

theorem DescriptiveComplexity.SuccinctReachHard.sr_pos_iff {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (tc tx : SRTag B stepS srcS tgtS) (u x : Fin (srDim B stepS srcS tgtS) → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsPosIn ![(tc, u), (tx, x)] ↔ srLitSem true tc tx u x

theorem DescriptiveComplexity.SuccinctReachHard.sr_neg_iff {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (tc tx : SRTag B stepS srcS tgtS) (u x : Fin (srDim B stepS srcS tgtS) → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsNegIn ![(tc, u), (tx, x)] ↔ srLitSem false tc tx u x

theorem DescriptiveComplexity.SuccinctReachHard.clausesHold_group_iff {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (f : ((L.sum FirstOrder.Language.order).sum B.double.lang).Sentence) (hctx : Tseitin.maxCtx f ≤ srDim B stepS srcS tgtS) (grp : FirstOrder.Language.transSys.Relations 1) (cl : (m : ℕ) × Tseitin.NodeAt f m → Fin 3 → SRTag B stepS srcS tgtS) (top : SRTag B stepS srcS tgtS) (vr : B.double.ι ⊕ (m : ℕ) × Tseitin.NodeAt f m → SRTag B stepS srcS tgtS) (h₀ : IsBot a₀) (hclause : ∀ (t : SRTag B stepS srcS tgtS) (u : Fin (srDim B stepS srcS tgtS) → A), FirstOrder.Language.Structure.RelMap grp ![(t, u)] ↔ (∃ (σp : (m : ℕ) × Tseitin.NodeAt f m) (k : Fin 3), t = cl σp k ∧ Tseitin.IsClauseSem f hctx σp.snd k u) ∨ t = top ∧ Canon 0 u) (hlitNode : ∀ (s : Bool) (σp : (m : ℕ) × Tseitin.NodeAt f m) (k : Fin 3) (tx : SRTag B stepS srcS tgtS) (u x : Fin (srDim B stepS srcS tgtS) → A), srLitSem s (cl σp k) tx u x ↔ ∃ (vt : B.double.ι ⊕ (m : ℕ) × Tseitin.NodeAt f m), tx = vr vt ∧ Tseitin.LitSem s f hctx σp.snd k u vt x) (hlitTop : ∀ (s : Bool) (tx : SRTag B stepS srcS tgtS) (u x : Fin (srDim B stepS srcS tgtS) → A), srLitSem s top tx u x ↔ s = true ∧ tx = vr (Sum.inr ⟨0, Tseitin.rootAt f⟩) ∧ Canon 0 u ∧ Canon 0 x) (ν : (srInterp B stepS srcS tgtS).Map A → Prop) : ClausesHold ((srInterp B stepS srcS tgtS).Map A) ν grp ↔ (Tseitin.SatCond f hctx fun (w : B.double.ι ⊕ (m : ℕ) × Tseitin.NodeAt f m) (u : Fin (srDim B stepS srcS tgtS) → A) => ν (vr w, u)) ∧ ν (vr (Sum.inr ⟨0, Tseitin.rootAt f⟩), pad a₀ finZeroElim)

Clause satisfaction, group by group: the clauses of a group hold of a valuation exactly when the Tseitin clauses of that group's kernel hold of the induced valuation and the kernel's root gate is true at the padded empty tuple.

theorem DescriptiveComplexity.SuccinctReachHard.sr_step_cases {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (t : SRTag B stepS srcS tgtS) (u : Fin (srDim B stepS srcS tgtS) → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsStepCl ![(t, u)] ↔ (∃ (σp : StepNode B stepS) (k : Fin 3), t = tagStepCl σp k ∧ Tseitin.IsClauseSem (stepK B stepS) ⋯ σp.snd k u) ∨ t = tagStepTop ∧ Canon 0 u

theorem DescriptiveComplexity.SuccinctReachHard.sr_step_litNode {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (s : Bool) (σp : (m : ℕ) × Tseitin.NodeAt (stepK B stepS) m) (k : Fin 3) (tx : SRTag B stepS srcS tgtS) (u x : Fin (srDim B stepS srcS tgtS) → A) : srLitSem s (tagStepCl σp k) tx u x ↔ ∃ (vt : B.double.ι ⊕ StepNode B stepS), tx = stepVar vt ∧ Tseitin.LitSem s (stepK B stepS) ⋯ σp.snd k u vt x

theorem DescriptiveComplexity.SuccinctReachHard.sr_step_litTop {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (s : Bool) (tx : SRTag B stepS srcS tgtS) (u x : Fin (srDim B stepS srcS tgtS) → A) : srLitSem s tagStepTop tx u x ↔ s = true ∧ tx = stepVar (Sum.inr ⟨0, Tseitin.rootAt (stepK B stepS)⟩) ∧ Canon 0 u ∧ Canon 0 x

theorem DescriptiveComplexity.SuccinctReachHard.sr_src_cases {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (t : SRTag B stepS srcS tgtS) (u : Fin (srDim B stepS srcS tgtS) → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsSrcCl ![(t, u)] ↔ (∃ (σp : SrcNode B srcS) (k : Fin 3), t = tagSrcCl σp k ∧ Tseitin.IsClauseSem (srcK B srcS) ⋯ σp.snd k u) ∨ t = tagSrcTop ∧ Canon 0 u

theorem DescriptiveComplexity.SuccinctReachHard.sr_src_litNode {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (s : Bool) (σp : (m : ℕ) × Tseitin.NodeAt (srcK B srcS) m) (k : Fin 3) (tx : SRTag B stepS srcS tgtS) (u x : Fin (srDim B stepS srcS tgtS) → A) : srLitSem s (tagSrcCl σp k) tx u x ↔ ∃ (vt : B.double.ι ⊕ SrcNode B srcS), tx = srcVar vt ∧ Tseitin.LitSem s (srcK B srcS) ⋯ σp.snd k u vt x

theorem DescriptiveComplexity.SuccinctReachHard.sr_src_litTop {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (s : Bool) (tx : SRTag B stepS srcS tgtS) (u x : Fin (srDim B stepS srcS tgtS) → A) : srLitSem s tagSrcTop tx u x ↔ s = true ∧ tx = srcVar (Sum.inr ⟨0, Tseitin.rootAt (srcK B srcS)⟩) ∧ Canon 0 u ∧ Canon 0 x

theorem DescriptiveComplexity.SuccinctReachHard.sr_tgt_cases {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (t : SRTag B stepS srcS tgtS) (u : Fin (srDim B stepS srcS tgtS) → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsTgtCl ![(t, u)] ↔ (∃ (σp : TgtNode B tgtS) (k : Fin 3), t = tagTgtCl σp k ∧ Tseitin.IsClauseSem (tgtK B tgtS) ⋯ σp.snd k u) ∨ t = tagTgtTop ∧ Canon 0 u

theorem DescriptiveComplexity.SuccinctReachHard.sr_tgt_litNode {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (s : Bool) (σp : (m : ℕ) × Tseitin.NodeAt (tgtK B tgtS) m) (k : Fin 3) (tx : SRTag B stepS srcS tgtS) (u x : Fin (srDim B stepS srcS tgtS) → A) : srLitSem s (tagTgtCl σp k) tx u x ↔ ∃ (vt : B.double.ι ⊕ TgtNode B tgtS), tx = tgtVar vt ∧ Tseitin.LitSem s (tgtK B tgtS) ⋯ σp.snd k u vt x

theorem DescriptiveComplexity.SuccinctReachHard.sr_tgt_litTop {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (s : Bool) (tx : SRTag B stepS srcS tgtS) (u x : Fin (srDim B stepS srcS tgtS) → A) : srLitSem s tagTgtTop tx u x ↔ s = true ∧ tx = tgtVar (Sum.inr ⟨0, Tseitin.rootAt (tgtK B tgtS)⟩) ∧ Canon 0 u ∧ Canon 0 x

The two walks correspond

A state of the interpreted transition system is a set of atoms of the first copy of the doubled block, i.e. an assignment of B; a valuation witnessing a transition or an endpoint condition is the canonical Tseitin valuation of the corresponding kernel. The two directions use the two translations between states and assignments, so no round trip is ever needed.

noncomputable def DescriptiveComplexity.SuccinctReachHard.canonTv {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (μ : B.double.Assignment A) (f : ((L.sum FirstOrder.Language.order).sum B.double.lang).Sentence) (hctx : Tseitin.maxCtx f ≤ srDim B stepS srcS tgtS) : B.double.ι ⊕ (m : ℕ) × Tseitin.NodeAt f m → (Fin (srDim B stepS srcS tgtS) → A) → Prop

The Tseitin valuation of a kernel induced by an assignment of the doubled block: block atoms take their values, gates their canonical ones.

Equations

• DescriptiveComplexity.SuccinctReachHard.canonTv μ f hctx (Sum.inl i) u = μ i (DescriptiveComplexity.pref ⋯ u)
• DescriptiveComplexity.SuccinctReachHard.canonTv μ f hctx (Sum.inr σp) u = DescriptiveComplexity.Tseitin.canonVal μ f σp.fst σp.snd (DescriptiveComplexity.pref ⋯ u)

theorem DescriptiveComplexity.SuccinctReachHard.padAssign_canonTv {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (μ : B.double.Assignment A) (f : ((L.sum FirstOrder.Language.order).sum B.double.lang).Sentence) (hctx : Tseitin.maxCtx f ≤ srDim B stepS srcS tgtS) : Tseitin.padAssign a₀ (canonTv μ f hctx) = μ

theorem DescriptiveComplexity.SuccinctReachHard.padVal_canonTv {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (μ : B.double.Assignment A) (f : ((L.sum FirstOrder.Language.order).sum B.double.lang).Sentence) (hctx : Tseitin.maxCtx f ≤ srDim B stepS srcS tgtS) : Tseitin.padVal a₀ (canonTv μ f hctx) = Tseitin.canonVal μ f

theorem DescriptiveComplexity.SuccinctReachHard.satCond_canonTv {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (h₀ : IsBot a₀) (μ : B.double.Assignment A) (f : ((L.sum FirstOrder.Language.order).sum B.double.lang).Sentence) (hctx : Tseitin.maxCtx f ≤ srDim B stepS srcS tgtS) : Tseitin.SatCond f hctx (canonTv μ f hctx)

theorem DescriptiveComplexity.SuccinctReachHard.root_canonTv {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (μ : B.double.Assignment A) (f : ((L.sum FirstOrder.Language.order).sum B.double.lang).Sentence) (hctx : Tseitin.maxCtx f ≤ srDim B stepS srcS tgtS) : canonTv μ f hctx (Sum.inr ⟨0, Tseitin.rootAt f⟩) (pad a₀ finZeroElim) ↔ Tseitin.RealizeWith μ f finZeroElim

theorem DescriptiveComplexity.SuccinctReachHard.realizeWith_of_satCond {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (h₀ : IsBot a₀) (f : ((L.sum FirstOrder.Language.order).sum B.double.lang).Sentence) (hctx : Tseitin.maxCtx f ≤ srDim B stepS srcS tgtS) (tv : B.double.ι ⊕ (m : ℕ) × Tseitin.NodeAt f m → (Fin (srDim B stepS srcS tgtS) → A) → Prop) (hsat : Tseitin.SatCond f hctx tv) (hroot : tv (Sum.inr ⟨0, Tseitin.rootAt f⟩) (pad a₀ finZeroElim)) : Tseitin.RealizeWith (Tseitin.padAssign a₀ tv) f finZeroElim

The Tseitin valuation induced by a kernel's satisfaction of its clauses realizes the kernel.

theorem DescriptiveComplexity.SuccinctReachHard.realizeWith_iff {L : FirstOrder.Language} {B : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] (μ : B.double.Assignment A) (f : ((L.sum FirstOrder.Language.order).sum B.double.lang).Sentence) : Tseitin.RealizeWith μ f finZeroElim ↔ A ⊨ f

Realization of a kernel is realization of the sentence it renames.

States

def DescriptiveComplexity.SuccinctReachHard.srStateOf {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} (ρ : B.Assignment A) : (srInterp B stepS srcS tgtS).Map A → Prop

The state of the interpreted system carried by an assignment of B: the atoms of the first copy that it satisfies.

Equations

• DescriptiveComplexity.SuccinctReachHard.srStateOf ρ e = match e.1 with | Sum.inr (Sum.inl (Sum.inl i)) => ρ i (DescriptiveComplexity.pref ⋯ e.2) | x => False

def DescriptiveComplexity.SuccinctReachHard.srAssignOf {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} (a₀ : A) (S : (srInterp B stepS srcS tgtS).Map A → Prop) : B.Assignment A

The assignment of B read off a state of the interpreted system: its canonically padded atoms of the first copy.

Equations

• DescriptiveComplexity.SuccinctReachHard.srAssignOf a₀ S i w = S (DescriptiveComplexity.SuccinctReachHard.tagAtom (Sum.inl i), DescriptiveComplexity.pad a₀ w)

noncomputable def DescriptiveComplexity.SuccinctReachHard.srCanon {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (μ : B.double.Assignment A) : (srInterp B stepS srcS tgtS).Map A → Prop

The canonical valuation of the interpreted instance under an assignment of the doubled block.

Equations

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

theorem DescriptiveComplexity.SuccinctReachHard.srCanon_step {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (μ : B.double.Assignment A) : (fun (w : B.double.ι ⊕ StepNode B stepS) (u : Fin (srDim B stepS srcS tgtS) → A) => srCanon μ (stepVar w, u)) = canonTv μ (stepK B stepS) ⋯

theorem DescriptiveComplexity.SuccinctReachHard.srCanon_src {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (μ : B.double.Assignment A) : (fun (w : B.double.ι ⊕ SrcNode B srcS) (u : Fin (srDim B stepS srcS tgtS) → A) => srCanon μ (srcVar w, u)) = canonTv μ (srcK B srcS) ⋯

theorem DescriptiveComplexity.SuccinctReachHard.srCanon_tgt {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (μ : B.double.Assignment A) : (fun (w : B.double.ι ⊕ TgtNode B tgtS) (u : Fin (srDim B stepS srcS tgtS) → A) => srCanon μ (tgtVar w, u)) = canonTv μ (tgtK B tgtS) ⋯

theorem DescriptiveComplexity.SuccinctReachHard.readsCur_srCanon {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (μ : B.double.Assignment A) : ReadsCur ((srInterp B stepS srcS tgtS).Map A) (srCanon μ) (srStateOf (B.fstAssign μ))

The canonical valuation reads the state its assignment's first copy carries.

theorem DescriptiveComplexity.SuccinctReachHard.writesNext_srCanon {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (μ : B.double.Assignment A) : WritesNext ((srInterp B stepS srcS tgtS).Map A) (srCanon μ) (srStateOf (B.sndAssign μ))

The canonical valuation writes the state its assignment's second copy carries.

From the specification's walk to the interpreted one

theorem DescriptiveComplexity.SuccinctReachHard.stepRel_srStateOf {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (h₀ : IsBot a₀) (ρ σ : B.Assignment A) (h : A ⊨ stepS) : StepRel ((srInterp B stepS srcS tgtS).Map A) (srStateOf ρ) (srStateOf σ)

A transition of the specification is a transition of the interpreted system.

theorem DescriptiveComplexity.SuccinctReachHard.isStart_srStateOf {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (h₀ : IsBot a₀) (ρ : B.Assignment A) (h : A ⊨ srcS) : IsStart ((srInterp B stepS srcS tgtS).Map A) (srStateOf ρ)

A source state of the specification is a source state of the interpreted system.

theorem DescriptiveComplexity.SuccinctReachHard.isGoal_srStateOf {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (h₀ : IsBot a₀) (ρ : B.Assignment A) (h : A ⊨ tgtS) : IsGoal ((srInterp B stepS srcS tgtS).Map A) (srStateOf ρ)

A target state of the specification is a target state of the interpreted system.

From the interpreted walk back to the specification's

theorem DescriptiveComplexity.SuccinctReachHard.realize_step_of_stepRel {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (h₀ : IsBot a₀) (S S' : (srInterp B stepS srcS tgtS).Map A → Prop) (h : StepRel ((srInterp B stepS srcS tgtS).Map A) S S') : A ⊨ stepS

A transition of the interpreted system is a transition of the specification, between the assignments its two states carry.

theorem DescriptiveComplexity.SuccinctReachHard.realize_src_of_isStart {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (h₀ : IsBot a₀) (S : (srInterp B stepS srcS tgtS).Map A → Prop) (h : IsStart ((srInterp B stepS srcS tgtS).Map A) S) : A ⊨ srcS

A source state of the interpreted system carries an assignment satisfying the source sentence.

theorem DescriptiveComplexity.SuccinctReachHard.realize_tgt_of_isGoal {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (h₀ : IsBot a₀) (S : (srInterp B stepS srcS tgtS).Map A → Prop) (h : IsGoal ((srInterp B stepS srcS tgtS).Map A) S) : A ⊨ tgtS

A target state of the interpreted system carries an assignment satisfying the target sentence.

Correctness of the interpretation

theorem DescriptiveComplexity.SuccinctReachHard.srInterp_correct {L : FirstOrder.Language} {B : SOBlock} {stepS : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence} {srcS tgtS : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (h₀ : IsBot a₀) : SuccinctReachable ((srInterp B stepS srcS tgtS).Map A) ↔ ∃ (ρ : B.Assignment A) (σ : B.Assignment A), A ⊨ srcS ∧ A ⊨ tgtS ∧ Relation.ReflTransGen DescriptiveComplexity.SuccinctReachHard.specStep✝ ρ σ

Correctness of the interpretation: the interpreted transition system reaches a target state from a source state exactly when the specification accepts the input structure.

The discharge

noncomputable def DescriptiveComplexity.sotcReduction {L : FirstOrder.Language} (Q : DecisionProblem L) (spec : SOTCSpec L) (hspec : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], Q.Holds A ↔ spec.Accepts A) : OrderedFOReduction Q SUCCINCTREACH

The generic reduction to SUCCINCT-REACH: an ordered first-order reduction from any problem defined, on nonempty finite ordered structures, by an SO(TC) specification.

Equations

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

theorem DescriptiveComplexity.succinctReach_hard_of_sotcDefinable {L : FirstOrder.Language} (Q : DecisionProblem L) : SOTCDefinable Q → Nonempty (OrderedFOReduction Q SUCCINCTREACH)

Hardness: every SO(TC) definable problem admits an ordered first-order reduction to SUCCINCT-REACH.

theorem DescriptiveComplexity.SUCCINCTREACH_PSPACE_complete : PSPACE.Complete SUCCINCTREACH

SUCCINCT-REACH is PSPACE-complete. Membership is DescriptiveComplexity.succinctReach_mem_PSPACE, the SO(TC) specification whose states are the states of the transition system; hardness is DescriptiveComplexity.succinctReach_hard_of_sotcDefinable, the three-group Tseitin discharge.