Nuprl - Definition Cascade for iter_via

Remark Remark WhoCites Definitions IteratedBinops Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Iteration of a binary operator over a finite sequence of values. Some special cases of this iteration operator include sum, product and exponentiation:

i:{a..b}. e(i) Iter(x,y. x+y;0) i:{a..b}. e(i)

i:b. e(i) Iter(x,y. x+y;0) i:{0..b}. e(i)

i:{a..b}. e(i) Iter(x,y. xy;1) i:{a..b}. e(i)

i:b. e(i) Iter(x,y. xy;1) i:{0..b}. e(i)

eb Iter(x,y. xy;1) :{0..b}. e

Or i:{a..b}. e(i) Iter(x,y. x y;False) i:{a..b}. e(i)

Or i:b. e(i) Iter(x,y. x y;False) i:{0..b}. e(i)

And i:{a..b}. e(i) Iter(x,y. x & y;True) i:{a..b}. e(i)

And i:b. e(i) Iter(x,y. x & y;True) i:{0..b}. e(i)

Who Cites iter via intseg?

iter_via_intseg Def  Iter(f;u) i:{a..b}. e(i)
Def  == if a<b f((Iter(f;u) i:{a..b-1}. e(i)),e(b-1)) else u fi
Def  (recursive)
Thm*  f:(AAA), u:A, a,b:, e:({a..b}A). (Iter(f;u) i:{a..b}. e(i))  A

lt_int Def  i<j == if i<j true ; false fi
Thm*  i,j:. (i<j)

Syntax: Iter(f;u) i:{a..b}. e(i) has structure: iter_via_intseg(f; u; i.e(i); a; b)

About:

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

Remark Remark WhoCites Definitions IteratedBinops Sections DiscrMathExt Doc

i:{a..b}. e(i)		Iter(x,y. x+y;0) i:{a..b}. e(i)
i:b. e(i)		Iter(x,y. x+y;0) i:{0..b}. e(i)
i:{a..b}. e(i)		Iter(x,y. xy;1) i:{a..b}. e(i)
i:b. e(i)		Iter(x,y. xy;1) i:{0..b}. e(i)
eb		Iter(x,y. xy;1) :{0..b}. e
Or i:{a..b}. e(i)		Iter(x,y. x y;False) i:{a..b}. e(i)
Or i:b. e(i)		Iter(x,y. x y;False) i:{0..b}. e(i)
And i:{a..b}. e(i)		Iter(x,y. x & y;True) i:{a..b}. e(i)
And i:b. e(i)		Iter(x,y. x & y;True) i:{0..b}. e(i)

	Who Cites iter via intseg?

iter_via_intseg	Def Iter(f;u) i:{a..b}. e(i) Def == if a<b f((Iter(f;u) i:{a..b-1}. e(i)),e(b-1)) else u fi Def (recursive)

	Thm* f:(AAA), u:A, a,b:, e:({a..b}A). (Iter(f;u) i:{a..b}. e(i)) A

lt_int	Def i<j == if i<j true ; false fi

	Thm* i,j:. (i<j)