OAI/NumberTheory/Ostmann/Arithmetic/HistorySymbolicScope.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.HistorySymbolicScope.Above line 14
  2. theorem OAI.Ostmann.Arithmetic.HistorySymbolicScope.above_mono line 19
  3. theorem OAI.Ostmann.Arithmetic.HistorySymbolicScope.above_atoms line 27
  4. theorem OAI.Ostmann.Arithmetic.HistorySymbolicScope.product_above line 41
  5. theorem OAI.Ostmann.Arithmetic.HistorySymbolicScope.product_ofFn_above line 47
  6. def OAI.Ostmann.Arithmetic.HistorySymbolicScope.StateAbove line 54
  7. theorem OAI.Ostmann.Arithmetic.HistorySymbolicScope.stateAbove_mono line 57
  8. theorem OAI.Ostmann.Arithmetic.HistorySymbolicScope.reorder_above line 61
  9. theorem OAI.Ostmann.Arithmetic.HistorySymbolicScope.append_above line 66
  10. theorem OAI.Ostmann.Arithmetic.HistorySymbolicScope.child_above line 82
  11. def OAI.Ostmann.Arithmetic.HistorySymbolicScope.TreeAbove line 101
  12. theorem OAI.Ostmann.Arithmetic.HistorySymbolicScope.encode_above line 106
  13. theorem OAI.Ostmann.Arithmetic.HistorySymbolicScope.symbolicHistory_above line 125