OAI/NumberTheory/SingleFold/CounterCompilation.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleFold.Compiler.ScalarSF.finset_sum line 7
  2. lemma OAI.SingleFold.Compiler.ScalarSF.sum line 15
  3. lemma OAI.SingleFold.Compiler.ScalarSF.bits line 17
  4. inductive OAI.SingleFold.CounterCompilation.Var line 24
  5. def OAI.SingleFold.CounterCompilation.encode line 30
  6. def OAI.SingleFold.CounterCompilation.decode line 35
  7. lemma OAI.SingleFold.CounterCompilation.decode_encode line 39
  8. lemma OAI.SingleFold.CounterCompilation.encode_decode line 40
  9. lemma OAI.SingleFold.CounterCompilation.decode_injective line 42
  10. abbrev OAI.SingleFold.CounterCompilation.Input line 48
  11. abbrev OAI.SingleFold.CounterCompilation.inp line 49
  12. abbrev OAI.SingleFold.CounterCompilation.wit line 50
  13. lemma OAI.SingleFold.CounterCompilation.field_sf line 52
  14. lemma OAI.SingleFold.CounterCompilation.input_sf line 54
  15. lemma OAI.SingleFold.CounterCompilation.baseC_sf line 56
  16. lemma OAI.SingleFold.CounterCompilation.arc_sf line 59
  17. lemma OAI.SingleFold.CounterCompilation.incoming_sf line 63
  18. lemma OAI.SingleFold.CounterCompilation.increments_sf line 72
  19. lemma OAI.SingleFold.CounterCompilation.decrements_sf line 83
  20. lemma OAI.SingleFold.CounterCompilation.branch_sf line 95
  21. lemma OAI.SingleFold.CounterCompilation.zero_test_sf line 117
  22. lemma OAI.SingleFold.CounterCompilation.system_sf line 131
  23. lemma OAI.SingleFold.CounterCompilation.halts_sf line 168