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 . (insloc 0 ) = (intloc 2) := (intloc 0 ) & s . (insloc 1) = goto (insloc 2) & s . (insloc 2) = (intloc 3) := (intloc 0 ) & s . (insloc 3) = goto (insloc 4) & s . (insloc 4) = (intloc 4) := (intloc 0 ) & s . (insloc 5) = goto (insloc 6) & s . (insloc 6) = (intloc 5) := (intloc 0 ) & s . (insloc 7) = goto (insloc 8) & s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) ) )
assume A1: Bubble-Sort-Algorithm c= s ; :: thesis: ( s . (insloc 0 ) = (intloc 2) := (intloc 0 ) & s . (insloc 1) = goto (insloc 2) & s . (insloc 2) = (intloc 3) := (intloc 0 ) & s . (insloc 3) = goto (insloc 4) & s . (insloc 4) = (intloc 4) := (intloc 0 ) & s . (insloc 5) = goto (insloc 6) & s . (insloc 6) = (intloc 5) := (intloc 0 ) & s . (insloc 7) = goto (insloc 8) & s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )

A2: now

let i be Element of NAT ; :: thesis: ( i < 63 implies (bubble-sort (fsloc 0 )) . (insloc i) = s . (insloc i) )
assume i < 63 ; :: thesis: (bubble-sort (fsloc 0 )) . (insloc i) = s . (insloc i)
then insloc i in dom (bubble-sort (fsloc 0 )) by Th63;
hence (bubble-sort (fsloc 0 )) . (insloc i) = s . (insloc 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 B7: 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;
A8: 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;
dom (Macro ((intloc 2) := (intloc 0 ))) = {(insloc 0 ),(insloc 1)} by SCMFSA7B:4;
then A9: ( insloc 0 in dom (Macro ((intloc 2) := (intloc 0 ))) & insloc 1 in dom (Macro ((intloc 2) := (intloc 0 ))) ) by TARSKI:def 2;
A10: (intloc 2) := (intloc 0 ) <> halt SCM+FSA by SCMFSA_2:42, SCMFSA_2:124;
thus s . (insloc 0 ) = (bubble-sort (fsloc 0 )) . (insloc 0 ) by A2
.= (Directed (Macro ((intloc 2) := (intloc 0 )))) . (insloc 0 ) by B7, A9, SCMFSA8A:28
.= (intloc 2) := (intloc 0 ) by A10, SCMFSA7B:7 ; :: thesis: ( s . (insloc 1) = goto (insloc 2) & s . (insloc 2) = (intloc 3) := (intloc 0 ) & s . (insloc 3) = goto (insloc 4) & s . (insloc 4) = (intloc 4) := (intloc 0 ) & s . (insloc 5) = goto (insloc 6) & s . (insloc 6) = (intloc 5) := (intloc 0 ) & s . (insloc 7) = goto (insloc 8) & s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )
thus s . (insloc 1) = (bubble-sort (fsloc 0 )) . (insloc 1) by A2
.= (Directed (Macro ((intloc 2) := (intloc 0 )))) . (insloc 1) by B7, A9, SCMFSA8A:28
.= goto (insloc 2) by SCMFSA7B:8 ; :: thesis: ( s . (insloc 2) = (intloc 3) := (intloc 0 ) & s . (insloc 3) = goto (insloc 4) & s . (insloc 4) = (intloc 4) := (intloc 0 ) & s . (insloc 5) = goto (insloc 6) & s . (insloc 6) = (intloc 5) := (intloc 0 ) & s . (insloc 7) = goto (insloc 8) & s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )
A11: card (Macro ((intloc 2) := (intloc 0 ))) = 2 by SCMFSA7B:6;
thus s . (insloc 2) = (bubble-sort (fsloc 0 )) . (insloc 2) by A2
.= (intloc 3) := (intloc 0 ) by A8, A11, Th51 ; :: thesis: ( s . (insloc 3) = goto (insloc 4) & s . (insloc 4) = (intloc 4) := (intloc 0 ) & s . (insloc 5) = goto (insloc 6) & s . (insloc 6) = (intloc 5) := (intloc 0 ) & s . (insloc 7) = goto (insloc 8) & s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )
thus s . (insloc 3) = (bubble-sort (fsloc 0 )) . (insloc (2 + 1)) by A2
.= goto (insloc (2 + 2)) by A8, A11, Th51
.= goto (insloc 4) ; :: thesis: ( s . (insloc 4) = (intloc 4) := (intloc 0 ) & s . (insloc 5) = goto (insloc 6) & s . (insloc 6) = (intloc 5) := (intloc 0 ) & s . (insloc 7) = goto (insloc 8) & s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )
A12: 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 . (insloc 4) = (bubble-sort (fsloc 0 )) . (insloc 4) by A2
.= (intloc 4) := (intloc 0 ) by A5, A12, Th51 ; :: thesis: ( s . (insloc 5) = goto (insloc 6) & s . (insloc 6) = (intloc 5) := (intloc 0 ) & s . (insloc 7) = goto (insloc 8) & s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )
thus s . (insloc 5) = (bubble-sort (fsloc 0 )) . (insloc (4 + 1)) by A2
.= goto (insloc (4 + 2)) by A5, A12, Th51
.= goto (insloc 6) ; :: thesis: ( s . (insloc 6) = (intloc 5) := (intloc 0 ) & s . (insloc 7) = goto (insloc 8) & s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )
A13: card ((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) = 6 by Th45;
thus s . (insloc 6) = (bubble-sort (fsloc 0 )) . (insloc 6) by A2
.= (intloc 5) := (intloc 0 ) by A4, A13, Th51 ; :: thesis: ( s . (insloc 7) = goto (insloc 8) & s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )
thus s . (insloc 7) = (bubble-sort (fsloc 0 )) . (insloc (6 + 1)) by A2
.= goto (insloc (6 + 2)) by A4, A13, Th51
.= goto (insloc 8) ; :: thesis: ( s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )
A14: 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 A13, SCMFSA6A:61
.= 6 + 2 by SCMFSA7B:6 ;
thus s . (insloc 8) = (bubble-sort (fsloc 0 )) . (insloc 8) by A2
.= (intloc 6) := (intloc 0 ) by A3, A14, Th51 ; :: thesis: ( s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )
thus s . (insloc 9) = (bubble-sort (fsloc 0 )) . (insloc (8 + 1)) by A2
.= goto (insloc (8 + 2)) by A3, A14, Th51
.= goto (insloc 10) ; :: thesis: ( s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )
A15: 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 A14, SCMFSA6A:61
.= 8 + 2 by SCMFSA7B:6 ;
thus s . (insloc 10) = (bubble-sort (fsloc 0 )) . (insloc 10) by A2
.= (intloc 1) :=len (fsloc 0 ) by A15, Th52 ; :: thesis: s . (insloc 11) = goto (insloc 12)
thus s . (insloc 11) = (bubble-sort (fsloc 0 )) . (insloc (10 + 1)) by A2
.= goto (insloc (10 + 2)) by A15, Th52
.= goto (insloc 12) ; :: thesis: verum