OAI/Analysis/MatrixSigning/Realization/NaturalRealization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CurrentKS.Realization.natCode line 10
2. def OAI.CurrentKS.Realization.natSucc line 12
3. def OAI.CurrentKS.Realization.natPred line 22
4. def OAI.CurrentKS.Realization.natAdd line 32
5. def OAI.CurrentKS.Realization.Realizes.iterate line 43
6. def OAI.CurrentKS.Realization.rangeStep line 48
7. def OAI.CurrentKS.Realization.rangeStepRealizes line 49
8. lemma OAI.CurrentKS.Realization.rangeStep_iterate line 55
9. def OAI.CurrentKS.Realization.range line 62