(70steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc

At: adjm to adjl graph 1 2 2 2 1 1 1 1
1. size:
2. m1: sizesize
3. b: sizesize
4. m1(1of(b),2of(b))
(2of(b) upto(0;size))
By: AssertBY (2of(b) upto(0;size)) (RWO Thm* i,j,k:. (k upto(i;j)) ik & k < j 0)
Generated subgoal:

15. (2of(b) upto(0;size))
(2of(b) upto(0;size))		1 step

About:
productboolassertnatural_numberless_thanapplyfunctionandall

(70steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc