law QG

lawful-fields@0.1.1.0 · proof_num.bend:113

import Base

113# M = 10 q + 6, from 2^32 - 1 = 10 q + 5 with every number abstract.
114law QG:
115  for +N1: Nat
116  for +Qn: Nat
117  for +R: Nat
118  for +T: Nat
119  for +Z: Nat
120  for +M: Nat
121  for +hdm: {Nat.add(Nat.mul(Nat.div(N1, T), T), Nat.mod(N1, T)) == N1 : Nat}
122  for +hd: {Nat.div(N1, T) == Qn : Nat}
123  for +hr: {Nat.mod(N1, T) == R : Nat}
124  for +hT: {T == 10n : Nat}
125  for +hR: {R == 5n : Nat}
126  for +hZ: {Z == 0n : Nat}
127  for +hN: {N1 == Nat.sub(Nat.sub(M, 1n), Z) : Nat}
128  for +hM: {Nat.is_lt(0n, M) == True{} : Bool}
129  {Nat.add(Nat.mul(Qn, 10n), 6n) == M : Nat}