OAI/Combinatorics/ContingencyTables/Machines/ListSubtractProgram.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Binary subtraction at one list coordinate

The scan depends on the stored list length. The subtracted amount remains binary throughout and never controls a loop.

  1. abbrev OAI.ContingencyTables.ListSubtractProgram.Input line 16
  2. abbrev OAI.ContingencyTables.ListSubtractProgram.Cell line 17
  3. def OAI.ContingencyTables.ListSubtractProgram.entry line 19
  4. def OAI.ContingencyTables.ListSubtractProgram.entryRealizer line 22
  5. lemma OAI.ContingencyTables.ListSubtractProgram.polynomial_entry line 32
  6. def OAI.ContingencyTables.ListSubtractProgram.indices line 46
  7. def OAI.ContingencyTables.ListSubtractProgram.indicesRealizer line 48
  8. lemma OAI.ContingencyTables.ListSubtractProgram.polynomial_indices line 51
  9. def OAI.ContingencyTables.ListSubtractProgram.subtractAt line 59
  10. def OAI.ContingencyTables.ListSubtractProgram.subtractAtRealizer line 62
  11. lemma OAI.ContingencyTables.ListSubtractProgram.polynomial_subtractAt line 65
  12. lemma OAI.ContingencyTables.ListSubtractProgram.subtractAt_length line 69
  13. lemma OAI.ContingencyTables.ListSubtractProgram.subtractAt_ofFn line 73