OAI/Computability/WitnessedChoice/GuardedProgram.lean

GitHub source file

169 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WitnessedChoice.BGS.QuotedTerm.witnessRelations line 19
  2. def OAI.WitnessedChoice.BGS.QuotedTerm.guardedChoice line 25
  3. def OAI.WitnessedChoice.BGS.QuotedTerm.selectionStep line 30
  4. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_cond line 35
  5. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_witnessRelations line 38
  6. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_guardedChoice line 75
  7. lemma OAI.WitnessedChoice.BGS.QuotedTerm.uniqueHF_atom line 102
  8. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_unique line 108
  9. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_inter line 111
  10. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_selectionStep line 116
  11. def OAI.WitnessedChoice.BGS.QuotedTerm.triple line 163
  12. def OAI.WitnessedChoice.BGS.QuotedTerm.successor line 165
  13. def OAI.WitnessedChoice.BGS.QuotedTerm.indices line 167
  14. def OAI.WitnessedChoice.BGS.QuotedFormula.incident line 175
  15. def OAI.WitnessedChoice.BGS.QuotedFormula.adjacent line 178
  16. def OAI.WitnessedChoice.BGS.QuotedTerm.distanceBase line 187
  17. def OAI.WitnessedChoice.BGS.QuotedTerm.distanceFresh line 189
  18. def OAI.WitnessedChoice.BGS.QuotedTerm.distanceStep line 198
  19. def OAI.WitnessedChoice.BGS.QuotedTerm.tripleDomain line 201
  20. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_triple line 206
  21. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_successor line 210
  22. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_card line 214
  23. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_indices line 216
  24. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_incident line 226
  25. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_adjacent line 230
  26. structure OAI.WitnessedChoice.BGS.CPTTerm line 240
  27. structure OAI.WitnessedChoice.BGS.CPTFormula line 244
  28. def OAI.WitnessedChoice.BGS.CPTTerm.value line 252
  29. lemma OAI.WitnessedChoice.BGS.CPTTerm.eval_value line 255
  30. lemma OAI.WitnessedChoice.BGS.CPTTerm.value_eq line 258
  31. def OAI.WitnessedChoice.BGS.CPTTerm.quoted line 262
  32. def OAI.WitnessedChoice.BGS.CPTTerm.var line 264
  33. def OAI.WitnessedChoice.BGS.CPTTerm.rename line 266
  34. def OAI.WitnessedChoice.BGS.CPTTerm.up line 269
  35. def OAI.WitnessedChoice.BGS.CPTTerm.letIn line 271
  36. def OAI.WitnessedChoice.BGS.CPTTerm.iterate line 275
  37. lemma OAI.WitnessedChoice.BGS.CPTTerm.value_quoted line 277
  38. lemma OAI.WitnessedChoice.BGS.CPTTerm.value_var line 280
  39. lemma OAI.WitnessedChoice.BGS.CPTTerm.value_rename line 283
  40. lemma OAI.WitnessedChoice.BGS.CPTTerm.value_up line 289
  41. lemma OAI.WitnessedChoice.BGS.CPTTerm.value_letIn line 292
  42. lemma OAI.WitnessedChoice.BGS.CPTTerm.eval_iterate line 298
  43. def OAI.WitnessedChoice.BGS.CPTTerm.unary line 303
  44. def OAI.WitnessedChoice.BGS.CPTTerm.binary line 305
  45. def OAI.WitnessedChoice.BGS.CPTTerm.distance line 308
  46. def OAI.WitnessedChoice.BGS.CPTFormula.value line 317
  47. lemma OAI.WitnessedChoice.BGS.CPTFormula.eval_value line 320
  48. lemma OAI.WitnessedChoice.BGS.CPTFormula.value_eq line 323
  49. def OAI.WitnessedChoice.BGS.CPTFormula.quoted line 327
  50. def OAI.WitnessedChoice.BGS.CPTFormula.rename line 329
  51. def OAI.WitnessedChoice.BGS.CPTFormula.up line 332
  52. def OAI.WitnessedChoice.BGS.CPTFormula.letIn line 334
  53. lemma OAI.WitnessedChoice.BGS.CPTFormula.value_quoted line 338
  54. lemma OAI.WitnessedChoice.BGS.CPTFormula.value_rename line 341
  55. lemma OAI.WitnessedChoice.BGS.CPTFormula.value_up line 347
  56. lemma OAI.WitnessedChoice.BGS.CPTFormula.value_letIn line 350
  57. def OAI.WitnessedChoice.BGS.QuotedTerm.nat line 365
  58. def OAI.WitnessedChoice.BGS.QuotedTerm.fst line 369
  59. def OAI.WitnessedChoice.BGS.QuotedTerm.snd line 372
  60. def OAI.WitnessedChoice.BGS.QuotedTerm.component line 376
  61. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_union line 382
  62. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_diff line 385
  63. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_nat line 389
  64. lemma OAI.WitnessedChoice.BGS.QuotedTerm.cardHF_singleton line 395
  65. lemma OAI.WitnessedChoice.BGS.QuotedTerm.cardHF_double_ne line 399
  66. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_fst_pair line 405
  67. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_snd_pair line 433
  68. def OAI.WitnessedChoice.BGS.QuotedTerm.tupleProduct line 461
  69. lemma OAI.WitnessedChoice.BGS.QuotedTerm.mem_tupleProduct line 467
  70. def OAI.WitnessedChoice.BGS.QuotedTerm.blockParameters line 491
  71. lemma OAI.WitnessedChoice.BGS.QuotedTerm.mem_blockParameters line 493
  72. lemma OAI.WitnessedChoice.BGS.collect_on line 512
  73. lemma OAI.WitnessedChoice.BGS.Formula.eval_existsIn_on line 539
  74. def OAI.WitnessedChoice.BGS.QuotedFormula.falsehood line 558
  75. def OAI.WitnessedChoice.BGS.QuotedFormula.anyList line 560
  76. def OAI.WitnessedChoice.BGS.QuotedFormula.allFin line 564
  77. def OAI.WitnessedChoice.BGS.QuotedFormula.anyFin line 566
  78. def OAI.WitnessedChoice.BGS.QuotedFormula.nonempty line 568
  79. def OAI.WitnessedChoice.BGS.QuotedTerm.distanceAt line 576
  80. def OAI.WitnessedChoice.BGS.QuotedFormula.connected line 589
  81. def OAI.WitnessedChoice.BGS.QuotedFormula.resolving line 592
  82. def OAI.WitnessedChoice.BGS.QuotedFormula.vertexLt line 597
  83. def OAI.WitnessedChoice.BGS.QuotedFormula.leastVertex line 603
  84. def OAI.WitnessedChoice.BGS.QuotedFormula.hasEndpoints line 606
  85. def OAI.WitnessedChoice.BGS.QuotedFormula.edgeLt line 609
  86. def OAI.WitnessedChoice.BGS.QuotedFormula.parentEligible line 619
  87. def OAI.WitnessedChoice.BGS.QuotedFormula.parent line 622
  88. def OAI.WitnessedChoice.BGS.QuotedTerm.root line 635
  89. def OAI.WitnessedChoice.BGS.QuotedTerm.tree line 638
  90. def OAI.WitnessedChoice.BGS.QuotedTerm.nextEdges line 644
  91. def OAI.WitnessedChoice.BGS.SourceSyntax.next4 line 657
  92. def OAI.WitnessedChoice.BGS.SourceSyntax.prev4 line 659
  93. def OAI.WitnessedChoice.BGS.SourceSyntax.fv line 661
  94. def OAI.WitnessedChoice.BGS.SourceSyntax.fe line 663
  95. def OAI.WitnessedChoice.BGS.SourceSyntax.faceDescription line 665
  96. def OAI.WitnessedChoice.BGS.SourceSyntax.faces line 670
  97. def OAI.WitnessedChoice.BGS.SourceSyntax.adjacentMatch line 674
  98. def OAI.WitnessedChoice.BGS.SourceSyntax.matchFace line 679
  99. def OAI.WitnessedChoice.BGS.SourceSyntax.side line 687
  100. def OAI.WitnessedChoice.BGS.SourceSyntax.onSide line 690
  101. def OAI.WitnessedChoice.BGS.SourceSyntax.baseEq line 693
  102. def OAI.WitnessedChoice.BGS.SourceSyntax.candidates line 696
  103. def OAI.WitnessedChoice.BGS.CPTTerm.comprehend line 708
  104. def OAI.WitnessedChoice.BGS.CPTTerm.map line 712
  105. def OAI.WitnessedChoice.BGS.CPTTerm.union line 715
  106. def OAI.WitnessedChoice.BGS.CPTTerm.bind line 717
  107. theorem OAI.WitnessedChoice.BGS.CPTTerm.value_comprehend line 719
  108. theorem OAI.WitnessedChoice.BGS.CPTTerm.value_map line 728
  109. theorem OAI.WitnessedChoice.BGS.CPTTerm.value_union line 736
  110. theorem OAI.WitnessedChoice.BGS.CPTTerm.value_bind line 741
  111. def OAI.WitnessedChoice.BGS.decodeRelation line 756
  112. lemma OAI.WitnessedChoice.BGS.decodeRelation_code line 759
  113. def OAI.WitnessedChoice.BGS.QuotedTerm.normalizeRelation line 767
  114. def OAI.WitnessedChoice.BGS.QuotedTerm.normalizeRelations line 770
  115. def OAI.WitnessedChoice.BGS.QuotedTerm.normalizeCandidates line 772
  116. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_normalizeRelation line 775
  117. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_normalizeRelations line 781
  118. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_normalizeCandidates line 786
  119. def OAI.WitnessedChoice.BGS.CPTTerm.normalizeCandidates line 801
  120. def OAI.WitnessedChoice.BGS.CPTTerm.normalizeRelations line 804
  121. lemma OAI.WitnessedChoice.BGS.CPTTerm.value_normalizeCandidates line 807
  122. lemma OAI.WitnessedChoice.BGS.CPTTerm.value_normalizeRelations line 812
  123. structure OAI.WitnessedChoice.BGS.GuardedProgram line 819
  124. def OAI.WitnessedChoice.BGS.GuardedProgram.witnesses line 829
  125. def OAI.WitnessedChoice.BGS.GuardedProgram.choice line 832
  126. def OAI.WitnessedChoice.BGS.GuardedProgram.step line 835
  127. def OAI.WitnessedChoice.BGS.GuardedProgram.witness line 837
  128. def OAI.WitnessedChoice.BGS.GuardedProgram.formula line 839
  129. lemma OAI.WitnessedChoice.BGS.GuardedProgram.count line 841
  130. def OAI.WitnessedChoice.BGS.GuardedProgram.candidateSet line 846
  131. def OAI.WitnessedChoice.BGS.GuardedProgram.cycleSet line 850
  132. def OAI.WitnessedChoice.BGS.GuardedProgram.selection line 853
  133. lemma OAI.WitnessedChoice.BGS.GuardedProgram.candidates_eq line 856
  134. lemma OAI.WitnessedChoice.BGS.GuardedProgram.candidate_edge line 859
  135. lemma OAI.WitnessedChoice.BGS.GuardedProgram.witnesses_value line 864
  136. lemma OAI.WitnessedChoice.BGS.GuardedProgram.choice_value line 874
  137. lemma OAI.WitnessedChoice.BGS.GuardedProgram.realizes line 885
  138. theorem OAI.WitnessedChoice.BGS.GuardedProgram.boolean line 908
  139. structure OAI.WitnessedChoice.BGS.ClosedGuardedProgram line 923
  140. def OAI.WitnessedChoice.BGS.ClosedGuardedProgram.parameterTerm line 931
  141. def OAI.WitnessedChoice.BGS.ClosedGuardedProgram.formula line 934
  142. def OAI.WitnessedChoice.BGS.ClosedGuardedProgram.sentence line 936
  143. lemma OAI.WitnessedChoice.BGS.ClosedGuardedProgram.count line 938
  144. lemma OAI.WitnessedChoice.BGS.ClosedGuardedProgram.parameter_mem line 944
  145. theorem OAI.WitnessedChoice.BGS.ClosedGuardedProgram.boolean line 951
  146. theorem OAI.WitnessedChoice.BGS.ClosedGuardedProgram.boolean_all line 963
  147. def OAI.WitnessedChoice.BGS.SourceSyntax.connWithout line 977
  148. def OAI.WitnessedChoice.BGS.SourceSyntax.traversal line 980
  149. def OAI.WitnessedChoice.BGS.SourceSyntax.traversalEdge line 988
  150. def OAI.WitnessedChoice.BGS.SourceSyntax.directedZ line 991
  151. def OAI.WitnessedChoice.BGS.SourceSyntax.cycleY line 998
  152. def OAI.WitnessedChoice.BGS.SourceSyntax.cycleX line 1005
  153. def OAI.WitnessedChoice.BGS.SourceSyntax.cycleRelation line 1012
  154. def OAI.WitnessedChoice.BGS.SourceSyntax.cycleRelations line 1015
  155. def OAI.WitnessedChoice.BGS.SourceSyntax.complete line 1022
  156. def OAI.WitnessedChoice.BGS.SourceSyntax.allowed line 1027
  157. def OAI.WitnessedChoice.BGS.SourceSyntax.unsupported line 1031
  158. def OAI.WitnessedChoice.BGS.SourceSyntax.deletedStep line 1038
  159. def OAI.WitnessedChoice.BGS.SourceProgram.distances line 1049
  160. def OAI.WitnessedChoice.BGS.SourceProgram.parameters line 1051
  161. def OAI.WitnessedChoice.BGS.SourceProgram.candidates line 1054
  162. def OAI.WitnessedChoice.BGS.SourceProgram.connTable line 1059
  163. def OAI.WitnessedChoice.BGS.SourceProgram.cycles line 1063
  164. def OAI.WitnessedChoice.BGS.SourceProgram.output line 1069
  165. def OAI.WitnessedChoice.BGS.SourceProgram.program line 1076
  166. theorem OAI.WitnessedChoice.BGS.SourceProgram.one_occurrence line 1083
  167. theorem OAI.WitnessedChoice.BGS.SourceProgram.boolean_all line 1085
  168. theorem OAI.WitnessedChoice.BGS.QuotedTerm.closure_bound line 1095
  169. theorem OAI.WitnessedChoice.BGS.QuotedTerm.TC_bound line 1104