OAI/Combinatorics/ParityLifts/GraphPrograms.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ParityWL.Complexity.PolyProgram.finite2 line 7
  2. def OAI.ParityWL.Complexity.PolyProgram.choiceEntry line 15
  3. def OAI.ParityWL.Complexity.PolyProgram.choiceBound line 28
  4. def OAI.ParityWL.Complexity.PolyProgram.choiceLabel line 38
  5. def OAI.ParityWL.Complexity.roleCode line 47

    Source documentation

    The finite role data is compiled into finite control, independent of table size.

    noncomputable def roleCode {t : ℕ} [NeZero t] : TemplateVertex t → Bool × (Fin t × Fin t)
  | .inl i => (false,(i,i))
  | .inr h => (true,(h.1.1.1.1,h.1.1.1.2))

    Mentions: OAI.ParityWL.TemplateVertex

  6. def OAI.ParityWL.Complexity.PolyProgram.indexSize line 51
  7. def OAI.ParityWL.Complexity.PolyProgram.vertices line 70
  8. def OAI.ParityWL.Complexity.baseRule line 81

    Source documentation

    0 and 1 are constants; 2 compares two labels; 3 and 4 compare a label and a helper value.

    def baseRule {t : ℕ} [NeZero t] : TemplateVertex t → TemplateVertex t → Fin 5 × (Fin t × Fin t)
  | .inl i, .inl j => (if i=j then 0 else 2,(i,j))
  | .inl i, .inr h =>
    if i=h.1.1.1.1 then (3,(i,h.1.1.1.2))
    else if i=h.1.1.1.2 then (3,(i,h.1.1.1.1))
    else (if i=h.1.2 then 1 else 0,(0,0))
  | .inr h, .inl i =>
    if i=h.1.1.1.1 then (4,(i,h.1.1.1.2))
    else if i=h.1.1.1.2 then (4,(i,h.1.1.1.1))
    else (if i=h.1.2 then 1 else 0,(0,0))
  | .inr _, .inr _ => (0,(0,0))

    Mentions: OAI.ParityWL.TemplateVertex

  9. def OAI.ParityWL.Complexity.evalRule line 93
  10. lemma OAI.ParityWL.Complexity.eval_baseRule line 99
  11. def OAI.ParityWL.Complexity.edgeRule line 115
  12. lemma OAI.ParityWL.Complexity.eval_edgeRule line 120
  13. def OAI.ParityWL.Complexity.PolyProgram.evalRule line 127
  14. def OAI.ParityWL.Complexity.PolyProgram.edgeTest line 162
  15. def OAI.ParityWL.Complexity.ChoiceData.matrix line 177
  16. def OAI.ParityWL.Complexity.PolyProgram.matrixRow line 180
  17. def OAI.ParityWL.Complexity.PolyProgram.matrixRows line 191
  18. def OAI.ParityWL.Complexity.PolyProgram.rowMatrix line 196
  19. def OAI.ParityWL.Complexity.PolyProgram.matrix line 201