Nuprl - Proof: increasing split 2 1

(35steps total) PrintForm Definitions mb nat Sections MarkB generic Doc

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

1. m :

2. 0<m
3.

P:(

(m-1)

Prop).
3. (

i:

(m-1). Dec(P(i)))
3.

3. (

n,k:

, f:(

n

(m-1)), g:(

k

(m-1)).
3. (increasing(f;n)
3. (& increasing(g;k)
3. (& (

i:

n. P(f(i)))
3. (& (

j:

k.

P(g(j)))
3. (& (

i:

(m-1). (

j:

n. i = f(j))

(

j:

k. i = g(j))))
4. P :

m

Prop
5.

i:

m. Dec(P(i))

i:

(m-1). Dec(P(i))

By:	ParallelOp -1

Generated subgoals:

None

About:

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

(35steps total) PrintForm Definitions mb nat Sections MarkB generic Doc