(19steps 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: iseg select 2 2
1. T : Type
2. T List
3. u : T
4. v : T List
5. l2:T List. v  l2  ||v||||l2|| & (i:. i<||v||  v[i] = l2[i])
6. T List
7. u1 : T
8. v1 : T List
9. [u / v]  v1
9. 
9. ||[u / v]||||v1|| & (i:. i<||[u / v]||  [u / v][i] = v1[i])
  [u / v]  [u1 / v1]
  
  ||[u / v]||||[u1 / v1]||
  & (i:. i<||[u / v]||  [u / v][i] = [u1 / v1][i])
By: (Reduce 0 THEN Analyze 0) THEN (Analyze 0)

Generated subgoals:

1 10. [u / v]  [u1 / v1]
  ||v||+1||v1||+1 & (i:. i<||v||+1  [u / v][i] = [u1 / v1][i])
5 steps
2 10. ||v||+1||v1||+1 & (i:. i<||v||+1  [u / v][i] = [u1 / v1][i])
  [u / v]  [u1 / v1]
4 steps
3 9. [u / v]  v1
9. 
9. ||[u / v]||||v1|| & (i:. i<||[u / v]||  [u / v][i] = v1[i])
10. [u / v]  v1  (||[u / v]||||v1||
10. & (i:. i<||[u / v]||  [u / v][i] = v1[i]))
11. ||v||+1||v1||+1
12. i : 
13. i<||v||+1
  i<||[u / v]||
1 step
4 9. [u / v]  v1
9. 
9. ||[u / v]||||v1|| & (i:. i<||[u / v]||  [u / v][i] = v1[i])
10. [u / v]  v1  (||[u / v]||||v1||
10. & (i:. i<||[u / v]||  [u / v][i] = v1[i]))
11. ||v||+1||v1||+1
12. i : 
13. i<||v||+1
  i<||[u1 / v1]||
1 step

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

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