Nuprl - Proof: mul via intseg split mid

(5steps 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: mul via intseg split mid

a,c,b:

, e:({a..b

}

).

a

c

c

b

(

i:{a..b

}. e(i)) = (

i:{a..c

}. e(i))

(

i:{c..b

}. e(i))

By:

Inst:
Thm*

f:(A

A

A), u:A.
Thm* is_ident(A; f; u)
Thm*

Thm* is_assoc_sep(A; f)
Thm*

Thm* (

a,c,b:

, e:({a..b

}

A).
Thm* (a

c
Thm* (

Thm* (c

b
Thm* (

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

}. e(i))
Thm* (=
Thm* (f((Iter(f;u) i:{a..c

}. e(i)),Iter(f;u) i:{c..b

}. e(i)))
Using:[

|

x,y. x

y | 1]
THEN
OnAllClauses Reduce

Generated subgoals:

1 is_ident(; (x,y. xy); 1)
2 steps

2 is_assoc_sep(; (x,y. xy))
2 steps

About:

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

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