Nuprl - Proof: can reduce composite factor 1 1 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 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_factor2(g; x; y))

& split_factor2(g; x; y)(x

y) = 0

& (

u:{2..k

}. x

y<u

split_factor2(g; x; y)(u) = g(u))

By:	Guarding (<prop> & <prop>) BackThru: Thm* k:{2...}, g:({2..k}), x,y:{2..k}. Thm* xy<k Thm* Thm* x<y Thm* Thm* {2..k}(g) = {2..k}(split_factor2(g; x; y)) Thm* & split_factor2(g; x; y)(xy) = 0 Thm* & (u:{2..k}. xy<u split_factor2(g; x; y)(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