Nuprl - Proof: can reduce composite factor 1 1 2 1 1

(12steps 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 factor 1 1 2 1 1

1. k : {2...}
2. g : {2..k

}

3. x : {2..k

}
4. y : {2..k

}
5. x

y
6. x

y<k
7. y<x

y
8.

x<y

{2..k

}(g) =

{2..k

}(split_factor1(g; x))

& split_factor1(g; x)(x

x) = 0

& (

u:{2..k

}. x

x<u

split_factor1(g; x)(u) = g(u))

By:	Guarding (<prop> & <prop>) BackThru: Thm* k:{2...}, g:({2..k}), x:{2..k}. Thm* xx<k Thm* Thm* {2..k}(g) = {2..k}(split_factor1(g; x)) Thm* & split_factor1(g; x)(xx) = 0 Thm* & (u:{2..k}. xx<u split_factor1(g; x)(u) = g(u))

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(12steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc