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 A6: 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;
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 A5, SCMFSA6A:69;
A8: dom (Macro ((intloc 2) := (intloc 0 ))) = {0 ,1} by SCMFSA7B:4;
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;
A11: (intloc 2) := (intloc 0 ) <> halt SCM+FSA by SCMFSA_2:42, SCMFSA_2:124;
thus P . 0 = Bubble-Sort-Algorithm . 0 by A1, Th63
.= (Directed (Macro ((intloc 2) := (intloc 0 )))) . 0 by A6, A9, SCMFSA8A:28
.= (intloc 2) := (intloc 0 ) by A11, 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 A6, A10, 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 SCMFSA7B:6;
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 ))) = (card (Macro ((intloc 2) := (intloc 0 )))) + (card (Macro ((intloc 3) := (intloc 0 )))) by SCMFSA6A:61
.= 2 + (card (Macro ((intloc 3) := (intloc 0 )))) by SCMFSA7B:6
.= 2 + 2 by SCMFSA7B:6
.= 4 ;
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 + (card (Macro ((intloc 5) := (intloc 0 )))) by A14, SCMFSA6A:61
.= 6 + 2 by SCMFSA7B:6 ;
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 + (card (Macro ((intloc 6) := (intloc 0 )))) by A15, SCMFSA6A:61
.= 8 + 2 by SCMFSA7B:6 ;
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