Nuprl - Proof: iter via intseg wf 1

(13steps total) PrintForm Definitions IteratedBinops Sections DiscrMathExt Search Doc

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: iter via intseg wf 1

1. A : Type
2. f : A

A
3. u : A
4. a :

, e:({a..b

}

A). (Iter(f;u) i:{a..b

}. e(i))

By:	n:, b:. bn+a (e:({a..b}A). (Iter(f;u) i:{a..b}. e(i)) A) Asserted

Generated subgoals:

1   n:, b:. bn+a  (e:({a..b}A). (Iter(f;u) i:{a..b}. e(i))  A)
5 steps

2 5. n:, b:. bn+a  (e:({a..b}A). (Iter(f;u) i:{a..b}. e(i))  A)
  b:, e:({a..b}A). (Iter(f;u) i:{a..b}. e(i))  A
6 steps

About:

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

(13steps total) PrintForm Definitions IteratedBinops Sections DiscrMathExt Search Doc

1	n:, b:. bn+a (e:({a..b}A). (Iter(f;u) i:{a..b}. e(i)) A)	5 steps
2	5. n:, b:. bn+a (e:({a..b}A). (Iter(f;u) i:{a..b}. e(i)) A) b:, e:({a..b}A). (Iter(f;u) i:{a..b}. e(i)) A	6 steps