(2steps total)
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
one
exponentiation
x
:
. 1
x
= 1
By:
Rewrite by
Thm*
f
:(
A
A
A
),
u
:
A
.
Thm*
is_ident(
A
;
f
;
u
)
Thm*
Thm*
(
a
,
b
:
,
e
:({
a
..
b
}
A
).
Thm* (
(
i
:{
a
..
b
}.
e
(
i
) =
u
)
(Iter(
f
;
u
)
i
:{
a
..
b
}.
e
(
i
)) =
u
)
Generated subgoal:
1
1.
is_ident(
; (
x
,
y
.
x
y
); 1)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
x:
. 1
x = 1 x:. 1x = 1f:(A
AA), u:A.
a,b:, e:({a..b
}A).
i:{a..b}. e(i) = u) (Iter(f;u) i:{a..b}. e(i)) = u)
is_ident(; (
x,y. x
y); 1)
