OAI/NumberTheory/TwoPoint/Circuits/CircuitPartialAssignment.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Partial assignments and the consistent terms used in the canonical decision tree of a DNF. Each term contains at most one literal per variable.

  1. abbrev OAI.TwoPointCorrelations.PartialAssignment line 13
  2. def OAI.TwoPointCorrelations.PartialAssignment.apply line 17
  3. def OAI.TwoPointCorrelations.PartialAssignment.Extends line 20
  4. def OAI.TwoPointCorrelations.PartialAssignment.assign line 23
  5. def OAI.TwoPointCorrelations.PartialAssignment.free line 26
  6. lemma OAI.TwoPointCorrelations.PartialAssignment.assign_empty line 29
  7. lemma OAI.TwoPointCorrelations.PartialAssignment.assign_insert line 32
  8. lemma OAI.TwoPointCorrelations.PartialAssignment.apply_assign_free line 38
  9. lemma OAI.TwoPointCorrelations.PartialAssignment.assign_extends line 47
  10. lemma OAI.TwoPointCorrelations.PartialAssignment.extends_trans line 57
  11. structure OAI.TwoPointCorrelations.CubeTerm line 63
  12. def OAI.TwoPointCorrelations.CubeTerm.eval line 69
  13. def OAI.TwoPointCorrelations.CubeTerm.Compatible line 72
  14. def OAI.TwoPointCorrelations.CubeTerm.Satisfied line 75
  15. def OAI.TwoPointCorrelations.CubeTerm.live line 78
  16. lemma OAI.TwoPointCorrelations.CubeTerm.live_subset_free line 81
  17. lemma OAI.TwoPointCorrelations.CubeTerm.incompatible_mono line 86
  18. lemma OAI.TwoPointCorrelations.CubeTerm.eval_apply_of_incompatible line 101
  19. lemma OAI.TwoPointCorrelations.CubeTerm.satisfied_assign_live_iff line 116
  20. lemma OAI.TwoPointCorrelations.CubeTerm.satisfied_assign_value line 137