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 ;
set q0 = bubble-sort (fsloc 0 );
let s be State of SCM+FSA ; :: thesis: ( Bubble-Sort-Algorithm c= s implies ( s . 0 = (intloc 2) := (intloc 0 ) & s . 1 = goto 2 & s . 2 = (intloc 3) := (intloc 0 ) & s . 3 = goto 4 & s . 4 = (intloc 4) := (intloc 0 ) & s . 5 = goto 6 & s . 6 = (intloc 5) := (intloc 0 ) & s . 7 = goto 8 & s . 8 = (intloc 6) := (intloc 0 ) & s . 9 = goto 10 & s . 10 = (intloc 1) :=len (fsloc 0 ) & s . 11 = goto 12 ) )
assume A1: Bubble-Sort-Algorithm c= s ; :: thesis: ( s . 0 = (intloc 2) := (intloc 0 ) & s . 1 = goto 2 & s . 2 = (intloc 3) := (intloc 0 ) & s . 3 = goto 4 & s . 4 = (intloc 4) := (intloc 0 ) & s . 5 = goto 6 & s . 6 = (intloc 5) := (intloc 0 ) & s . 7 = goto 8 & s . 8 = (intloc 6) := (intloc 0 ) & s . 9 = goto 10 & s . 10 = (intloc 1) :=len (fsloc 0 ) & s . 11 = goto 12 )

A2: now

let i be Element of NAT ; :: thesis: ( i < 63 implies (bubble-sort (fsloc 0 )) . i = s . i )
assume i < 63 ; :: thesis: (bubble-sort (fsloc 0 )) . i = s . i
then i in dom (bubble-sort (fsloc 0 )) by Th63;
hence (bubble-sort (fsloc 0 )) . i = s . i by A1, GRFUNC_1:8; :: thesis: verum

end;

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 (fsloc 0 ) = ((((((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 (fsloc 0 ) = (((((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 (fsloc 0 ) = ((((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 (fsloc 0 ) = (((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 (fsloc 0 ) = ((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 (fsloc 0 ) = ((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 s . 0 = (bubble-sort (fsloc 0 )) . 0 by A2
.= (Directed (Macro ((intloc 2) := (intloc 0 )))) . 0 by A6, A9, SCMFSA8A:28
.= (intloc 2) := (intloc 0 ) by A11, SCMFSA7B:7 ; :: thesis: ( s . 1 = goto 2 & s . 2 = (intloc 3) := (intloc 0 ) & s . 3 = goto 4 & s . 4 = (intloc 4) := (intloc 0 ) & s . 5 = goto 6 & s . 6 = (intloc 5) := (intloc 0 ) & s . 7 = goto 8 & s . 8 = (intloc 6) := (intloc 0 ) & s . 9 = goto 10 & s . 10 = (intloc 1) :=len (fsloc 0 ) & s . 11 = goto 12 )
thus s . 1 = (bubble-sort (fsloc 0 )) . 1 by A2
.= (Directed (Macro ((intloc 2) := (intloc 0 )))) . 1 by A6, A10, SCMFSA8A:28
.= goto 2 by SCMFSA7B:8 ; :: thesis: ( s . 2 = (intloc 3) := (intloc 0 ) & s . 3 = goto 4 & s . 4 = (intloc 4) := (intloc 0 ) & s . 5 = goto 6 & s . 6 = (intloc 5) := (intloc 0 ) & s . 7 = goto 8 & s . 8 = (intloc 6) := (intloc 0 ) & s . 9 = goto 10 & s . 10 = (intloc 1) :=len (fsloc 0 ) & s . 11 = goto 12 )
A12: card (Macro ((intloc 2) := (intloc 0 ))) = 2 by SCMFSA7B:6;
thus s . 2 = (bubble-sort (fsloc 0 )) . 2 by A2
.= (intloc 3) := (intloc 0 ) by A7, A12, Th51 ; :: thesis: ( s . 3 = goto 4 & s . 4 = (intloc 4) := (intloc 0 ) & s . 5 = goto 6 & s . 6 = (intloc 5) := (intloc 0 ) & s . 7 = goto 8 & s . 8 = (intloc 6) := (intloc 0 ) & s . 9 = goto 10 & s . 10 = (intloc 1) :=len (fsloc 0 ) & s . 11 = goto 12 )
thus s . 3 = (bubble-sort (fsloc 0 )) . (2 + 1) by A2
.= goto (2 + 2) by A7, A12, Th51
.= goto 4 ; :: thesis: ( s . 4 = (intloc 4) := (intloc 0 ) & s . 5 = goto 6 & s . 6 = (intloc 5) := (intloc 0 ) & s . 7 = goto 8 & s . 8 = (intloc 6) := (intloc 0 ) & s . 9 = goto 10 & s . 10 = (intloc 1) :=len (fsloc 0 ) & s . 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 s . 4 = (bubble-sort (fsloc 0 )) . 4 by A2
.= (intloc 4) := (intloc 0 ) by A5, A13, Th51 ; :: thesis: ( s . 5 = goto 6 & s . 6 = (intloc 5) := (intloc 0 ) & s . 7 = goto 8 & s . 8 = (intloc 6) := (intloc 0 ) & s . 9 = goto 10 & s . 10 = (intloc 1) :=len (fsloc 0 ) & s . 11 = goto 12 )
thus s . 5 = (bubble-sort (fsloc 0 )) . (4 + 1) by A2
.= goto (4 + 2) by A5, A13, Th51
.= goto 6 ; :: thesis: ( s . 6 = (intloc 5) := (intloc 0 ) & s . 7 = goto 8 & s . 8 = (intloc 6) := (intloc 0 ) & s . 9 = goto 10 & s . 10 = (intloc 1) :=len (fsloc 0 ) & s . 11 = goto 12 )
A14: card ((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) = 6 by Th45;
thus s . 6 = (bubble-sort (fsloc 0 )) . 6 by A2
.= (intloc 5) := (intloc 0 ) by A4, A14, Th51 ; :: thesis: ( s . 7 = goto 8 & s . 8 = (intloc 6) := (intloc 0 ) & s . 9 = goto 10 & s . 10 = (intloc 1) :=len (fsloc 0 ) & s . 11 = goto 12 )
thus s . 7 = (bubble-sort (fsloc 0 )) . (6 + 1) by A2
.= goto (6 + 2) by A4, A14, Th51
.= goto 8 ; :: thesis: ( s . 8 = (intloc 6) := (intloc 0 ) & s . 9 = goto 10 & s . 10 = (intloc 1) :=len (fsloc 0 ) & s . 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 s . 8 = (bubble-sort (fsloc 0 )) . 8 by A2
.= (intloc 6) := (intloc 0 ) by A3, A15, Th51 ; :: thesis: ( s . 9 = goto 10 & s . 10 = (intloc 1) :=len (fsloc 0 ) & s . 11 = goto 12 )
thus s . 9 = (bubble-sort (fsloc 0 )) . (8 + 1) by A2
.= goto (8 + 2) by A3, A15, Th51
.= goto 10 ; :: thesis: ( s . 10 = (intloc 1) :=len (fsloc 0 ) & s . 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 s . 10 = (bubble-sort (fsloc 0 )) . 10 by A2
.= (intloc 1) :=len (fsloc 0 ) by A16, Th52 ; :: thesis: s . 11 = goto 12
thus s . 11 = (bubble-sort (fsloc 0 )) . (10 + 1) by A2
.= goto (10 + 2) by A16, Th52
.= goto 12 ; :: thesis: verum