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

At: adjm to adjl graph 1 2 2 1 1 1 1 1 2 2
1. size:
2. m1: sizesize
3. x: size
4. a2: ||filter(j.m1(x,j);upto(0;size))||
5. x1: size
6. a3: ||filter(j.m1(x1,j);upto(0;size))||
7. m1(x,filter(j.m1(x,j);upto(0;size))[a2])
8. x = x1
9. filter(j.m1(x,j);upto(0;size))[a2] = filter(j.m1(x1,j);upto(0;size))[a3]
10. no_repeats(size;filter(j.m1(x,j);upto(0;size)))
11. a2 = a3 ||filter(j.m1(x,j);upto(0;size))||
a2 = a3 ||filter(j.m1(x,j);upto(0;size))||
By:
Unfold `no_repeats` -2
THEN
InstHyp [a2;a3] -2
Generated subgoals:

110. i,j:. i < ||filter(j.m1(x,j);upto(0;size))|| j < ||filter(j.m1(x,j);upto(0;size))|| i = j filter(j.m1(x,j);upto(0;size))[i] = filter(j.m1(x,j);upto(0;size))[j]
11. a2 = a3 ||filter(j.m1(x,j);upto(0;size))||
a3 < ||filter(j.m1(x,j);upto(0;size))||		1 step
 
210. i,j:. i < ||filter(j.m1(x,j);upto(0;size))|| j < ||filter(j.m1(x,j);upto(0;size))|| i = j filter(j.m1(x,j);upto(0;size))[i] = filter(j.m1(x,j);upto(0;size))[j]
11. a2 = a3 ||filter(j.m1(x,j);upto(0;size))||
a2 = a3 		1 step
 
310. i,j:. i < ||filter(j.m1(x,j);upto(0;size))|| j < ||filter(j.m1(x,j);upto(0;size))|| i = j filter(j.m1(x,j);upto(0;size))[i] = filter(j.m1(x,j);upto(0;size))[j]
11. a2 = a3 ||filter(j.m1(x,j);upto(0;size))||
12. filter(j.m1(x,j);upto(0;size))[a2] = filter(j.m1(x,j);upto(0;size))[a3]
a2 = a3 ||filter(j.m1(x,j);upto(0;size))||		2 steps

About:
boolassertnatural_numberless_thanlambdaapplyfunctionequal

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