LanglibGlobal embeddings of productive-node owners #
The local productive nodes of a pending parse occupy one contiguous window in the root carrier
Fin (10 * input.length). A binary root owns the first slot; its left and right children
occupy the two following consecutive subwindows. These embeddings agree definitionally, up to
the arithmetic offsets, with NFParse.eventOwnerNat.
theorem
IndexedGrammar.NFParse.productiveCount_binary
{T : Type}
{g : IndexedGrammar T}
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
(hr : r ∈ g.rules)
(hlhs : r.lhs = A)
(hc : r.consume = none)
(hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none])
(left : g.NFParse B stack u)
(right : g.NFParse C stack v)
:
(binary hr hlhs hc hrhs left right).productiveCount = left.productiveCount + right.productiveCount + 1
Productive nodes split into the binary root, the left subtree, and the right subtree.
def
IndexedGrammar.NFParse.embedBinaryLeftProductive
{T : Type}
{g : IndexedGrammar T}
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
(left : g.NFParse B stack u)
(right : g.NFParse C stack v)
(owner : Fin left.productiveCount)
:
Fin (binary hr hlhs hc hrhs left right).productiveCount
Embed a left-child productive-node ID into the parent's preorder numbering.
Equations
- left.embedBinaryLeftProductive right owner = ⟨↑owner + 1, ⋯⟩
Instances For
def
IndexedGrammar.NFParse.embedBinaryRightProductive
{T : Type}
{g : IndexedGrammar T}
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
(left : g.NFParse B stack u)
(right : g.NFParse C stack v)
(owner : Fin right.productiveCount)
:
Fin (binary hr hlhs hc hrhs left right).productiveCount
Embed a right-child productive-node ID after the root and left-subtree ranges.
Equations
- left.embedBinaryRightProductive right owner = ⟨left.productiveCount + ↑owner + 1, ⋯⟩
Instances For
theorem
IndexedGrammar.NFParse.embedBinaryLeftProductive_injective
{T : Type}
{g : IndexedGrammar T}
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
(left : g.NFParse B stack u)
(right : g.NFParse C stack v)
:
Function.Injective (left.embedBinaryLeftProductive right)
theorem
IndexedGrammar.NFParse.embedBinaryRightProductive_injective
{T : Type}
{g : IndexedGrammar T}
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
(left : g.NFParse B stack u)
(right : g.NFParse C stack v)
:
Function.Injective (left.embedBinaryRightProductive right)
theorem
IndexedGrammar.Aho.consumeRoute_popContinuation_noBinary_with_owners
{T : Type}
{g : IndexedGrammar T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{p : g.NFParse A stack w}
{k : ℕ}
(route : NFParse.ConsumeRoute g p k)
(hroute : route.NoBinary)
:
∃ (Y : g.nt) (suffix : List g.flag) (rest : g.NFParse Y suffix w),
suffix = List.drop (k + 1) stack ∧ PopPath g A (List.take (k + 1) stack) Y ∧ rest.nodeCount < p.nodeCount ∧ (∀ (j : ℕ), rest.ConsumesAt j ↔ p.ConsumesAt (k + 1 + j)) ∧ (∀ (d : ℕ), d ∈ rest.eventDepths ↔ k + 1 + d ∈ p.eventDepths) ∧ ∀ (d : ℕ), rest.eventOwnerNat d = p.eventOwnerNat (k + 1 + d)
A binary-free consumed route preserves the canonical productive-node owner numbering when
its popped prefix is removed. This is the owner-aware form of
consumeRoute_popContinuation_noBinary_with_consumption; it lives here because
NFParse.eventOwnerNat is defined after that earlier continuation theorem.
structure
IndexedGrammar.Aho.ProductiveOwnerWindow
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
(parse : g.NFParse A stack w)
:
A contiguous slice of the root productive-node carrier assigned to one pending parse.
- base : ℕ
Productive nodes use only the initial
2|input|-1slots.
Instances For
Start of the generic ghost-owner pool. The preceding interval contains the primary and shadow semantic windows together with the two dedicated temporary labels; every pooled label is therefore outside both semantic windows and distinct from both temporary labels.
Equations
- IndexedGrammar.Aho.genericOwnerOffset input = 4 * input.length
Instances For
def
IndexedGrammar.Aho.genericOwner
{T : Type}
{g : IndexedGrammar T}
{input : List T}
(slot : Fin (6 * input.length))
:
Embed one of the 6|input| reusable pool slots into the generic owner bank.
Equations
- IndexedGrammar.Aho.genericOwner slot = ⟨IndexedGrammar.Aho.genericOwnerOffset input + ↑slot, ⋯⟩
Instances For
@[simp]
theorem
IndexedGrammar.Aho.genericOwner_val
{T : Type}
{g : IndexedGrammar T}
{input : List T}
(slot : Fin (6 * input.length))
:
theorem
IndexedGrammar.Aho.genericOwner_injective
{T : Type}
{g : IndexedGrammar T}
{input : List T}
:
The complete reusable owner universe. Its cardinality, not the ambient carrier size, is what bounds the number of persistent indices on the erased work tape.
Equations
- IndexedGrammar.Aho.genericOwnerRange g input = List.ofFn fun (slot : Fin (6 * input.length)) => IndexedGrammar.Aho.genericOwner slot
Instances For
@[simp]
theorem
IndexedGrammar.Aho.genericOwnerRange_length
{T : Type}
(g : IndexedGrammar T)
(input : List T)
:
theorem
IndexedGrammar.Aho.genericOwnerRange_nodup
{T : Type}
(g : IndexedGrammar T)
(input : List T)
:
(genericOwnerRange g input).Nodup
theorem
IndexedGrammar.Aho.mem_genericOwnerRange_iff
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{owner : Fin (10 * input.length)}
:
theorem
IndexedGrammar.Aho.genericOwnerRange_val_ge
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{owner : Fin (10 * input.length)}
(howner : owner ∈ genericOwnerRange g input)
:
def
IndexedGrammar.Aho.ProductiveOwnerWindow.scratchOwner
{T : Type}
{g : IndexedGrammar T}
{input : List T}
(hinput : 0 < input.length)
:
The first of the two labels between the semantic banks and the generic owner pool.
Instances For
@[simp]
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.scratchOwner_val
{T : Type}
{g : IndexedGrammar T}
{input : List T}
(hinput : 0 < input.length)
:
def
IndexedGrammar.Aho.ProductiveOwnerWindow.transientOwner
{T : Type}
{g : IndexedGrammar T}
{input : List T}
(hinput : 0 < input.length)
:
The second of the two labels between the semantic banks and the generic owner pool.
Instances For
@[simp]
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.transientOwner_val
{T : Type}
{g : IndexedGrammar T}
{input : List T}
(hinput : 0 < input.length)
:
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.scratchOwner_ne_transientOwner
{T : Type}
{g : IndexedGrammar T}
{input : List T}
(hinput : 0 < input.length)
:
def
IndexedGrammar.Aho.ProductiveOwnerWindow.owner
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
(node : Fin parse.productiveCount)
:
Embed a local productive-node ID into its root-capacity owner window.
Instances For
@[simp]
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.owner_val
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
(node : Fin parse.productiveCount)
:
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.owner_injective
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
:
Function.Injective window.owner
A productive window embeds local IDs injectively into the root carrier.
def
IndexedGrammar.Aho.ProductiveOwnerWindow.eventOwner
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
(d : ℕ)
(hd : d ∈ parse.eventDepths)
:
Globally embed the canonical owner selected for an event depth.
Equations
- window.eventOwner d hd = window.owner (parse.eventOwner d hd)
Instances For
@[simp]
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.eventOwner_val
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
(d : ℕ)
(hd : d ∈ parse.eventDepths)
:
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.eventOwner_injective
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
{d e : ℕ}
(hd : d ∈ parse.eventDepths)
(he : e ∈ parse.eventDepths)
:
window.eventOwner d hd = window.eventOwner e he → d = e
Distinct event depths in one task receive distinct global owners.
def
IndexedGrammar.Aho.ProductiveOwnerWindow.root
{T : Type}
{g : IndexedGrammar T}
{input : List T}
(parse : g.NFParse g.initial [] input)
:
ProductiveOwnerWindow parse
The root parse owns the complete root productive-node carrier.
Equations
- IndexedGrammar.Aho.ProductiveOwnerWindow.root parse = { base := 0, end_le := ⋯ }
Instances For
def
IndexedGrammar.Aho.ProductiveOwnerWindow.transport
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{stack stack' : List g.flag}
{w w' : List T}
{parse : g.NFParse A stack w}
{parse' : g.NFParse B stack' w'}
(window : ProductiveOwnerWindow parse)
(hcount : parse'.productiveCount = parse.productiveCount)
:
ProductiveOwnerWindow parse'
Transport a window across a parse change which preserves productive-node count.
Instances For
@[simp]
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.transport_base
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{stack stack' : List g.flag}
{w w' : List T}
{parse : g.NFParse A stack w}
{parse' : g.NFParse B stack' w'}
(window : ProductiveOwnerWindow parse)
(hcount : parse'.productiveCount = parse.productiveCount)
:
def
IndexedGrammar.Aho.ProductiveOwnerWindow.popChild
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{f : g.flag}
{stack : List g.flag}
{w : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = some f}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none]}
{rest : g.NFParse B stack w}
(window : ProductiveOwnerWindow (NFParse.pop hr hlhs hc hrhs rest))
:
Unary pop constructors preserve the productive-node window.
Instances For
def
IndexedGrammar.Aho.ProductiveOwnerWindow.pushChild
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{f : g.flag}
{stack : List g.flag}
{w : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]}
{rest : g.NFParse B (f :: stack) w}
(window : ProductiveOwnerWindow (NFParse.push hr hlhs hc hrhs rest))
:
Unary push constructors preserve the productive-node window.
Instances For
@[simp]
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.popChild_base
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{f : g.flag}
{stack : List g.flag}
{w : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = some f}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none]}
{rest : g.NFParse B stack w}
(window : ProductiveOwnerWindow (NFParse.pop hr hlhs hc hrhs rest))
:
@[simp]
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.pushChild_base
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{f : g.flag}
{stack : List g.flag}
{w : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]}
{rest : g.NFParse B (f :: stack) w}
(window : ProductiveOwnerWindow (NFParse.push hr hlhs hc hrhs rest))
:
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.eventOwner_pop_succ
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{f : g.flag}
{stack : List g.flag}
{w : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = some f}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none]}
{rest : g.NFParse B stack w}
(window : ProductiveOwnerWindow (NFParse.pop hr hlhs hc hrhs rest))
{d : ℕ}
(hd : d ∈ rest.eventDepths)
:
Event owners commute with the one-position depth shift of a pop.
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.eventOwner_push
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{f : g.flag}
{stack : List g.flag}
{w : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]}
{rest : g.NFParse B (f :: stack) w}
(window : ProductiveOwnerWindow (NFParse.push hr hlhs hc hrhs rest))
{d : ℕ}
(hd : d ∈ (NFParse.push hr hlhs hc hrhs rest).eventDepths)
:
window.eventOwner d hd = window.pushChild.eventOwner (NFParse.pushEventPreimage rest.eventDepths d) ⋯
Event owners commute with the canonical preimage selected through a push.
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.eventOwner_push_pos
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{f : g.flag}
{stack : List g.flag}
{w : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]}
{rest : g.NFParse B (f :: stack) w}
(window : ProductiveOwnerWindow (NFParse.push hr hlhs hc hrhs rest))
{d : ℕ}
(hdpos : 0 < d)
(hd : d + 1 ∈ rest.eventDepths)
:
Away from depth zero, a push has the unique event-depth preimage d + 1.
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.exists_child_eventDepth_of_push_parent_pos
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{f : g.flag}
{stack : List g.flag}
{w : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]}
{rest : g.NFParse B (f :: stack) w}
(_window : ProductiveOwnerWindow (NFParse.push hr hlhs hc hrhs rest))
{d : ℕ}
(hdpos : 0 < d)
(hd : d ∈ (NFParse.push hr hlhs hc hrhs rest).eventDepths)
:
Every positive parent event has the unique child preimage one position deeper.
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.eventOwner_one_ne_parent_positive
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{f : g.flag}
{stack : List g.flag}
{w : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]}
{rest : g.NFParse B (f :: stack) w}
(window : ProductiveOwnerWindow (NFParse.push hr hlhs hc hrhs rest))
(hone : 1 ∈ rest.eventDepths)
{d : ℕ}
(hdpos : 0 < d)
(hd : d ∈ (NFParse.push hr hlhs hc hrhs rest).eventDepths)
:
A child event newly exposed at depth one cannot collide with any positive parent event.
def
IndexedGrammar.Aho.ProductiveOwnerWindow.predecessor
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
(hbase : 0 < window.base)
:
The immediately preceding global slot is a canonical scratch owner for any non-root productive window.
Instances For
@[simp]
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.predecessor_val
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
(hbase : 0 < window.base)
:
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.predecessor_lt_base
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
(hbase : 0 < window.base)
:
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.predecessor_ne_owner
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
(hbase : 0 < window.base)
(node : Fin parse.productiveCount)
:
The distinguished scratch slot is outside, and hence distinct from, every local owner.
def
IndexedGrammar.Aho.ProductiveOwnerWindow.binaryLeft
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
{left : g.NFParse B stack u}
{right : g.NFParse C stack v}
(window : ProductiveOwnerWindow (NFParse.binary hr hlhs hc hrhs left right))
:
The left child occupies the subwindow immediately after the binary root.
Instances For
def
IndexedGrammar.Aho.ProductiveOwnerWindow.binaryRight
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
{left : g.NFParse B stack u}
{right : g.NFParse C stack v}
(window : ProductiveOwnerWindow (NFParse.binary hr hlhs hc hrhs left right))
:
ProductiveOwnerWindow right
The right child occupies the subwindow after the root and complete left subtree.
Equations
- window.binaryRight = { base := window.base + left.productiveCount + 1, end_le := ⋯ }
Instances For
@[simp]
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.binaryLeft_base
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
{left : g.NFParse B stack u}
{right : g.NFParse C stack v}
(window : ProductiveOwnerWindow (NFParse.binary hr hlhs hc hrhs left right))
:
@[simp]
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.binaryRight_base
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
{left : g.NFParse B stack u}
{right : g.NFParse C stack v}
(window : ProductiveOwnerWindow (NFParse.binary hr hlhs hc hrhs left right))
:
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.owner_embedBinaryLeft
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
{left : g.NFParse B stack u}
{right : g.NFParse C stack v}
(window : ProductiveOwnerWindow (NFParse.binary hr hlhs hc hrhs left right))
(node : Fin left.productiveCount)
:
Embedding through the left subwindow agrees with embedding its local ID into the parent.
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.owner_embedBinaryRight
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
{left : g.NFParse B stack u}
{right : g.NFParse C stack v}
(window : ProductiveOwnerWindow (NFParse.binary hr hlhs hc hrhs left right))
(node : Fin right.productiveCount)
:
Embedding through the right subwindow agrees with embedding its local ID into the parent.
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.eventOwner_binaryLeft
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
{left : g.NFParse B stack u}
{right : g.NFParse C stack v}
(window : ProductiveOwnerWindow (NFParse.binary hr hlhs hc hrhs left right))
{d : ℕ}
(hd0 : d ≠ 0)
(hd : d ∈ left.eventDepths)
:
A positive event inherited from the left child has the same global owner in both windows.
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.eventOwner_binaryRight
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
{left : g.NFParse B stack u}
{right : g.NFParse C stack v}
(window : ProductiveOwnerWindow (NFParse.binary hr hlhs hc hrhs left right))
{d : ℕ}
(hd0 : d ≠ 0)
(hleft : d ∉ left.eventDepths)
(hd : d ∈ right.eventDepths)
:
A positive event selected from the right child has the same global owner in both windows.
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.eventOwner_binary_zero_val
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B C : g.nt}
{stack : List g.flag}
{u v : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]}
{left : g.NFParse B stack u}
{right : g.NFParse C stack v}
(window : ProductiveOwnerWindow (NFParse.binary hr hlhs hc hrhs left right))
:
The binary root's productive event is exactly the first owner of its window.