Nuprl - Proof: increasing split 2

(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. 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))))

P:(

m

Prop).

(

i:

m. Dec(P(i)))

(

n,k:

, f:(

n

m), g:(

k

m).

(increasing(f;n)

(& increasing(g;k)

(& (

i:

n. P(f(i)))

(& (

j:

k.

P(g(j)))

(& (

i:

m. (

j:

n. i = f(j))

(

j:

k. i = g(j))))

By:	RepeatFor 2 (ParallelOp -1)

Generated subgoals:

1 4. P : mProp
5. i:m. Dec(P(i))
  i:(m-1). Dec(P(i))
1 step

2 4. P : mProp
5. i:m. Dec(P(i))
6. n,k:, f:(n(m-1)), g:(k(m-1)).
6. increasing(f;n)
6. & increasing(g;k)
6. & (i:n. P(f(i)))
6. & (j:k. P(g(j)))
6. & (i:(m-1). (j:n. i = f(j))  (j:k. i = g(j)))
  n,k:, f:(nm), g:(km).
  increasing(f;n)
  & increasing(g;k)
  & (i:n. P(f(i)))
  & (j:k. P(g(j)))
  & (i:m. (j:n. i = f(j))  (j:k. i = g(j)))
31 steps

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