OAI/Computability/WitnessedChoice/TermGraphs.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WitnessedChoice.BGS.LoopGraph line 15
  2. lemma OAI.WitnessedChoice.BGS.domain_cons_val line 60
  3. lemma OAI.WitnessedChoice.BGS.LoopGraph.sound line 65
  4. def WitnessedChoice.BGS.AdmissibleTrace line 192
  5. lemma WitnessedChoice.BGS.AdmissibleTrace.mono line 195
  6. lemma WitnessedChoice.BGS.admissibleTrace_of_closed line 199
  7. lemma WitnessedChoice.BGS.LoopGraph.complete line 204
  8. lemma WitnessedChoice.BGS.uniform_const line 360
  9. lemma WitnessedChoice.BGS.uniform_exists_finite line 365
  10. lemma WitnessedChoice.BGS.uniform_decide line 371
  11. lemma WitnessedChoice.BGS.uniform_formula_binary line 378
  12. lemma WitnessedChoice.BGS.uniform_BGS_comprehension line 410
  13. lemma WitnessedChoice.BGS.LoopGraph.uniform line 444
  14. lemma WitnessedChoice.BGS.unionHF_eq_operational line 491
  15. lemma WitnessedChoice.BGS.uniqueHF_eq_operational line 497
  16. lemma WitnessedChoice.BGS.cardHF_eq_operational line 499
  17. lemma WitnessedChoice.BGS.atomsHF_eq_operational line 501
  18. lemma WitnessedChoice.BGS.lift_emptyHF line 685
  19. lemma WitnessedChoice.BGS.lift_unionHF line 687
  20. lemma WitnessedChoice.BGS.lift_uniqueHF line 690
  21. lemma WitnessedChoice.BGS.lift_cardHF line 693
  22. lemma WitnessedChoice.BGS.lift_atomsHF line 696
  23. lemma WitnessedChoice.BGS.lift_inputHF line 700
  24. lemma WitnessedChoice.BGS.lift_closureHF line 710
  25. lemma WitnessedChoice.BGS.lift_TC line 717
  26. lemma WitnessedChoice.BGS.lift_TC_card line 721
  27. lemma WitnessedChoice.BGS.lift_cons line 725
  28. lemma WitnessedChoice.BGS.tracedLoop_transport line 731
  29. lemma WitnessedChoice.BGS.selected_transport line 747
  30. lemma WitnessedChoice.BGS.realPolynomial_majorant line 828
  31. lemma WitnessedChoice.BGS.resource_majorant line 842
  32. lemma WitnessedChoice.BGS.Formula.grid_trace_invariant line 865
  33. lemma WitnessedChoice.BGS.Formula.grid_trace_supported line 878
  34. lemma WitnessedChoice.BGS.Formula.grid_traced_agrees line 890
  35. def WitnessedChoice.BGS.gridInput line 953
  36. theorem WitnessedChoice.BGS.Sentence.agrees_on_some_grid_pair line 956
  37. def WitnessedChoice.fullAut line 1018
  38. def WitnessedChoice.paramAut line 1029
  39. def WitnessedChoice.stateCode line 1032
  40. def WitnessedChoice.choiceCode line 1034
  41. structure WitnessedChoice.Selection line 1038
  42. def WitnessedChoice.Selection.TransitiveAt line 1046
  43. def WitnessedChoice.Selection.choices line 1050
  44. def WitnessedChoice.Selection.advance line 1055
  45. def WitnessedChoice.Selection.Prefix line 1059
  46. def WitnessedChoice.Selection.FirstStabilization line 1062
  47. def WitnessedChoice.Selection.witnessAt line 1065
  48. def WitnessedChoice.Selection.HistoryAut line 1068
  49. def WitnessedChoice.Selection.WitnessedAt line 1072
  50. def WitnessedChoice.Selection.Filtered line 1079
  51. def WitnessedChoice.Selection.Fresh line 1084
  52. def WitnessedChoice.Selection.Equivariant line 1086