Nuprl - Proof: split factor2 char a 1 2

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

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

split_factor2(g; x; y)(x

y) = 0

& (

u:{2..k

}. x

y<u

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

By:	Auto THEN Def of split_factor2(<term>; <term>; <term>) THEN Reduce Concl THEN SplitOnConclITEs ...

Generated subgoals:

None

About:

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