Counted intervals of paired split-right anchors

A split-right visible anchor executes the completed single marker as a positive one-symbol net-pop interval. This file retains the exact interval position, its untouched child/outer frame, and a productive future from its return endpoint. For a paired split anchor it also records the exhaustive Allen-style order of the two positive intervals.

def DPDA_to_LR.SplitRightInterval {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (completedWord _suffix : List T) (source : State M) (top : StackSymbol M) (returnState : State M) (gamma : List (StackSymbol M)) (_target : State M) (context : List (StackSymbol M)) (startSteps returnSteps : ℕ) : Prop

A counted, retained, productive interval represented by one split-right anchor. startSteps is measured from the wrapper's global initial configuration on the entire completed visible-prefix word.

Equations

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

theorem DPDA_to_LR.splitRightInterval_of_anchor_data {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {base : List (symbol T (Nonterminal M))} {completedWord beforeWord leftWord suffix : List T} {context : List (StackSymbol M)} {source returnState target : State M} {top : StackSymbol M} {gamma : List (StackSymbol M)} (parent : ConcreteOperationalSpine M base (PDA_to_CFG.N.list source (top :: gamma) target) suffix beforeWord context) (hlength : ↑(top :: gamma).length ≤ PDA_to_CFG.max_push (emptyStackPDA M)) (hrule : (PDA_to_CFG.N.list source (top :: gamma) target, [symbol.nonterminal (PDA_to_CFG.N.single source top returnState), symbol.nonterminal (PDA_to_CFG.N.list returnState gamma target)]) ∈ (characteristicGrammar M).rules) (hleft : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.single source top returnState)] (List.map symbol.terminal leftWord)) (hword : completedWord = beforeWord ++ leftWord) : ∃ (startSteps : ℕ) (returnSteps : ℕ), SplitRightInterval M completedWord suffix source top returnState gamma target context startSteps returnSteps

Construct the counted interval directly from the retained data of a split-right visible anchor.

def DPDA_to_LR.ReturnIntervalOrder (start₁ length₁ start₂ length₂ : ℕ) : Prop

The exhaustive relative order of two positive half-open return intervals [start, start + length]. Equal starts and equal finishes are kept separate because they lead to different synchronization arguments.

Equations

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

theorem DPDA_to_LR.returnIntervalOrder_total {start₁ length₁ start₂ length₂ : ℕ} (hpositive₁ : 0 < length₁) (hpositive₂ : 0 < length₂) : ReturnIntervalOrder start₁ length₁ start₂ length₂

Every pair of positive return intervals has one of the thirteen standard relative orders.

theorem DPDA_to_LR.pairedSplitRight_intervals {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {base : List (symbol T (Nonterminal M))} {completedWord beforeWord₁ leftWord₁ beforeWord₂ leftWord₂ suffix₁ suffix₂ : List T} {context₁ context₂ : List (StackSymbol M)} {source returnState target₁ target₂ : State M} {top : StackSymbol M} {gamma₁ gamma₂ : List (StackSymbol M)} (parent₁ : ConcreteOperationalSpine M base (PDA_to_CFG.N.list source (top :: gamma₁) target₁) suffix₁ beforeWord₁ context₁) (length₁ : ↑(top :: gamma₁).length ≤ PDA_to_CFG.max_push (emptyStackPDA M)) (rule₁ : (PDA_to_CFG.N.list source (top :: gamma₁) target₁, [symbol.nonterminal (PDA_to_CFG.N.single source top returnState), symbol.nonterminal (PDA_to_CFG.N.list returnState gamma₁ target₁)]) ∈ (characteristicGrammar M).rules) (left₁ : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.single source top returnState)] (List.map symbol.terminal leftWord₁)) (parent₂ : ConcreteOperationalSpine M base (PDA_to_CFG.N.list source (top :: gamma₂) target₂) suffix₂ beforeWord₂ context₂) (length₂ : ↑(top :: gamma₂).length ≤ PDA_to_CFG.max_push (emptyStackPDA M)) (rule₂ : (PDA_to_CFG.N.list source (top :: gamma₂) target₂, [symbol.nonterminal (PDA_to_CFG.N.single source top returnState), symbol.nonterminal (PDA_to_CFG.N.list returnState gamma₂ target₂)]) ∈ (characteristicGrammar M).rules) (left₂ : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.single source top returnState)] (List.map symbol.terminal leftWord₂)) (word₁ : completedWord = beforeWord₁ ++ leftWord₁) (word₂ : completedWord = beforeWord₂ ++ leftWord₂) : ∃ (start₁ : ℕ) (return₁ : ℕ) (start₂ : ℕ) (return₂ : ℕ), SplitRightInterval M completedWord suffix₁ source top returnState gamma₁ target₁ context₁ start₁ return₁ ∧ SplitRightInterval M completedWord suffix₂ source top returnState gamma₂ target₂ context₂ start₂ return₂ ∧ ReturnIntervalOrder start₁ return₁ start₂ return₂

The two sides of a paired split-right anchor expose counted retained return intervals and their exhaustive relative order.