PrintForm Definitions mb nat Sections MarkB generic Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sum-ite

  k:f,g:(k), p:(k).
  sum(if p(i) f(i)+g(i) else f(i) fi | i < k)
  =
  sum(f(i) | i < k)+sum(if p(i) g(i) else 0 fi | i < k)


By: SumInd


Generated subgoals:

None

About:
boolifthenelseintnatural_numberaddfunctionequalall
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions mb nat Sections MarkB generic Search Doc