OAI/GroupTheory/UniversalGroup/StackPrograms.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Higman.AffineStack.Counter line 11
  2. def OAI.Higman.AffineStack.scale line 13
  3. lemma OAI.Higman.AffineStack.scale_injective line 20
  4. inductive OAI.Higman.AffineStack.Op line 25
  5. def OAI.Higman.AffineStack.Op.Rel line 30
  6. def OAI.Higman.AffineStack.localEdge line 37
  7. instance OAI.Higman.AffineStack.localEdge_finitelyPresented line 50
  8. def OAI.Higman.AffineStack.encode line 59
  9. lemma OAI.Higman.AffineStack.encode_injective line 62
  10. theorem OAI.Higman.AffineStack.local_sound line 67
  11. theorem OAI.Higman.AffineStack.local_complete line 104
  12. abbrev OAI.Higman.AffineStack.Stores line 127
  13. abbrev OAI.Higman.AffineStack.Rest line 128
  14. def OAI.Higman.AffineStack.insertLinear line 130
  15. lemma OAI.Higman.AffineStack.insertLinear_apply line 136
  16. lemma OAI.Higman.AffineStack.insertLinear_injective line 140
  17. def OAI.Higman.AffineStack.insertOffset line 149
  18. def OAI.Higman.AffineStack.liftEdge line 151
  19. lemma OAI.Higman.AffineStack.liftEdge_finitelyPresented line 163
  20. inductive OAI.Higman.AffineStack.Action line 168
  21. def OAI.Higman.AffineStack.Action.Rel line 171
  22. def OAI.Higman.AffineStack.encodeStores line 178
  23. def OAI.Higman.AffineStack.actionEdge line 180
  24. lemma OAI.Higman.AffineStack.action_finitelyPresented line 185
  25. theorem OAI.Higman.AffineStack.action_sound line 192
  26. theorem OAI.Higman.AffineStack.action_complete line 222
  27. lemma OAI.Higman.AffineStack.actionEdge_inputState line 259
  28. lemma OAI.Higman.AffineStack.actionEdge_outputState line 265
  29. lemma OAI.Higman.AffineStack.actionEdge_weight line 271
  30. lemma OAI.Higman.AffineStack.encodeStores_injective line 281
  31. structure OAI.Higman.StackProgram.Instruction line 294
  32. def OAI.Higman.StackProgram.Instruction.edge line 300
  33. inductive OAI.Higman.StackProgram.Run line 303
  34. theorem OAI.Higman.StackProgram.run_sound line 315
  35. theorem OAI.Higman.StackProgram.run_complete line 329
  36. def OAI.Higman.StackProgram.outputs line 349
  37. theorem OAI.Higman.StackProgram.benign_outputs line 359