(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. 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:nP(f(i))
12. j:kP(g(j))
13. i:||L||. (j:ni = f(j))  (j:ki = g(j))
  L1,L2:T List, f1:(||L1||||L||), f2:(||L2||||L||).
  interleaving_occurence(T;L1;L2;L;f1;f2)
  & (i:||L1||. P(f1(i))) & (i:||L2||. P(f2(i)))
  & (i:||L||. 
  & ((P(i (j:||L1||. f1(j) = i)) & (P(i (j:||L2||. f2(j) = i)))


By: Inst
Thm* L:T List, n:f:(n||L||).
Thm* increasing(f;n)
Thm* 
Thm* (L1:T List. ||L1|| = n   & sublist_occurence(T;L1;L;f))
[T;L;n;f]
THEN
Inst
Thm* L:T List, n:f:(n||L||).
Thm* increasing(f;n)
Thm* 
Thm* (L1:T List. ||L1|| = n   & sublist_occurence(T;L1;L;f))
[T;L;k;g]
THEN
ExRepD


Generated subgoal:

1 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)
  L1,L2:T List, f1:(||L1||||L||), f2:(||L2||||L||).
  interleaving_occurence(T;L1;L2;L;f1;f2)
  & (i:||L1||. P(f1(i))) & (i:||L2||. P(f2(i)))
  & (i:||L||. 
  & ((P(i (j:||L1||. f1(j) = i)) & (P(i (j:||L2||. f2(j) = i)))

20 steps

About:
listdecidableintnatural_numberapplyfunctionuniverse
equalpropimpliesandorall
exists
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