OAI/Computability/DegreeRigidity/Syntax/FiniteTerm.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.BoundedSetTheory.FiniteTerm.tag line 12
2. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTerm.tag_inj line 14
3. inductive OAI.TuringRigidity.BoundedSetTheory.FiniteTerm.Eval line 18
4. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTerm.Eval.value_mem line 25
5. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTerm.Eval.code_finite line 31
6. def OAI.TuringRigidity.BoundedSetTheory.FiniteTerm.Step line 41
7. def OAI.TuringRigidity.BoundedSetTheory.FiniteTerm.Certificate line 48
8. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTerm.Step.mono line 51
9. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTerm.Certificate.subset line 60
10. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTerm.Certificate.step line 66
11. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTerm.pair_rank_left line 73
12. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTerm.pair_rank_right line 78
13. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTerm.Certificate.sound line 83