OAI/Computability/WitnessedChoice/EvaluationTrace.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WitnessedSeparation.Operational.closure_union_subset line 16
  2. lemma OAI.WitnessedSeparation.Operational.closure_unique_subset line 24
  3. lemma OAI.WitnessedSeparation.Operational.card_closure_card line 31
  4. lemma OAI.WitnessedSeparation.Operational.card_closure_boolean line 35
  5. lemma OAI.WitnessedSeparation.Operational.State.empty_mem_active line 42
  6. lemma OAI.WitnessedSeparation.Operational.State.atoms_mem_active line 46
  7. lemma OAI.WitnessedSeparation.Operational.State.closure_value_subset_active line 50
  8. lemma OAI.WitnessedSeparation.Operational.State.closure_atoms_subset_active line 58
  9. def OAI.WitnessedSeparation.Operational.Term.trace line 67
  10. lemma OAI.WitnessedSeparation.Operational.Term.closure_eval_subset_trace line 92
  11. def OAI.WitnessedSeparation.Operational.Term.bound line 124
  12. def OAI.WitnessedSeparation.Operational.Term.potential line 143
  13. lemma OAI.WitnessedSeparation.Operational.Term.potential_var line 146
  14. lemma OAI.WitnessedSeparation.Operational.Term.potential_active line 152
  15. lemma OAI.WitnessedSeparation.Operational.Term.potential_cons line 155
  16. lemma OAI.WitnessedSeparation.Operational.Term.card_trace_le line 160
  17. lemma OAI.WitnessedSeparation.Operational.member_count_iff line 295
  18. lemma OAI.WitnessedSeparation.Operational.uniform_double_value line 313
  19. lemma OAI.WitnessedSeparation.Operational.uniform_singleton_value line 319
  20. lemma OAI.WitnessedSeparation.Operational.uniform_atoms line 325
  21. lemma OAI.WitnessedSeparation.Operational.uniform_union line 362
  22. lemma OAI.WitnessedSeparation.Operational.uniform_unique line 399
  23. def OAI.WitnessedSeparation.Operational.BoundedCard line 441
  24. lemma OAI.WitnessedSeparation.Operational.uniform_card line 446
  25. lemma OAI.WitnessedSeparation.Operational.uniform_boolean line 466
  26. lemma OAI.WitnessedSeparation.Counting.UniformDefinable.forall_finset line 490
  27. lemma OAI.WitnessedSeparation.Counting.UniformDefinable.forall_finite line 496
  28. lemma OAI.WitnessedSeparation.Counting.UniformDefinable.append_cons line 501
  29. lemma OAI.WitnessedSeparation.Counting.UniformDefinable.exists_vec line 507
  30. lemma OAI.WitnessedSeparation.Counting.UniformDefinable.compose_unary line 534
  31. lemma OAI.WitnessedSeparation.Counting.UniformDefinable.compose_binary line 550
  32. lemma OAI.WitnessedSeparation.Counting.UniformDefinable.compose_vec line 573
  33. def OAI.WitnessedSeparation.Operational.Term.Graph line 617
  34. lemma OAI.WitnessedSeparation.Operational.Term.graph_sound line 647
  35. lemma OAI.WitnessedSeparation.Operational.Term.eval_mem_trace line 704
  36. lemma OAI.WitnessedSeparation.Operational.Term.graph_complete line 709
  37. lemma OAI.WitnessedSeparation.Operational.uniform_comprehension line 837
  38. def OAI.WitnessedSeparation.Operational.Term.width line 883
  39. lemma OAI.WitnessedSeparation.Operational.Term.uniform_graph line 913
  40. def OAI.WitnessedSeparation.Operational.Rule.trace line 1044
  41. def OAI.WitnessedSeparation.Operational.Rule.bound line 1053
  42. lemma OAI.WitnessedSeparation.Operational.Rule.closure_update_subset_trace line 1061
  43. lemma OAI.WitnessedSeparation.Operational.Rule.card_trace_le line 1098