Nuprl - Proof: split factor2 char a 1 1

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: split factor2 char a 1 1

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

}

3. x : {2..k

}
4. y : {2..k

}
5. x

y<k
6. x<y
7. x<x

y
8. y<x

y

{2..k

}(g) =

{2..k

}(split_factor2(g; x; y))

By:

Let (h = split_factor2(g; x; y)) ...w

THEN
((h(x

y) = 0

((& h(x) = g(x)+g(x

y)

((& h(y) = g(y)+g(x

y)

((& (

u:{2..k

}.

u = x

u = y

u = x

y

h(u) = g(u)

)
((& By (Rewrite by h = split_factor2(g; x; y)

{2..k

}

...w

((& By (THEN
((& By (Def of split_factor2(g; x; y)
((& By (THEN
((& By (Reduce Concl ...

THEN SplitOnConclITEs ...

))
(THEN
(Auto

)

Generated subgoal:

1 9. h : {2..k}
10. h = split_factor2(g; x; y)
11. h(xy) = 0
12. h(x) = g(x)+g(xy)
13. h(y) = g(y)+g(xy)
14. u:{2..k}. u = x  u = y  u = xy  h(u) = g(u)
  {2..k}(g) = {2..k}(h)
PREMISE

About:

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

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