OAI/MathematicalPhysics/NavierStokes/VelocityDetection/StacksLookup.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VelocityDetection.Stacks.lookup line 14

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:203 (same declaration text).

  2. def OAI.VelocityDetection.Stacks.next line 17
  3. def OAI.VelocityDetection.Stacks.orbit line 20
  4. theorem OAI.VelocityDetection.Stacks.orbit_zero line 24
  5. theorem OAI.VelocityDetection.Stacks.orbit_succ line 26
  6. theorem OAI.VelocityDetection.Stacks.next_eq_of_lookup line 29
  7. theorem OAI.VelocityDetection.Stacks.next_eq_of_none line 33
  8. theorem OAI.VelocityDetection.Stacks.next_fits line 36
  9. theorem OAI.VelocityDetection.Stacks.orbit_fits line 50
  10. def OAI.VelocityDetection.Stacks.NoOutgoing line 58
  11. def OAI.VelocityDetection.Stacks.Continues line 60
  12. def OAI.VelocityDetection.Stacks.Reaches line 63
  13. theorem OAI.VelocityDetection.Stacks.lookup_source_nonterminal line 66
  14. theorem OAI.VelocityDetection.Stacks.next_terminal line 72