(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
  m:, P:(mProp).
  (i:m. Dec(P(i)))
  
  (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: Analyze 0 THEN NatInd 1

Generated subgoals:

1   P:(0Prop). 
  (i:0. Dec(P(i)))
  
  (n,k:, f:(n0), g:(k0).
  (increasing(f;n)
  (& increasing(g;k)
  (& (i:n. P(f(i)))
  (& (j:k. P(g(j)))
  (& (i:0. (j:n. i = f(j))  (j:k. i = g(j))))
1 step
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))))
  P:(mProp). 
  (i:m. Dec(P(i)))
  
  (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))))
33 steps

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

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