(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 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))))
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)))
By: InstHyp [m-1] -2 THEN Analyze -1 THEN ExRepD

Generated subgoals:

1 6. n : 
7. k : 
8. f : n(m-1)
9. g : k(m-1)
10. increasing(f;n)
11. increasing(g;k)
12. i:n. P(f(i))
13. j:k. P(g(j))
14. i:(m-1). (j:n. i = f(j))  (j:k. i = g(j))
15. P(m-1)
  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)))
16 steps
2 6. n : 
7. k : 
8. f : n(m-1)
9. g : k(m-1)
10. increasing(f;n)
11. increasing(g;k)
12. i:n. P(f(i))
13. j:k. P(g(j))
14. i:(m-1). (j:n. i = f(j))  (j:k. i = g(j))
15. P(m-1)
  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)))
14 steps

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

(35steps total) PrintForm Definitions mb nat Sections MarkB generic Doc