(2steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
compose
iter
sum
comp
A
:Type,
f
:(
A
A
),
i
,
j
,
k
:
.
k
=
i
+
j
f
{
i
} o
f
{
j
} =
f
{
k
}
By:
Def of <fun> o <fun> THEN FunExtensionality
Generated subgoal:
1
1.
A
: Type
2.
f
:
A
A
3.
i
:
4.
j
:
5.
k
:
6.
k
=
i
+
j
7.
x
:
A
f
{
i
}(
f
{
j
}(
x
)) =
f
{
k
}(
x
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
A:Type, f:(A
A), i,j,k:
. k = i+j 
f{
i} o f{j} = f{k} A:Type, f:(AA), i,j,k:. k = i+j f{i} o f{j} = f{k}A
f{i}(f{j}(x)) = f{k}(x)
