OAI/Computability/FiniteCompiler/Selectors.lean

GitHub source file

129 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.frame line 17
2. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.length_frame line 20
3. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.infix_strip_cons line 24
4. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.infix_strip_prefix line 33
5. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.infix_strip_suffix line 41
6. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.prefix_mem_initial line 48
7. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.infix_strip_outer line 61
8. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.bounded_strip_left line 69

   Source documentation

   A short older selector cannot start in, or straddle, the new left guard.

   theorem bounded_strip_left {d l h : S} {v w : List S} {N : ℕ}
       (hdl : d≠l) (hhd : h≠d) (hhl : h≠l) (hend : h∈d::v)
       (hlen : (d::v).length ≤ N) (hi : d::v <:+: d::(List.replicate N l++w)) :
       d::v <:+: w := by
   …

9. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.bounded_infix_frame line 87

   Source documentation

   Every older selector side of length at most N lies wholly in the body of an N-envelope. Its body is checked irreducible when that envelope is chosen.

   theorem bounded_infix_frame {d l r h : S} {v w : List S} {N : ℕ}
       (hdl : d≠l) (hhr : h≠r) (hhd : h≠d) (hhl : h≠l) (hdr : d≠r)
       (hlen : (d::(v++[h])).length ≤ N)
       (hi : d::(v++[h]) <:+: frame d l r h N w) : d::(v++[h]) <:+: w := by
   …

   Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.frame

10. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.alphabet_infix_frame line 100

    Source documentation

    The purely alphabetic version used for static/selector overlaps.

    theorem alphabet_infix_frame {d l r h a b : S} {v w : List S} {N : ℕ}
        (had : a≠d) (hal : a≠l) (hbr : b≠r) (hbh : b≠h)
        (hi : a::(v++[b]) <:+: frame d l r h N w) : a::(v++[b]) <:+: w := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.frame

11. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.header_unique line 111

    Source documentation

    The long header has exactly one occurrence in its own envelope.

    theorem header_unique {d l r h : S} {N : ℕ} {w x y : List S}
        (hdl : d≠l) (hlr : l≠r) (hlh : l≠h) (hw : w.length < N)
        (he : frame d l r h N w = x++(d::List.replicate N l)++y) : x=[] := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.frame

12. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.prefix_frame line 131

    Source documentation

    Prefix-comparable same-stage envelopes have equal bodies.

    theorem prefix_frame {d l r h : S} {N : ℕ} {u v : List S}
        (hhr : h≠r) (_ : u.length<N) (hv : v.length<N)
        (hp : frame d l r h N u <+: frame d l r h N v) : u=v := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.frame

13. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.infix_frame line 159

    Source documentation

    Same-stage left sides cannot properly contain one another.

    theorem infix_frame {d l r h : S} {N : ℕ} {u v x y : List S}
        (hdl : d≠l) (hlr : l≠r) (hlh : l≠h) (hhr : h≠r)
        (hu : u.length<N) (hv : v.length<N)
        (he : frame d l r h N u = x++frame d l r h N v++y) :
        x=[] ∧ u=v ∧ y=[] := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.frame

14. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.frame_last line 174
15. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.no_short_overlap line 181

    Source documentation

    A suffix ending in h cannot be a short prefix of a fresh header.

    theorem no_short_overlap {d l r h : S} {N : ℕ} {w m : List S}
        (hhd : h≠d) (hhl : h≠l) (hm : m.getLast? = some h)
        (hpre : m <+: frame d l r h N w) (hlen : m.length ≤ N+1) : False := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.frame

16. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.overlap_frame line 191

    Source documentation

    Aligned headers and guards exclude every proper same-stage boundary peak.

    theorem overlap_frame {d l r h : S} {N : ℕ} {u v p m q : List S}
        (hdl : d≠l) (hlr : l≠r) (hlh : l≠h) (hhr : h≠r) (hhd : h≠d)
        (hu : u.length<N) (hv : v.length<N) (hm : m≠[])
        (he₁ : frame d l r h N u = p++m)
        (he₂ : frame d l r h N v = m++q) : p=[] ∧ u=v ∧ q=[] := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.frame

17. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.reverse_frame line 219
18. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.short_long_overlap line 225

    Source documentation

    Different-stage boundary overlaps are excluded by spacing alone; this does not depend on which earlier stage passed its irreducibility test.

    theorem short_long_overlap {d l r h : S} {N M : ℕ} {u v p m q : List S}
        (hhd : h≠d) (hhl : h≠l) (hsmall : (frame d l r h N u).length≤M+1)
        (hm : m≠[]) (he : frame d l r h N u=p++m)
        (hf : frame d l r h M v=m++q) : False := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.frame

19. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.long_short_overlap line 238
20. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.avoiding_infix_frame line 251

    Source documentation

    General form of code containment: only avoidance of the four envelope markers is used, so it applies to either of the two disjoint code types.

    theorem avoiding_infix_frame {d l r h : S} {N : ℕ} {u w : List S}
        (hn : u≠[]) (hd : d∉u) (hl : l∉u) (hr : r∉u) (hh : h∉u)
        (hi : u <:+: frame d l r h N w) : u <:+: w := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.frame

21. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.avoiding_frame_overlap_left line 274

    Source documentation

    A code suffix cannot meet the first envelope marker.

    theorem avoiding_frame_overlap_left {d l r h : S} {N : ℕ} {u w p m q : List S}
        (hd : d∉u) (hm : m≠[]) (he : u=p++m) (hf : frame d l r h N w=m++q) : False := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.frame

22. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.avoiding_frame_overlap_right line 284

    Source documentation

    An envelope suffix cannot meet a code prefix because it ends in h.

    theorem avoiding_frame_overlap_right {d l r h : S} {N : ℕ} {u w p m q : List S}
        (hh : h∉u) (hm : m≠[]) (he : frame d l r h N w=p++m) (hf : u=m++q) : False := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Envelopes.frame

23. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.join_context line 297
24. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Critical line 303

    Source documentation

    The two critical configurations, checked only inside the current length ball.

    def Critical (rs : List (List S × List S)) (n : ℕ) : Prop :=
    …

25. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.critical_ordered line 310
26. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.step_decompose line 346
27. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.critical_localJoin line 352

    Source documentation

    Critical-pair reduction, including disjoint, boundary and containment peaks.

    theorem critical_localJoin {n : ℕ} (crit : Critical rs n) {w a b : List S}
        (hw : w.length≤n) (ha : Step rs w a) (hb : Step rs w b) : Join (Steps rs) a b := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Critical, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Step, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Steps

28. structure OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.Markers line 368
29. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.Markers.z_d line 378
30. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.Markers.z_l line 379
31. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.Markers.z_r line 380
32. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.Markers.z_h line 381
33. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.Markers.d_l line 382
34. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.Markers.d_r line 383
35. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.Markers.d_h line 384
36. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.Markers.l_r line 385
37. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.Markers.l_h line 386
38. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.Markers.r_h line 387
39. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.Markers.wrap line 389
40. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.Markers.wrap_avoids line 391
41. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.rules line 398

    Source documentation

    Literal selector rules, with the first member sent to the empty word.

    def rules (N : ℕ) (ws : List (List S)) : List (List S × List S) :=
    …

42. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.mem_rules line 401
43. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.Old line 407

    Source documentation

    The only possible old left-side shapes at a selector stage.

    def Old (N : ℕ) (u : List S) : Prop :=
    …

44. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.no_occurrence line 413
45. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.old_in_new line 419
46. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.new_in_old line 431
47. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.old_new_overlap line 442
48. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.new_old_overlap line 450
49. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.join_mono line 458
50. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.zero_join line 464
51. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.critical_extension line 473

    Source documentation

    The actual finite selector extension preserves the entire bounded critical condition, not just the disjoint cases. All irreducibility tests are on bodies.

    theorem critical_extension {rs : List (List S × List S)} {N B : ℕ} {ws : List (List S)}
        (hz : Absorbs rs a.zero) (hp : ∀ p∈rs,a.zero∈p.1 → a.zero∈p.2)
        (hold : ∀ p∈rs,Old a N p.1)
        (hws : ∀ w∈ws, w.length<N ∧ a.zero∉w ∧ Irreducible (Step rs) w)
        (hc : Critical rs B) : Critical (rs++rules a N ws) B := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Absorbs, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.Old, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Irreducible, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Step, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Critical, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.rules

52. structure OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.Stage line 540

    Source documentation

    A potential tuple and its envelope size, independent of all class tests.

    structure Stage (S : Type*) where
    …

53. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.allowed line 546
54. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.choose line 549
55. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.process line 552
56. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.BoundedEq line 556
57. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.allowed_iff line 559
58. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.irreducible_bounded line 572
59. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.choose_contains line 579
60. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.mem_choose line 587
61. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.choose_bounded line 594
62. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.process_bounded line 619
63. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.process_members line 627
64. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.process_contains line 639
65. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.process_zero line 645
66. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.process_critical line 657

    Source documentation

    Full consecutive selector processing preserves critical joins. The spacing is required for all potential earlier sides, selected or not.

    theorem process_critical {base : List (List S × List S)} {stages : ℕ → Stage S} {n : ℕ}
        (hz : Absorbs base a.zero) (hp : ∀ p ∈ base,a.zero ∈ p.1 → a.zero ∈ p.2)
        (hold : ∀ p ∈ base,a.zero ∈ p.1 ∨ (p.1≠[] ∧ a.d∉p.1 ∧ a.l∉p.1 ∧ a.r∉p.1 ∧ a.h∉p.1))
        (hbody : ∀ i w, w ∈ (stages i).bodies → w.length<(stages i).size ∧ a.zero∉w)
        (hspace : ∀ i j, i<j → ∀ w ∈ (stages i).bodies,(a.wrap (stages i).size w).length<(stages j).size)
        (hc : Critical base n) (j : ℕ) : Critical (process (a:=a) base stages n j) n := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.stages, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.Stage, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Absorbs, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Critical, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.process

67. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.boundedEq_refl line 686
68. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.boundedEq_trans line 690
69. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.choose_inert line 694
70. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.process_future line 707
71. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.tables_bounded line 717

    Source documentation

    Stability for the literal completed tables, whose number of examined tuples varies with the normalization bound.

    theorem tables_bounded {bases : ℕ → List (List S × List S)} {stages : ℕ → Stage S}
        (hb : ∀ k n, k ≤ n → BoundedEq (bases k) (bases n) k)
        (hlen : ∀ j w, w ∈ (stages j).bodies → w.length<(stages j).size)
        (hsize : ∀ j, j<(stages j).size) {k n : ℕ} (hkn : k ≤ n) :
        BoundedEq (process (a:=a) (bases k) stages k k)
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.stages, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.Stage, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.BoundedEq, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.process

72. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.rules_decrease line 726
73. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.process_decrease line 735
74. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.pickStep line 749
75. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.pick line 752
76. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.pick_class line 757
77. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.pick_least_fixed line 769
78. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.pick_eq_least line 785

    Source documentation

    The finite answer list computes the same least shortlex representative as the manuscript, even though it tests every word in the common length ball.

    theorem pick_eq_least {ps : List (List A × Q)} {w : List A}
        (hps : ∀ p ∈ ps,p.2=q p.1) (hm : (least wf q w,q w) ∈ ps) :
        pick (r:=r) ps w (q w)=least wf q w := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.least, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.pick

79. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.lexBool line 815
80. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.lexBool_eq line 821
81. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.lexFoldStep line 842
82. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.lexFinish line 848
83. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.lexFold line 850
84. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.primrec_lexBool line 869
85. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.primrec_shortlex line 894
86. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.output line 911
87. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.table line 915
88. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.compute line 919
89. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.traverse_map line 923
90. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.output_full line 934
91. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.table_full line 946
92. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.compute_full line 972
93. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.primrec_encode line 985
94. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.primrec_words line 989
95. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.primrec_pickStep line 998
96. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.primrec_pick line 1006
97. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.primrec_output line 1015
98. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.primrec_table line 1023
99. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.partrec_compute line 1039
100. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.maxLength line 1054
101. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.length_le_maxLength line 1057
102. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.tuples line 1066
103. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.tuples_valid line 1070
104. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.tuples_complete line 1078
105. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.sizes line 1085

     Source documentation

     Each new size is past the entire preceding potential envelope, not merely past those actually selected. The index and current body bounds are included.

     def sizes (z : S) : ℕ → ℕ
       | 0 => maxLength (tuples z 0)+1
       | i+1 => max (max (i+2) (maxLength (tuples z (i+1))+1))
           (2 * sizes z i+3+maxLength (tuples z i))

     Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.maxLength, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.tuples

106. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.stages line 1090
107. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.index_lt_size line 1092
108. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.body_lt_size line 1099
109. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.sizes_step line 1107
110. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.sizes_strictMono line 1111
111. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.stage_spacing line 1117
112. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.primrec_mem line 1128
113. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.primrec_dedup line 1131
114. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.primrec_nodup line 1144
115. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.primrec_maxLength line 1148
116. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.primrec_tuples line 1153
117. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.primrec_sizes line 1161
118. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.stageEquiv line 1179
119. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.(instance at line 1185) line 1185
120. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.primrec_stage_size line 1188
121. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.primrec_stage_bodies line 1191
122. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.primrec_stages line 1193
123. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.primrec_replicate line 1197
124. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.primrec_wrap line 1202
125. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.primrec_rules line 1208
126. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.primrec_allowed line 1215
127. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.primrec_choose line 1221
128. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.primrec_process line 1230
129. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.primrec_full_process line 1240