OAI/Analysis/MatrixSigning/Realization/PairRoutine.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentKS.PairRoutine.pair line 12
  2. def OAI.CurrentKS.PairRoutine.smallState line 14
  3. def OAI.CurrentKS.PairRoutine.split line 15
  4. def OAI.CurrentKS.PairRoutine.first line 16
  5. def OAI.CurrentKS.PairRoutine.second line 18
  6. lemma OAI.CurrentKS.PairRoutine.split_spec line 20
  7. lemma OAI.CurrentKS.PairRoutine.clear_first line 25
  8. lemma OAI.CurrentKS.PairRoutine.take_first line 32
  9. lemma OAI.CurrentKS.PairRoutine.clear_second line 39
  10. def OAI.CurrentKS.PairRoutine.fstRoutine line 46
  11. def OAI.CurrentKS.PairRoutine.sndRoutine line 54
  12. abbrev OAI.CurrentKS.PairRoutine.saved line 62
  13. abbrev OAI.CurrentKS.PairRoutine.left line 63
  14. abbrev OAI.CurrentKS.PairRoutine.work line 64
  15. def OAI.CurrentKS.PairRoutine.ports line 65
  16. def OAI.CurrentKS.PairRoutine.state line 66
  17. def OAI.CurrentKS.PairRoutine.copyPorts line 68
  18. def OAI.CurrentKS.PairRoutine.framePorts line 70
  19. lemma OAI.CurrentKS.PairRoutine.copyPorts_apply line 73
  20. lemma OAI.CurrentKS.PairRoutine.framePorts_apply line 76
  21. lemma OAI.CurrentKS.PairRoutine.projection line 79
  22. lemma OAI.CurrentKS.PairRoutine.outside line 85
  23. lemma OAI.CurrentKS.PairRoutine.element_spec line 92
  24. lemma OAI.CurrentKS.PairRoutine.copy_spec line 98
  25. lemma OAI.CurrentKS.PairRoutine.frame_spec line 108
  26. lemma OAI.CurrentKS.PairRoutine.save_first_spec line 118
  27. lemma OAI.CurrentKS.PairRoutine.restore_spec line 130
  28. lemma OAI.CurrentKS.PairRoutine.prepend_spec line 143
  29. def OAI.CurrentKS.PairRoutine.pairingProgram line 158
  30. def OAI.CurrentKS.PairRoutine.pairingTicks line 167
  31. lemma OAI.CurrentKS.PairRoutine.pairing_spec line 172
  32. def OAI.CurrentKS.PairRoutine.pairing line 189