set f0 = fsloc 0;
set TT = Times ((intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len (fsloc 0))) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := ((fsloc 0),(intloc 3)))) ';' ((intloc 6) := ((fsloc 0),(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := ((fsloc 0),(intloc 4))) ';' (((fsloc 0),(intloc 3)) := (intloc 6))) ';' (((fsloc 0),(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))))));
set q = Bubble-Sort-Algorithm ;
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( Bubble-Sort-Algorithm c= P implies ( P . 0 = (intloc 2) := (intloc 0) & P . 1 = goto 2 & P . 2 = (intloc 3) := (intloc 0) & P . 3 = goto 4 & P . 4 = (intloc 4) := (intloc 0) & P . 5 = goto 6 & P . 6 = (intloc 5) := (intloc 0) & P . 7 = goto 8 & P . 8 = (intloc 6) := (intloc 0) & P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 ) )
assume A1: Bubble-Sort-Algorithm c= P ; :: thesis: ( P . 0 = (intloc 2) := (intloc 0) & P . 1 = goto 2 & P . 2 = (intloc 3) := (intloc 0) & P . 3 = goto 4 & P . 4 = (intloc 4) := (intloc 0) & P . 5 = goto 6 & P . 6 = (intloc 5) := (intloc 0) & P . 7 = goto 8 & P . 8 = (intloc 6) := (intloc 0) & P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 )
set W2 = (intloc 2) := (intloc 0);
set W3 = (intloc 3) := (intloc 0);
set W4 = (intloc 4) := (intloc 0);
set W5 = (intloc 5) := (intloc 0);
set W6 = (intloc 6) := (intloc 0);
set W7 = (intloc 1) :=len (fsloc 0);
set T7 = ((intloc 1) :=len (fsloc 0)) ';' (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len (fsloc 0))) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := ((fsloc 0),(intloc 3)))) ';' ((intloc 6) := ((fsloc 0),(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := ((fsloc 0),(intloc 4))) ';' (((fsloc 0),(intloc 3)) := (intloc 6))) ';' (((fsloc 0),(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))))))));
set T6 = ((intloc 6) := (intloc 0)) ';' (((intloc 1) :=len (fsloc 0)) ';' (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len (fsloc 0))) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := ((fsloc 0),(intloc 3)))) ';' ((intloc 6) := ((fsloc 0),(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := ((fsloc 0),(intloc 4))) ';' (((fsloc 0),(intloc 3)) := (intloc 6))) ';' (((fsloc 0),(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))))))));
set T5 = ((intloc 5) := (intloc 0)) ';' (((intloc 6) := (intloc 0)) ';' (((intloc 1) :=len (fsloc 0)) ';' (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len (fsloc 0))) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := ((fsloc 0),(intloc 3)))) ';' ((intloc 6) := ((fsloc 0),(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := ((fsloc 0),(intloc 4))) ';' (((fsloc 0),(intloc 3)) := (intloc 6))) ';' (((fsloc 0),(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))))))))));
set T4 = ((intloc 4) := (intloc 0)) ';' (((intloc 5) := (intloc 0)) ';' (((intloc 6) := (intloc 0)) ';' (((intloc 1) :=len (fsloc 0)) ';' (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len (fsloc 0))) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := ((fsloc 0),(intloc 3)))) ';' ((intloc 6) := ((fsloc 0),(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := ((fsloc 0),(intloc 4))) ';' (((fsloc 0),(intloc 3)) := (intloc 6))) ';' (((fsloc 0),(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))))))))));
set T3 = ((intloc 3) := (intloc 0)) ';' (((intloc 4) := (intloc 0)) ';' (((intloc 5) := (intloc 0)) ';' (((intloc 6) := (intloc 0)) ';' (((intloc 1) :=len (fsloc 0)) ';' (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len (fsloc 0))) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := ((fsloc 0),(intloc 3)))) ';' ((intloc 6) := ((fsloc 0),(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := ((fsloc 0),(intloc 4))) ';' (((fsloc 0),(intloc 3)) := (intloc 6))) ';' (((fsloc 0),(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))))))))))));
set X3 = ((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0));
set X4 = (((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0));
set X5 = ((((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0))) ';' ((intloc 5) := (intloc 0));
set X6 = (((((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0))) ';' ((intloc 5) := (intloc 0))) ';' ((intloc 6) := (intloc 0));
A3: Bubble-Sort-Algorithm = ((((((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0))) ';' ((intloc 5) := (intloc 0))) ';' ((intloc 6) := (intloc 0))) ';' (((intloc 1) :=len (fsloc 0)) ';' (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len (fsloc 0))) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := ((fsloc 0),(intloc 3)))) ';' ((intloc 6) := ((fsloc 0),(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := ((fsloc 0),(intloc 4))) ';' (((fsloc 0),(intloc 3)) := (intloc 6))) ';' (((fsloc 0),(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))))))))) by SCMFSA6A:69;
then A4: Bubble-Sort-Algorithm = (((((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0))) ';' ((intloc 5) := (intloc 0))) ';' (((intloc 6) := (intloc 0)) ';' (((intloc 1) :=len (fsloc 0)) ';' (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len (fsloc 0))) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := ((fsloc 0),(intloc 3)))) ';' ((intloc 6) := ((fsloc 0),(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := ((fsloc 0),(intloc 4))) ';' (((fsloc 0),(intloc 3)) := (intloc 6))) ';' (((fsloc 0),(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))))))))) by SCMFSA6A:69;
then A5: Bubble-Sort-Algorithm = ((((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0))) ';' (((intloc 5) := (intloc 0)) ';' (((intloc 6) := (intloc 0)) ';' (((intloc 1) :=len (fsloc 0)) ';' (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len (fsloc 0))) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := ((fsloc 0),(intloc 3)))) ';' ((intloc 6) := ((fsloc 0),(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := ((fsloc 0),(intloc 4))) ';' (((fsloc 0),(intloc 3)) := (intloc 6))) ';' (((fsloc 0),(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))))))))))) by SCMFSA6A:69;
then Bubble-Sort-Algorithm = (((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' (((intloc 4) := (intloc 0)) ';' (((intloc 5) := (intloc 0)) ';' (((intloc 6) := (intloc 0)) ';' (((intloc 1) :=len (fsloc 0)) ';' (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len (fsloc 0))) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := ((fsloc 0),(intloc 3)))) ';' ((intloc 6) := ((fsloc 0),(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := ((fsloc 0),(intloc 4))) ';' (((fsloc 0),(intloc 3)) := (intloc 6))) ';' (((fsloc 0),(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))))))))))) by SCMFSA6A:69;
then Bubble-Sort-Algorithm = ((intloc 2) := (intloc 0)) ';' (((intloc 3) := (intloc 0)) ';' (((intloc 4) := (intloc 0)) ';' (((intloc 5) := (intloc 0)) ';' (((intloc 6) := (intloc 0)) ';' (((intloc 1) :=len (fsloc 0)) ';' (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len (fsloc 0))) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := ((fsloc 0),(intloc 3)))) ';' ((intloc 6) := ((fsloc 0),(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := ((fsloc 0),(intloc 4))) ';' (((fsloc 0),(intloc 3)) := (intloc 6))) ';' (((fsloc 0),(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))))))))))))) by SCMFSA6A:73;
then XX: Bubble-Sort-Algorithm = (Macro ((intloc 2) := (intloc 0))) ';' (((intloc 3) := (intloc 0)) ';' (((intloc 4) := (intloc 0)) ';' (((intloc 5) := (intloc 0)) ';' (((intloc 6) := (intloc 0)) ';' (((intloc 1) :=len (fsloc 0)) ';' (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len (fsloc 0))) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := ((fsloc 0),(intloc 3)))) ';' ((intloc 6) := ((fsloc 0),(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := ((fsloc 0),(intloc 4))) ';' (((fsloc 0),(intloc 3)) := (intloc 6))) ';' (((fsloc 0),(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))))))))))))) by SCMFSA6A:def 6;
A7: Bubble-Sort-Algorithm = ((Macro ((intloc 2) := (intloc 0))) ';' ((intloc 3) := (intloc 0))) ';' (((intloc 4) := (intloc 0)) ';' (((intloc 5) := (intloc 0)) ';' (((intloc 6) := (intloc 0)) ';' (((intloc 1) :=len (fsloc 0)) ';' (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len (fsloc 0))) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := ((fsloc 0),(intloc 3)))) ';' ((intloc 6) := ((fsloc 0),(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := ((fsloc 0),(intloc 4))) ';' (((fsloc 0),(intloc 3)) := (intloc 6))) ';' (((fsloc 0),(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))))))))))) by XX, SCMFSA6A:69;
A8: dom (Macro ((intloc 2) := (intloc 0))) = {0,1} by COMPOS_1:149;
then A9: 0 in dom (Macro ((intloc 2) := (intloc 0))) by TARSKI:def 2;
A10: 1 in dom (Macro ((intloc 2) := (intloc 0))) by A8, TARSKI:def 2;
thus P . 0 = Bubble-Sort-Algorithm . 0 by A1, Th63
.= (Directed (Macro ((intloc 2) := (intloc 0)))) . 0 by A9, XX, SCMFSA8A:28
.= (intloc 2) := (intloc 0) by SCMFSA7B:7 ; :: thesis: ( P . 1 = goto 2 & P . 2 = (intloc 3) := (intloc 0) & P . 3 = goto 4 & P . 4 = (intloc 4) := (intloc 0) & P . 5 = goto 6 & P . 6 = (intloc 5) := (intloc 0) & P . 7 = goto 8 & P . 8 = (intloc 6) := (intloc 0) & P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 )
thus P . 1 = Bubble-Sort-Algorithm . 1 by A1, Th63
.= (Directed (Macro ((intloc 2) := (intloc 0)))) . 1 by A10, XX, SCMFSA8A:28
.= goto 2 by SCMFSA7B:8 ; :: thesis: ( P . 2 = (intloc 3) := (intloc 0) & P . 3 = goto 4 & P . 4 = (intloc 4) := (intloc 0) & P . 5 = goto 6 & P . 6 = (intloc 5) := (intloc 0) & P . 7 = goto 8 & P . 8 = (intloc 6) := (intloc 0) & P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 )
A12: card (Macro ((intloc 2) := (intloc 0))) = 2 by COMPOS_1:150;
thus P . 2 = Bubble-Sort-Algorithm . 2 by A1, Th63
.= (intloc 3) := (intloc 0) by A7, A12, Th51 ; :: thesis: ( P . 3 = goto 4 & P . 4 = (intloc 4) := (intloc 0) & P . 5 = goto 6 & P . 6 = (intloc 5) := (intloc 0) & P . 7 = goto 8 & P . 8 = (intloc 6) := (intloc 0) & P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 )
thus P . 3 = Bubble-Sort-Algorithm . (2 + 1) by A1, Th63
.= goto (2 + 2) by A7, A12, Th51
.= goto 4 ; :: thesis: ( P . 4 = (intloc 4) := (intloc 0) & P . 5 = goto 6 & P . 6 = (intloc 5) := (intloc 0) & P . 7 = goto 8 & P . 8 = (intloc 6) := (intloc 0) & P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 )
A13: card (((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) = 4 by SCMFSA6A:77;
thus P . 4 = Bubble-Sort-Algorithm . 4 by A1, Th63
.= (intloc 4) := (intloc 0) by A5, A13, Th51 ; :: thesis: ( P . 5 = goto 6 & P . 6 = (intloc 5) := (intloc 0) & P . 7 = goto 8 & P . 8 = (intloc 6) := (intloc 0) & P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 )
thus P . 5 = Bubble-Sort-Algorithm . (4 + 1) by A1, Th63
.= goto (4 + 2) by A5, A13, Th51
.= goto 6 ; :: thesis: ( P . 6 = (intloc 5) := (intloc 0) & P . 7 = goto 8 & P . 8 = (intloc 6) := (intloc 0) & P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 )
A14: card ((((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0))) = 6 by Th45;
thus P . 6 = Bubble-Sort-Algorithm . 6 by A1, Th63
.= (intloc 5) := (intloc 0) by A4, A14, Th51 ; :: thesis: ( P . 7 = goto 8 & P . 8 = (intloc 6) := (intloc 0) & P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 )
thus P . 7 = Bubble-Sort-Algorithm . (6 + 1) by A1, Th63
.= goto (6 + 2) by A4, A14, Th51
.= goto 8 ; :: thesis: ( P . 8 = (intloc 6) := (intloc 0) & P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 )
A15: card (((((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0))) ';' ((intloc 5) := (intloc 0))) = 6 + 2 by A14, SCMFSA6A:76;
thus P . 8 = Bubble-Sort-Algorithm . 8 by A1, Th63
.= (intloc 6) := (intloc 0) by A3, A15, Th51 ; :: thesis: ( P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 )
thus P . 9 = Bubble-Sort-Algorithm . (8 + 1) by A1, Th63
.= goto (8 + 2) by A3, A15, Th51
.= goto 10 ; :: thesis: ( P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 )
A16: card ((((((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0))) ';' ((intloc 5) := (intloc 0))) ';' ((intloc 6) := (intloc 0))) = 8 + 2 by A15, SCMFSA6A:76;
thus P . 10 = Bubble-Sort-Algorithm . 10 by A1, Th63
.= (intloc 1) :=len (fsloc 0) by A16, Th52 ; :: thesis: P . 11 = goto 12
thus P . 11 = Bubble-Sort-Algorithm . (10 + 1) by A1, Th63
.= goto (10 + 2) by A16, Th52
.= goto 12 ; :: thesis: verum