OAI/NumberTheory/TwoPoint/Circuits/CircuitCanonicalTree.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The canonical tree queries the unset variables of the first compatible term, then continues through the remaining terms. This concrete tree is the one encoded in the switching argument.

  1. def OAI.TwoPointCorrelations.BooleanDecisionTree.queryVariables line 17
  2. lemma OAI.TwoPointCorrelations.BooleanDecisionTree.queryVariables_eval line 24
  3. lemma OAI.TwoPointCorrelations.BooleanDecisionTree.queryVariables_depth_le line 42
  4. def OAI.TwoPointCorrelations.dnfEval line 57
  5. def OAI.TwoPointCorrelations.canonicalDNFTree line 60
  6. theorem OAI.TwoPointCorrelations.canonicalDNFTree_eval line 69