Nuprl - Proof: interleaving split 1 1 2 2 1

(22steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc

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

1. T : Type
2. L : T List
3. P :

||L||

Prop
4.

x:

||L||. Dec(P(x))
5. n :

6. k :

7. f :

n

||L||
8. g :

k

||L||
9. increasing(f;n)
10. increasing(g;k)
11.

i:

n. P(f(i))
12.

j:

k.

P(g(j))
13.

i:

||L||. (

j:

n. i = f(j))

(

j:

k. i = g(j))
14. L2 : T List
15. ||L2|| = n
16. sublist_occurence(T;L2;L;f)
17. L1 : T List
18. ||L1|| = k
19. sublist_occurence(T;L1;L;g)
20. ||L|| = ||L2||+||L1||
21. increasing(f;||L2||)
22.

j:

||L2||. L2[j] = L[(f(j))]
23. increasing(g;||L1||)
24.

j:

||L1||. L1[j] = L[(g(j))]
25.

j1:

||L2||, j2:

||L1||.

f(j1) = g(j2)
26. i :

||L||
27.

P(i)

j:

||L1||. g(j) = i

By:	AllHyps (j.InstHyp [i] j THENA Complete Auto) THEN Analyze -2

Generated subgoals:

1 28. j:n. i = f(j)
29. Dec(P(i))
j:||L1||. g(j) = i
2 steps

2 28. j:k. i = g(j)
29. Dec(P(i))
j:||L1||. g(j) = i
1 step

About:

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

(22steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc