(3steps total)
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
can
reduce
composite
factor2
1
1.
k
: {2...}
2.
g
: {2..
k
}
3.
x
,
y
:{2..
k
}.
3.
x
y
<
k
3.
3.
(
h
:({2..
k
}
).
3. (
{2..
k
}(
g
) =
{2..
k
}(
h
)
3. (
&
h
(
x
y
) = 0
3. (
& (
u
:{2..
k
}.
x
y
<
u
h
(
u
) =
g
(
u
)))
4.
z
: {2..
k
}
5.
prime(
z
)
g'
:({2..
k
}
).
{2..
k
}(
g
) =
{2..
k
}(
g'
) &
g'
(
z
) = 0 & (
u
:{2..
k
}.
z
<
u
g'
(
u
) =
g
(
u
))
By:
FwdThru:
Thm*
x
:
.
prime(
x
)
x
<2
(
i
,
j
:{2..
x
}.
x
=
i
j
) on [
prime(
z
) ]
THEN
Analyze-1 ...
THEN
ExistHD Hyp:-1
THEN
Inst: Hyp:3 Using:[
i
|
j
] ...a
Generated subgoal:
1
6.
i
: {2..
z
}
7.
j
: {2..
z
}
8.
z
=
i
j
9.
h
:({2..
k
}
).
9.
{2..
k
}(
g
) =
{2..
k
}(
h
) &
h
(
i
j
) = 0 & (
u
:{2..
k
}.
i
j
<
u
h
(
u
) =
g
(
u
))
g'
:({2..
k
}
).
{2..
k
}(
g
) =
{2..
k
}(
g'
) &
g'
(
z
) = 0 & (
u
:{2..
k
}.
z
<
u
g'
(
u
) =
g
(
u
))
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc