OAI/Combinatorics/IndependentSets/Machines/LengthLoop.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsCut.CounterMachine.Command.lengthLoop line 12
2. theorem OAI.IndependentSetsCut.CounterMachine.Command.lengthLoop_evaluates line 15
3. def OAI.IndependentSetsCut.CounterMachine.Command.inputLength line 63
4. theorem OAI.IndependentSetsCut.CounterMachine.Command.inputLength_evaluates line 65
5. inductive OAI.IndependentSetsCut.CounterMachine.Expr line 93
6. def OAI.IndependentSetsCut.CounterMachine.Expr.bind line 106
7. def OAI.IndependentSetsCut.CounterMachine.Expr.eval line 110
8. def OAI.IndependentSetsCut.CounterMachine.Expr.valueBudget line 121
9. theorem OAI.IndependentSetsCut.CounterMachine.Expr.eval_le line 132
10. def OAI.IndependentSetsCut.CounterMachine.Expr.timeBudget line 158
11. def OAI.IndependentSetsCut.CounterMachine.Expr.compile line 171
12. def OAI.IndependentSetsCut.CounterMachine.Data.Clean line 190
13. theorem OAI.IndependentSetsCut.CounterMachine.Data.Clean.mono line 192
14. theorem OAI.IndependentSetsCut.CounterMachine.Data.Clean.set_succ line 195
15. theorem OAI.IndependentSetsCut.CounterMachine.Data.set_args line 201
16. theorem OAI.IndependentSetsCut.CounterMachine.Data.set_clean_zero line 206