(41steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: append overlapping sublists 1 2 2 1
1. T : Type
2. L1 : T List
3. L2 : T List
4. L : T List
5. x : T
6. i,j:. i<||L||  j<||L||  i = j  L[i] = L[j]
7. f1 : ||L1 @ [x]||||L||
8. increasing(f1;||L1 @ [x]||)
9. j:||L1 @ [x]||. (L1 @ [x])[j] = L[(f1(j))]
10. f : (||L2||+1)||L||
11. increasing(f;||L2||+1)
12. j:(||L2||+1). [x / L2][j] = L[(f(j))]
13. ||L1 @ [x / L2]|| = ||L1||+||L2||+1
14. ||nil||0
  increasing(i.if i||L1|| f1(i) else f(i-||L1||) fi;||L1 @ [x / L2]||)
By: Unfold `increasing` 0 THEN Reduce 0 THEN SplitOnConclITE THEN SplitOnConclITE

Generated subgoals:

1 15. i : (||L1 @ [x / L2]||-1)
16. i||L1||
17. i+1||L1||
  f1(i)<f1(i+1)
1 step
2 15. i : (||L1 @ [x / L2]||-1)
16. i||L1||
17. ||L1||<i+1
  f1(i)<f(i+1-||L1||)
19 steps
3 15. i : (||L1 @ [x / L2]||-1)
16. ||L1||<i
17. ||L1||<i+1
  f(i-||L1||)<f(i+1-||L1||)
1 step

About:
listconsconsnilifthenelseintnatural_numberadd
subtractless_thanlambdaapplyfunctionuniverseequalimpliesall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(41steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc