OAI/Combinatorics/ParityLifts/ProgramLoops.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ParityWL.Complexity.treeEncode_tree line 7
  2. lemma OAI.ParityWL.Complexity.TreeProgram.loop_wf line 9
  3. abbrev OAI.ParityWL.Complexity.EqualState line 36
  4. def OAI.ParityWL.Complexity.equalStep line 38
  5. def OAI.ParityWL.Complexity.equalExpr line 44
  6. lemma OAI.ParityWL.Complexity.equalExpr_eval line 55
  7. def OAI.ParityWL.Complexity.equalStepProgram line 63
  8. def OAI.ParityWL.Complexity.equalMeasure line 68
  9. def OAI.ParityWL.Complexity.equalGood line 70
  10. lemma OAI.ParityWL.Complexity.equalStep_good line 72
  11. lemma OAI.ParityWL.Complexity.equalStep_decreases line 80
  12. lemma OAI.ParityWL.Complexity.equalState_size line 91
  13. def OAI.ParityWL.Complexity.FCode.treeEqual line 107
  14. lemma OAI.ParityWL.Complexity.BEval.treeEqual line 111
  15. def OAI.ParityWL.Complexity.TreeProgram.equal line 152