PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
eval
factorization
intseg
null
a
,
b
:
,
f
:({
a
..
b
}
).
b
a
{
a
..
b
}(
f
) = 1
By:
Def of
{
a
..
b
}(
f
)
THEN
Rewrite by
Thm*
f
:(
A
A
A
),
u
:
A
,
a
,
b
:
,
e
:({
a
..
b
}
A
).
Thm*
b
a
(Iter(
f
;
u
)
i
:{
a
..
b
}.
e
(
i
)) =
u
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc
a,b:
, f:({a..b
}
). b
a 
{a..b}(f) = 1 a,b:, f:({a..b}). ba {a..b}(f) = 1{a..b}(f)
f:(AAA), u:A, a,b:, e:({a..b}A).
a (Iter(f;u) i:{a..b}. e(i)) = u
