OAI/Combinatorics/EditApproximation/Geometry/CommonArrayTrace.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A finite array of fresh pass draws is equivalent to the sequential common-source trace. The conversion has exactly the nested product law.

  1. def OAI.EditApproximation.commonArrayToTrace line 15
  2. def OAI.EditApproximation.commonTraceToArray line 19
  3. theorem OAI.EditApproximation.commonTraceToArray_toTrace line 25
  4. theorem OAI.EditApproximation.commonArrayToTrace_toArray line 42
  5. theorem OAI.EditApproximation.commonArrayToTrace_atom line 61
  6. theorem OAI.EditApproximation.commonArrayToTrace_law line 75