OAI/Computability/FiniteCompiler/Paths.lean

GitHub source file

120 declarations, 0 contain sorry, 0 declared as axioms

Path alphabet, sectors, cuts, and contextual preparation.

  1. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Vertex line 13
  2. instance OAI.FiniteAlgebraicEnvelopes.Compiler.Path.(instance at line 17) line 17
  3. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter line 20

    Source documentation

    There are no vertex-identity letters. zero is the absorbing letter.

    inductive Letter (C H : Type*)
  | zero | enter | leave
  | head : H → Letter C H
  | left : C → Letter C H
  | right : C → Letter C H
  deriving DecidableEq, Fintype

/-- Boundary type of a word; `unit` belongs only to the empty word. -/
  4. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Shape line 28

    Source documentation

    Boundary type of a word; unit belongs only to the empty word.

    inductive Shape
  | zero | unit
  | path : Vertex → Vertex → Shape
  deriving DecidableEq

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Vertex

  5. instance OAI.FiniteAlgebraicEnvelopes.Compiler.Path.(instance at line 33) line 33
  6. def OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Shape.comp line 37
  7. instance OAI.FiniteAlgebraicEnvelopes.Compiler.Path.(instance at line 44) line 44
  8. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.unit_mul line 51
  9. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.mul_unit line 52
  10. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.zero_mul line 54
  11. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.mul_zero line 55
  12. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.path_mul_path line 56
  13. def OAI.FiniteAlgebraicEnvelopes.Compiler.Path.typeOf line 61
  14. def OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape line 69
  15. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape_nil line 71
  16. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape_cons line 72
  17. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape_append line 74
  18. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape_singleton line 76
  19. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape_context line 80

    Source documentation

    Parallel nonzero equation sides preserve the complete contextual shape, including nonpath status. This also covers all length-decreasing cleanup.

    theorem shape_context {u v : List (Letter C H)} (h : shape u = shape v)
    (x y : List (Letter C H)) : shape (x++u++y) = shape (x++v++y) := by simp [h]

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape

  20. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape_zero_context line 83
  21. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.typeOf_ne_unit line 86
  22. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.comp_eq_unit_iff line 89
  23. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape_unit_iff line 91
  24. def OAI.FiniteAlgebraicEnvelopes.Compiler.Path.headed line 96

    Source documentation

    A headed sector written literally. Cells left of the head are supplied in nearest-first zipper order.

    def headed (l : List C) (q : H) (r : List C) (lb rb : Bool) : List (Letter C H) :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter

  25. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape_left line 100
  26. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape_right line 110
  27. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape_headed line 120
  28. def OAI.FiniteAlgebraicEnvelopes.Compiler.Path.heads line 129
  29. def OAI.FiniteAlgebraicEnvelopes.Compiler.Path.lefts line 133
  30. def OAI.FiniteAlgebraicEnvelopes.Compiler.Path.rights line 137
  31. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.heads_headed line 141
  32. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.lefts_headed line 145
  33. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.rights_headed line 149
  34. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.headed_injective line 153
  35. def OAI.FiniteAlgebraicEnvelopes.Compiler.Path.glue line 169

    Source documentation

    Prefix a (possibly empty) fragment to the first sector, creating a sector only when the fragment is nonempty.

    def glue (u : List (Letter C H)) (cs : List (List (Letter C H))) : List (List (Letter C H)) :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter

  36. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.glue_nil line 176
  37. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.glue_cons line 179
  38. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.glue_assoc line 182
  39. def OAI.FiniteAlgebraicEnvelopes.Compiler.Path.cuts line 188

    Source documentation

    Cut immediately after an omega, omitting the empty final sector. On paths every interior cut is exactly omega-alpha, including headless end sectors.

    def cuts : List (Letter C H) → List (List (Letter C H))
  | [] => []
  | .leave::w => [.leave] :: cuts w
  | a::w => glue [a] (cuts w)

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.glue

  40. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.cuts_nil line 193
  41. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.cuts_leave line 194
  42. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.cuts_cons line 196
  43. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.flatten_glue line 199
  44. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.flatten_cuts line 203
  45. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.glue_singleton_nonempty line 208
  46. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.cuts_nonempty line 219
  47. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.cuts_append_nonleave line 231
  48. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.cuts_of_noLeave line 241
  49. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.headed_ne_nil line 244
  50. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.cuts_headed line 252
  51. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape_append_ne_zero line 267
  52. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape_mem_flatten_ne_zero line 271
  53. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape_cut_ne_zero line 281
  54. def OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Shape.act line 285
  55. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Shape.act_comp line 290
  56. def OAI.FiniteAlgebraicEnvelopes.Compiler.Path.walk line 293
  57. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.walk_nil line 295
  58. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.walk_cons line 297
  59. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.exists_walk line 301
  60. def OAI.FiniteAlgebraicEnvelopes.Compiler.Path.terminalLeave line 309

    Source documentation

    A sector cannot have any omega except its last letter.

    def terminalLeave : List (Letter C H) → Prop
  | [] => True
  | .leave::w => w = []
  | _::w => terminalLeave w

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter

  61. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.terminalLeave_cons line 314
  62. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.terminalLeave_glue line 317
  63. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.terminalLeave_cuts line 329
  64. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.right_form line 345

    Source documentation

    Once a path is at R, its terminal sector consists only of right loops and an optional omega. This includes a headless right end-sector.

    theorem right_form {w : List (Letter C H)} (hn : terminalLeave w) {v : Vertex}
    (h : walk .right w = some v) :
    ∃ r : List C, ∃ rb : Bool, w = r.map .right ++ (if rb then [.leave] else []) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.terminalLeave, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Vertex, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.walk

  65. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.left_form line 366

    Source documentation

    Starting at L, a sector either has no head and only left loops, or has exactly one head followed by a right-only tail.

    theorem left_form {w : List (Letter C H)} (hn : terminalLeave w) {v : Vertex}
    (h : walk .left w = some v) :
    (∃ l : List C, w = l.map .left) ∨
    (∃ l : List C, ∃ q : H, ∃ r : List C, ∃ rb : Bool,
      w = l.map .left ++ [.head q] ++ r.map .right ++ (if rb then [.leave] else [])) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.terminalLeave, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Vertex, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.walk

  66. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.sector_form line 391

    Source documentation

    Every nonzero sector is either literally headless or has the precise optional-boundary zipper grammar used by the finite component evaluator.

    theorem sector_form {w : List (Letter C H)} (hn : terminalLeave w)
    (h : shape w ≠ .zero) : heads w = [] ∨
    ∃ l q r lb rb, w = headed l q r lb rb := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.terminalLeave, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.heads, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.headed

  67. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.cut_form line 420
  68. structure OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Sector line 425
  69. def OAI.FiniteAlgebraicEnvelopes.Compiler.Path.encode line 433
  70. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.encode_injective line 436
  71. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.enter_mem_headed line 443
  72. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.leave_mem_headed line 447
  73. def OAI.FiniteAlgebraicEnvelopes.Compiler.Path.decode line 455

    Source documentation

    An entirely literal decoder, including a final equality check. It does not assume that its input is a path or that any tag is clean.

    def decode (w : List (Letter C H)) : Option (Sector C H) :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Sector

  74. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.decode_encode line 463
  75. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.decode_sound line 469
  76. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.decode_none_of_headless line 480
  77. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.decode_complete line 483
  78. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.cut_decode_complete line 489
  79. abbrev OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shortlex line 498

    Source documentation

    The shortlex order of literal encodings, fixed independently of a budget. The alphabet order may be the concrete compiler's numerical symbol order.

    abbrev shortlex [LinearOrder (Letter C H)] : LinearOrder (Sector C H) :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Sector

  80. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Context line 511

    Source documentation

    A single literal equation step in arbitrary word context.

    inductive Context (r : List (Letter C H) → List (Letter C H) → Prop) :
    List (Letter C H) → List (Letter C H) → Prop
  | apply (x y : List (Letter C H)) {a b} (h : r a b) :
      Context r (x++a++y) (x++b++y)

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter

  81. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.context_context line 516
  82. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.reaches_context line 523
  83. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Path.ZeroStep line 530

    Source documentation

    These are exactly the absorbing-letter and incompatible-arrow equations, oriented toward the zero letter.

    inductive ZeroStep : List (Letter C H) → List (Letter C H) → Prop
  | pair (a b : Letter C H) (h : typeOf a * typeOf b = .zero) : ZeroStep [a,b] [.zero]

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.typeOf

  84. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Shape.middle_zero line 533
  85. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.absorb_zero line 536
  86. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.zero_reaches line 546

    Source documentation

    Every dirty nonpath, including every occurrence of Omega, has a finite zero derivation. No simulation, program call, or confluence is used.

    theorem zero_reaches {w : List (Letter C H)} (h : shape w = .zero) :
    ReflTransGen (Context ZeroStep) w [.zero] := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Context, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.ZeroStep

  87. def OAI.FiniteAlgebraicEnvelopes.Compiler.Path.letterGrade line 567

    Source documentation

    Additive grade on literal words. The head and boundary letters each have grade one, while all cell-tag data is ignored by a supplied base grade.

    def letterGrade (g : C → ℕ) : Letter C H → ℕ
  | .zero => 0
  | .left c | .right c => g c
  | _ => 1

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter

  88. def OAI.FiniteAlgebraicEnvelopes.Compiler.Path.grade line 572
  89. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.grade_nil line 574
  90. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.grade_cons line 575
  91. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.grade_append line 577
  92. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.context_grade line 580
  93. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.zeroStep_grade line 588
  94. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.zero_context_grade line 591
  95. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.grade_headed line 594
  96. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.glue_append_of_ne_nil line 604
  97. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.cuts_append_leave line 611
  98. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.split_left_context line 627

    Source documentation

    Split an arbitrary left context after its last omega. The finished part cannot join the sector containing a subsequently inserted head.

    theorem split_left_context (x : List (Letter C H)) :
    ∃ p a, x = p++a ∧ (.leave : Letter C H) ∉ a ∧
      (p = [] ∨ ∃ t, p = t++[.leave]) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter

  99. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.context_frame line 643

    Source documentation

    One delimiter frame works simultaneously for every nonempty replacement with no omega. This lemma makes no path or cleanliness assumption.

    theorem context_frame (x y : List (Letter C H)) :
    ∃ cs a b ds, (.leave : Letter C H) ∉ a ∧ terminalLeave b ∧
      (∀ u : List (Letter C H), u ≠ [] → .leave ∉ u →
        cuts (x++u++y) = cs ++ (a++u++b)::ds) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.terminalLeave, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.cuts

  100. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.terminalLeave_append_nonleave line 673
  101. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.head_context_form line 683

    Source documentation

    The unique designated head identifies its entire host sector, even when the surrounding input is malformed. The only premise is literal pathhood.

    theorem head_context_form {a b : List (Letter C H)} {q : H}
    (hn : terminalLeave (a++ .head q::b)) (h : shape (a++ .head q::b) ≠ .zero) :
    ∃ (l r : List C) (lb rb : Bool), a = (if lb then [.enter] else []) ++ l.reverse.map .left ∧
      b = r.map .right ++ (if rb then [.leave] else []) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.terminalLeave, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape

  102. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.head_frame line 706

    Source documentation

    Extract the containing sector in an arbitrary path context. The same surrounding sector list works after any head change, or any added left and right loops. No claim that sector boundaries survive arbitrary attachment of context is built into the statement.

    theorem head_frame (x y : List (Letter C H)) (q : H)
    (h : shape (x++[.head q]++y) ≠ .zero) :
    ∃ cs ds l r lb rb, ∀ (q' : H) (ls rs : List C),
      cuts (x++ls.map .left++[.head q']++rs.map .right++y) =
        cs ++ [headed (ls.reverse++l) q' (rs++r) lb rb] ++ ds := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.cuts, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.headed

  103. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.split_right_context line 726
  104. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.general_context_frame line 743

    Source documentation

    A two-sided delimiter frame, valid even for replacements which change the number of heads or create/delete internal visits to the outer vertex.

    theorem general_context_frame (x y : List (Letter C H)) :
    ∃ cs a b ds, (.leave : Letter C H) ∉ a ∧ terminalLeave b ∧
      (∀ u, cuts (x++u++y) = cs ++ cuts (a++u++b) ++ ds) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.terminalLeave, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.cuts

  105. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.word_frame line 768

    Source documentation

    Around a fixed head every path context is exactly an arbitrary prefix of finished sectors, an optional alpha and left loops, right loops and an optional omega, and an arbitrary suffix of sectors. This uniform literal identity is also valid for merge and unmerge replacements.

    theorem word_frame (x y : List (Letter C H)) (q : H)
    (h : shape (x++[.head q]++y) ≠ .zero) :
    ∃ (cs ds : List (List (Letter C H))) (l r : List C) (lb rb : Bool), ∀ u,
      cuts (x++u++y) = cs ++
        cuts (((if lb then [.enter] else []) ++ l.reverse.map .left) ++ u ++
          (r.map .right ++ (if rb then [.leave] else []))) ++ ds := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.cuts

  106. def OAI.FiniteAlgebraicEnvelopes.Compiler.Path.prepareChunk line 794

    Source documentation

    Preprocessing is applied only to headed sectors. Headless pieces retain their literal words; no implicit boundary or identity generator is added.

    def prepareChunk (P : Sector C H → List (Sector C H)) (w : List (Letter C H)) :
    List (List (Letter C H)) :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter

  107. def OAI.FiniteAlgebraicEnvelopes.Compiler.Path.prepareChunks line 800
  108. def OAI.FiniteAlgebraicEnvelopes.Compiler.Path.prepare line 803
  109. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.prepareChunk_encode line 806
  110. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.prepareChunks_append line 809
  111. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.prepareChunks_singleton line 814
  112. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.prepare_context_headed line 820

    Source documentation

    All ordinary compiler rules can be checked on a sector with arbitrary extra zipper cells. This theorem transports those checks into arbitrary literal word contexts, without a cleanliness or boundary promise.

    theorem prepare_context_headed (P : Sector C H → List (Sector C H))
    (x y : List (Letter C H)) (l₁ l₂ r₁ r₂ : List C) (q₁ q₂ : H)
    (h : shape (x++headed l₁ q₁ r₁ false false++y) ≠ .zero)
    (hinv : ∀ (l r : List C) (lb rb : Bool),
      P ⟨l₁++l,q₁,r₁++r,lb,rb⟩ = P ⟨l₂++l,q₂,r₂++r,lb,rb⟩) :
    prepare P (x++headed l₁ q₁ r₁ false false++y) =
      prepare P (x++headed l₂ q₂ r₂ false false++y) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.headed, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.prepare

  113. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.prefix_end_enter line 848
  114. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.suffix_begin_leave line 863
  115. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.left_boundary_frame line 870
  116. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.right_boundary_frame line 891
  117. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.prepare_context_left_boundary line 922
  118. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.prepare_context_right_boundary line 933
  119. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.cuts_join_headed line 948
  120. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.prepare_context_merge line 960

    Source documentation

    Literal merge invariance in every well-typed context, including incomplete and dirty outer sectors. The two visits to the outer vertex are explicit.

    theorem prepare_context_merge (P : Sector C H → List (Sector C H))
    (x y : List (Letter C H)) (q p : H) (c d : C)
    (h : shape (x++[.head q,.leave,.enter,.head q]++y) ≠ .zero)
    (hinv : ∀ (l r : List C) (lb rb : Bool),
      P ⟨c::l,p,d::r,lb,rb⟩ = P ⟨l,q,[],lb,true⟩ ++ P ⟨[],q,r,true,rb⟩) :
    prepare P (x++[.head q,.leave,.enter,.head q]++y) =
      prepare P (x++[.left c,.head p,.right d]++y) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.prepare