LanglibFresh productive owners for unary pushes #
A fresh singleton block introduced by a push is owned by the child's depth-one event. This file isolates the two facts needed to allocate that owner: it can coincide with a parent event only at parent depth zero (and only when the child has no depth-zero event), and it is absent from a fully accounted cursor whenever either that parent depth-zero frame is absent or the child itself has a depth-zero event.
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.pushChild_eventOwner_one_not_outside
{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)
:
¬OutsideProductiveWindow window (window.pushChild.eventOwner 1 hone)
A child's depth-one event is inside the equal-count productive window of its push parent.
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.pushChild_eventOwner_one_eq_parent_iff
{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 : ℕ}
(hd : d ∈ (NFParse.push hr hlhs hc hrhs rest).eventDepths)
:
Exact collision characterization for the depth-one push owner. It aliases a parent event precisely when that event is depth zero and the child has no event at depth zero.
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.pushChild_shadowEventOwner_one_eq_parent_iff
{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 : ℕ}
(hd : d ∈ (NFParse.push hr hlhs hc hrhs rest).eventDepths)
:
window.pushChild.shadowEventOwner 1 hone = window.shadowEventOwner d hd ↔ d = 0 ∧ 0 ∉ rest.eventDepths
The shadow-bank depth-one ticket has the same collision behavior as its primary mate.
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.pushChild_shadowEventOwner_one_not_outside
{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)
:
¬OutsideShadowWindow window (window.pushChild.shadowEventOwner 1 hone)
The child depth-one shadow ticket remains inside the equal-count parent shadow window.
theorem
IndexedGrammar.Aho.EventOwnedFrames.pushChild_eventOwner_one_not_mem_of_no_parent_zero
{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)}
{owners : List (Fin (10 * input.length))}
(frames : EventOwnedFrames (NFParse.push hr hlhs hc hrhs rest) window owners)
(hone : 1 ∈ rest.eventDepths)
(hzeroFresh : ∀ (hd : 0 ∈ (NFParse.push hr hlhs hc hrhs rest).eventDepths), window.eventOwner 0 hd ∉ owners)
:
window.pushChild.eventOwner 1 hone ∉ owners
If no parent depth-zero owner is held by a frame, the child's depth-one owner is fresh from all frames. Outside-window frames cannot collide because unary windows have equal extent.
theorem
IndexedGrammar.Aho.EventOwnedFrames.pushChild_eventOwner_one_not_mem_of_child_zero
{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)}
{owners : List (Fin (10 * input.length))}
(frames : EventOwnedFrames (NFParse.push hr hlhs hc hrhs rest) window owners)
(hzero : 0 ∈ rest.eventDepths)
(hone : 1 ∈ rest.eventDepths)
:
window.pushChild.eventOwner 1 hone ∉ owners
If the child already has a depth-zero event, injectivity separates its depth-one owner from every possible local depth-zero frame.
theorem
IndexedGrammar.Aho.PrefixFrameLedger.pushChild_eventOwner_one_not_mem_indexOwners_of_not_mem_frames
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{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)}
{cursor : ScheduleCursor g input}
{blocks : List (List g.flag)}
{owners outsideOwners : List (Fin (10 * input.length))}
(prefixLedger : PrefixFrameLedger cursor)
(layout : EventOwnedLayout (NFParse.push hr hlhs hc hrhs rest) window blocks owners)
(hfocus : List.filterMap ScheduleAtom.indexOwner? [cursor.focus] = [])
(hright : List.filterMap ScheduleAtom.indexOwner? cursor.right = owners ++ outsideOwners)
(houtside : ∀ owner ∈ outsideOwners, OutsideProductiveWindow window owner)
(hone : 1 ∈ rest.eventDepths)
(hframes : window.pushChild.eventOwner 1 hone ∉ cursor.frameOwners)
:
window.pushChild.eventOwner 1 hone ∉ cursor.indexOwners
Once frame freshness is known, the full cursor decomposition proves that the canonical depth-one push owner is absent from every persistent index.
theorem
IndexedGrammar.Aho.PrefixFrameLedger.pushChild_eventOwner_one_not_mem_indexOwners_of_no_parent_zero_frame
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{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)}
{cursor : ScheduleCursor g input}
{blocks : List (List g.flag)}
{owners outsideOwners : List (Fin (10 * input.length))}
(prefixLedger : PrefixFrameLedger cursor)
(frames : EventOwnedFrames (NFParse.push hr hlhs hc hrhs rest) window cursor.frameOwners)
(layout : EventOwnedLayout (NFParse.push hr hlhs hc hrhs rest) window blocks owners)
(hfocus : List.filterMap ScheduleAtom.indexOwner? [cursor.focus] = [])
(hright : List.filterMap ScheduleAtom.indexOwner? cursor.right = owners ++ outsideOwners)
(houtside : ∀ owner ∈ outsideOwners, OutsideProductiveWindow window owner)
(hone : 1 ∈ rest.eventDepths)
(hzeroFresh : ∀ (hd : 0 ∈ (NFParse.push hr hlhs hc hrhs rest).eventDepths), window.eventOwner 0 hd ∉ cursor.frameOwners)
:
window.pushChild.eventOwner 1 hone ∉ cursor.indexOwners
Full-cursor push freshness when the parent depth-zero owner is not held by a frame.
theorem
IndexedGrammar.Aho.PrefixFrameLedger.pushChild_eventOwner_one_not_mem_indexOwners_of_child_zero
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{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)}
{cursor : ScheduleCursor g input}
{blocks : List (List g.flag)}
{owners outsideOwners : List (Fin (10 * input.length))}
(prefixLedger : PrefixFrameLedger cursor)
(frames : EventOwnedFrames (NFParse.push hr hlhs hc hrhs rest) window cursor.frameOwners)
(layout : EventOwnedLayout (NFParse.push hr hlhs hc hrhs rest) window blocks owners)
(hfocus : List.filterMap ScheduleAtom.indexOwner? [cursor.focus] = [])
(hright : List.filterMap ScheduleAtom.indexOwner? cursor.right = owners ++ outsideOwners)
(houtside : ∀ owner ∈ outsideOwners, OutsideProductiveWindow window owner)
(hzero : 0 ∈ rest.eventDepths)
(hone : 1 ∈ rest.eventDepths)
:
window.pushChild.eventOwner 1 hone ∉ cursor.indexOwners
Full-cursor push freshness when child depths zero and one are both productive events.
theorem
IndexedGrammar.Aho.ScheduleOwnerLedger.pushChild_eventOwner_one_not_mem_indexOwners_of_not_mem_frames
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{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)}
{cursor : ScheduleCursor g input}
(ledger : ScheduleOwnerLedger (NFParse.push hr hlhs hc hrhs rest) window cursor)
{blocks : List (List g.flag)}
(activeLayout : EventOwnedLayout (NFParse.push hr hlhs hc hrhs rest) window blocks ledger.active)
(hfocus : List.filterMap ScheduleAtom.indexOwner? [cursor.focus] = [])
(hone : 1 ∈ rest.eventDepths)
(hframes : window.pushChild.eventOwner 1 hone ∉ cursor.frameOwners)
:
window.pushChild.eventOwner 1 hone ∉ cursor.indexOwners
Schedule-ledger specialization of depth-one push freshness with an explicit frame premise.
theorem
IndexedGrammar.Aho.ScheduleOwnerLedger.pushChild_eventOwner_one_not_mem_indexOwners_of_no_parent_zero_frame
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{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)}
{cursor : ScheduleCursor g input}
(ledger : ScheduleOwnerLedger (NFParse.push hr hlhs hc hrhs rest) window cursor)
{blocks : List (List g.flag)}
(activeLayout : EventOwnedLayout (NFParse.push hr hlhs hc hrhs rest) window blocks ledger.active)
(hfocus : List.filterMap ScheduleAtom.indexOwner? [cursor.focus] = [])
(hone : 1 ∈ rest.eventDepths)
(hzeroFresh : ∀ (hd : 0 ∈ (NFParse.push hr hlhs hc hrhs rest).eventDepths), window.eventOwner 0 hd ∉ cursor.frameOwners)
:
window.pushChild.eventOwner 1 hone ∉ cursor.indexOwners
Schedule-ledger push freshness when no parent depth-zero owner is framed.
theorem
IndexedGrammar.Aho.ScheduleOwnerLedger.pushChild_eventOwner_one_not_mem_indexOwners_of_child_zero
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{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)}
{cursor : ScheduleCursor g input}
(ledger : ScheduleOwnerLedger (NFParse.push hr hlhs hc hrhs rest) window cursor)
{blocks : List (List g.flag)}
(activeLayout : EventOwnedLayout (NFParse.push hr hlhs hc hrhs rest) window blocks ledger.active)
(hfocus : List.filterMap ScheduleAtom.indexOwner? [cursor.focus] = [])
(hzero : 0 ∈ rest.eventDepths)
(hone : 1 ∈ rest.eventDepths)
:
window.pushChild.eventOwner 1 hone ∉ cursor.indexOwners
Schedule-ledger push freshness when child depths zero and one both carry events.
theorem
IndexedGrammar.Aho.ScheduleOwnerLedger.pushChild_eventOwner_one_mem_indexOwners_imp_parent_zero_frame
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{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)}
{cursor : ScheduleCursor g input}
(ledger : ScheduleOwnerLedger (NFParse.push hr hlhs hc hrhs rest) window cursor)
{blocks : List (List g.flag)}
(activeLayout : EventOwnedLayout (NFParse.push hr hlhs hc hrhs rest) window blocks ledger.active)
(hfocus : List.filterMap ScheduleAtom.indexOwner? [cursor.focus] = [])
(hone : 1 ∈ rest.eventDepths)
(hmem : window.pushChild.eventOwner 1 hone ∈ cursor.indexOwners)
:
0 ∉ rest.eventDepths ∧ ∃ (hd : 0 ∈ (NFParse.push hr hlhs hc hrhs rest).eventDepths), window.eventOwner 0 hd ∈ cursor.frameOwners
If the canonical depth-one child owner is already persistent, the unique collision is an open parent depth-zero frame. In particular, the child cannot itself have a depth-zero event.
theorem
IndexedGrammar.Aho.ShadowOwnerLedger.pushChild_shadowEventOwner_one_not_mem_indexOwners_of_child_zero
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{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)}
{cursor : ScheduleCursor g input}
(ledger : ShadowOwnerLedger (NFParse.push hr hlhs hc hrhs rest) window cursor)
{blocks : List (List g.flag)}
(layout : ShadowStartLayout (NFParse.push hr hlhs hc hrhs rest) window blocks ledger.active)
(hfocus : List.filterMap ScheduleAtom.indexOwner? [cursor.focus] = [])
(hzero : 0 ∈ rest.eventDepths)
(hone : 1 ∈ rest.eventDepths)
:
window.pushChild.shadowEventOwner 1 hone ∉ cursor.indexOwners
If child depths zero and one are both events, the depth-one shadow ticket is absent from an entirely accounted parent semantic cursor. It is neither a parent shadow event nor an outside-window ticket.