(17steps total) PrintForm Definitions Lemmas IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Splitting the range of iteration.

At: iter via intseg split mid


  A:Type, f:(AAA), u:A.
  is_ident(Afu)
  
  is_assoc_sep(Af)
  
  (a,c,b:e:({a..b}A).
  (ac
  (
  (cb
  (
  ((Iter(f;ui:{a..b}. e(i))
  (=
  (f((Iter(f;ui:{a..c}. e(i)),Iter(f;ui:{c..b}. e(i)))


By: Guarding (b:<type>. <prop>) Auto


Generated subgoal:

1 1. A : Type
2. f : AAA
3. u : A
4. is_ident(Afu)
5. is_assoc_sep(Af)
6. a : 
7. c : 
  b:e:({a..b}A).
  ac
  
  cb
  
  (Iter(f;ui:{a..b}. e(i))
  =
  f((Iter(f;ui:{a..c}. e(i)),Iter(f;ui:{c..b}. e(i))

16 steps

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

(17steps total) PrintForm Definitions Lemmas IteratedBinops Sections DiscrMathExt Doc