(4steps total)
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
split
factor1
wf
1
1
1.
k
: {2...}
2.
g
: {2..
k
}
3.
x
: {2..
k
}
4.
x
x
<
k
5.
x
<
x
x
&
x
<
x
x
split_factor1(
g
;
x
)
{2..
k
}
By:
Def THEN New:
u
FunExtensionality
Generated subgoal:
1
6.
u
: {2..
k
}
if
u
=
x
g
(
x
)+
g
(
x
x
)+
g
(
x
x
) ;
u
=
x
x
0 else
g
(
u
) fi
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc