OAI/Computability/DepthThree/Model.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DepthThreeLowerBound.Cube line 9

   Also declared: ComparatorChallenges/DepthThree.lean:9 (same declaration text).

2. abbrev OAI.DepthThreeLowerBound.Literal line 10

   Also declared: ComparatorChallenges/DepthThree.lean:10 (same declaration text).

3. def OAI.DepthThreeLowerBound.Literal.eval line 16

   Also declared: ComparatorChallenges/DepthThree.lean:16 (same declaration text).

4. abbrev OAI.DepthThreeLowerBound.GateInput line 20

   Also declared: ComparatorChallenges/DepthThree.lean:20 (same declaration text).

5. abbrev OAI.DepthThreeLowerBound.RawClause line 21

   Also declared: ComparatorChallenges/DepthThree.lean:21 (same declaration text).

6. def OAI.DepthThreeLowerBound.GateInput.eval line 25

   Also declared: ComparatorChallenges/DepthThree.lean:25 (same declaration text).

7. def OAI.DepthThreeLowerBound.RawClause.eval line 33

   Also declared: ComparatorChallenges/DepthThree.lean:33 (same declaration text).

8. structure OAI.DepthThreeLowerBound.Circuit3 line 39

   Also declared: ComparatorChallenges/DepthThree.lean:39 (same declaration text).

9. def OAI.DepthThreeLowerBound.Circuit3.gateCount line 48

   Also declared: ComparatorChallenges/DepthThree.lean:48 (same declaration text).

10. def OAI.DepthThreeLowerBound.Circuit3.middleEval line 50

    Also declared: ComparatorChallenges/DepthThree.lean:50 (same declaration text).

11. def OAI.DepthThreeLowerBound.Circuit3.eval line 55

    Also declared: ComparatorChallenges/DepthThree.lean:55 (same declaration text).

12. def OAI.DepthThreeLowerBound.Circuit3.Computes line 59

    Also declared: ComparatorChallenges/DepthThree.lean:59 (same declaration text).

13. def OAI.DepthThreeLowerBound.runSteps line 63

    Also declared: ComparatorChallenges/DepthThree.lean:63 (same declaration text).

14. inductive OAI.DepthThreeLowerBound.HeadMove line 66

    Also declared: ComparatorChallenges/DepthThree.lean:66 (same declaration text).

15. def OAI.DepthThreeLowerBound.HeadMove.apply line 71

    Also declared: ComparatorChallenges/DepthThree.lean:71 (same declaration text).

16. structure OAI.DepthThreeLowerBound.MultiTapeCfg line 76

    Also declared: ComparatorChallenges/DepthThree.lean:76 (same declaration text).

17. abbrev OAI.DepthThreeLowerBound.MultiTapeCode line 80

    Also declared: ComparatorChallenges/DepthThree.lean:80 (same declaration text).

18. def OAI.DepthThreeLowerBound.multiTapeUpdate line 83

    Also declared: ComparatorChallenges/DepthThree.lean:83 (same declaration text).

19. def OAI.DepthThreeLowerBound.multiTapeStep line 87

    Also declared: ComparatorChallenges/DepthThree.lean:87 (same declaration text).

20. structure OAI.DepthThreeLowerBound.FiniteMultiTapeMachine line 92

    Also declared: ComparatorChallenges/DepthThree.lean:92 (same declaration text).

21. abbrev OAI.DepthThreeLowerBound.FiniteMultiTapeMachine.Cfg line 115

    Also declared: ComparatorChallenges/DepthThree.lean:115 (same declaration text).

22. abbrev OAI.DepthThreeLowerBound.FiniteMultiTapeMachine.step line 117

    Also declared: ComparatorChallenges/DepthThree.lean:117 (same declaration text).

23. def OAI.DepthThreeLowerBound.FiniteMultiTapeMachine.init line 120

    Also declared: ComparatorChallenges/DepthThree.lean:120 (same declaration text).

24. def OAI.DepthThreeLowerBound.MultiTapeHaltsIn line 127

    Also declared: ComparatorChallenges/DepthThree.lean:127 (same declaration text).