PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
rect
enumer
1
3
1
1
1
1
1
1
1
1
1
1
1
1
2
2
1
1.
n:
2.
m:
3.
a3:
4.
0
a3
5.
a3 < n
6.
a4:
7.
0
a4
8.
a4 < m
9.
a5:
10.
0
a5
11.
a5 < n
12.
a6:
13.
0
a6
14.
a6 < m
15.
a3
m+a4 = a5
m+a6
(n
m)
16.
(a4 rem m) = a4
|a6| < |m|
By:
Unfold `absval` 0
Generated subgoal:
1
if 0
a6
a6 else -a6 fi < if 0
m
m else -m fi
About:
if 0
a6
a6 else -a6 fi < if 0m m else -m fi
a3a4a5a6
m+a4 = a5m+a6 
(nm) |a6| < |m| if 0a6 a6 else -a6 fi < if 0m m else -m fi
