OAI/NumberTheory/Ostmann/Arithmetic/HistorySmoothWeightSlots.lean
11 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.independentSlotline 10 - def
OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.AtomSlotsCorrectline 15 - theorem
OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.atomSlots_reorderline 19 - theorem
OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.atomSlots_leftPartline 28 - theorem
OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.atomSlots_rightPartline 34 - theorem
OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.atomSlots_appendline 40 - def
OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.StateAtomSlotsline 52 - theorem
OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.children_atomSlotsline 55 - def
OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.TreeAtomSlotsline 68 - theorem
OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.encode_atomSlotsline 73 - theorem
OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.symbolicHistory_atomSlotsline 91