(10steps total)
PrintForm
Definitions
Lemmas
num
thy
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
decidable
divides
1
2
1.
a
:
2.
b
:
3.
a
= 0
Dec(
a
|
b
)
By:
Using [`
A
',((
b
rem
a
) = 0)] (BackThru
Thm*
Dec(
A
)
(
A
B
)
Dec(
B
))
Generated subgoals:
1
Dec((
b
rem
a
) = 0)
1
step
2
(
b
rem
a
) = 0
a
|
b
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(10steps total)
PrintForm
Definitions
Lemmas
num
thy
1
Sections
StandardLIB
Doc
a = 0
Dec(a | b)
a = 0
Dec(a | b)
(A 
B) Dec(B)) Dec((b rem a) = 0)
(b rem a) = 0 a | b
