OAI/ModelTheory/Choiceless/Evaluation.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CPTSeparation.FullCPT.Term.elements_zero line 22
  2. def OAI.CPTSeparation.FullCPT.Term.pack line 26
  3. def OAI.CPTSeparation.FullCPT.Term.merge line 28
  4. def OAI.CPTSeparation.FullCPT.Term.merges line 30
  5. def OAI.CPTSeparation.FullCPT.Term.collect line 32
  6. lemma OAI.CPTSeparation.FullCPT.Term.eval_pack line 45
  7. lemma OAI.CPTSeparation.FullCPT.Term.eval_merge line 48
  8. lemma OAI.CPTSeparation.FullCPT.Term.eval_merges line 52
  9. lemma OAI.CPTSeparation.FullCPT.Term.eval_collect line 60
  10. lemma OAI.CPTSeparation.FullCPT.Term.eval_spread line 85
  11. def OAI.CPTSeparation.FullCPT.Rule.collect line 98
  12. lemma OAI.CPTSeparation.FullCPT.Rule.eval_collect line 107
  13. def OAI.CPTSeparation.FullCPT.Program.rootObserver line 128
  14. lemma OAI.CPTSeparation.FullCPT.Program.rootObserver_eval line 131
  15. lemma OAI.CPTSeparation.FullCPT.Program.observed_compile line 142
  16. lemma OAI.CPTSeparation.FullCPT.Program.evaluationAccepts_compile line 153
  17. theorem OAI.CPTSeparation.FullCPT.query_not_evaluationDefinable line 161