OAI/Computability/MaxCut/Encoding/BitValue.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OptimalMaxCut.CounterMachine.Expr.bitValue line 11
  2. def OAI.OptimalMaxCut.CounterMachine.Expr.zeroPrefix line 13
  3. def OAI.OptimalMaxCut.CounterMachine.Expr.wordValue line 16
  4. def OAI.OptimalMaxCut.CounterMachine.Expr.prefixZeros line 19
  5. def OAI.OptimalMaxCut.CounterMachine.Expr.word line 20
  6. theorem OAI.OptimalMaxCut.CounterMachine.Expr.prefixZeros_eval line 23
  7. theorem OAI.OptimalMaxCut.CounterMachine.Expr.word_eval line 30
  8. theorem OAI.OptimalMaxCut.CounterMachine.Expr.bitValue_cons_zero line 35
  9. theorem OAI.OptimalMaxCut.CounterMachine.Expr.bitValue_cons_succ line 37
  10. theorem OAI.OptimalMaxCut.CounterMachine.Expr.zeroPrefix_zero line 39
  11. theorem OAI.OptimalMaxCut.CounterMachine.Expr.zeroPrefix_cons_succ line 40
  12. theorem OAI.OptimalMaxCut.CounterMachine.Expr.wordValue_nil line 46
  13. theorem OAI.OptimalMaxCut.CounterMachine.Expr.wordValue_true line 48
  14. theorem OAI.OptimalMaxCut.CounterMachine.Expr.wordValue_false_zero line 53
  15. theorem OAI.OptimalMaxCut.CounterMachine.Expr.wordValue_false_succ line 57
  16. theorem OAI.OptimalMaxCut.CounterMachine.Expr.wordValue_block_zero line 62
  17. theorem OAI.OptimalMaxCut.CounterMachine.Expr.wordValue_block_succ line 68
  18. def OAI.OptimalMaxCut.CounterMachine.Expr.unaryWords line 74
  19. theorem OAI.OptimalMaxCut.CounterMachine.Expr.wordValue_encoded line 76