(3steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
At:
mod
minus
x:
, n:
. ((-x) mod n) = if (x mod n)=
0
0 else n-(x mod n) fi
By:
Auto
THEN
Inst
Thm*
a:
, n:
. a = (a
n)
n+(a mod n) & (a mod n) < n [x;n]
THEN
SplitOnConclITE
Generated subgoals:
1
1.
x:
2.
n:
3.
x = (x
n)
n+(x mod n) & (x mod n) < n
4.
(x mod n) = 0
((-x) mod n) = 0
1
step
 
2
1.
x:
2.
n:
3.
x = (x
n)
n+(x mod n) & (x mod n) < n
4.
(x mod n) = 0
((-x) mod n) = n-(x mod n)
1
step
About:
(3steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc