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 Instruction-Sequence of SCM+FSA; :: 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));
A2: 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:27;
then 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:27;
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:27;
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:27;
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:31;
then A5: 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 5;
A6: 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:27;
A7: dom (Macro ((intloc 2) := (intloc 0))) = {0,1} by COMPOS_1:61;
then A8: 0 in dom (Macro ((intloc 2) := (intloc 0))) by TARSKI:def 2;
A9: 1 in dom (Macro ((intloc 2) := (intloc 0))) by A7, TARSKI:def 2;
thus P . 0 = Bubble-Sort-Algorithm . 0 by A1, Th24
.= (Directed (Macro ((intloc 2) := (intloc 0)))) . 0 by A8, A5, SCMFSA8A:14
.= (intloc 2) := (intloc 0) by SCMFSA7B:1 ; :: 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, Th24
.= (Directed (Macro ((intloc 2) := (intloc 0)))) . 1 by A9, A5, SCMFSA8A:14
.= goto 2 by SCMFSA7B:2 ; :: 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 )
A10: card (Macro ((intloc 2) := (intloc 0))) = 2 by COMPOS_1:56;
thus P . 2 = Bubble-Sort-Algorithm . 2 by A1, Th24
.= (intloc 3) := (intloc 0) by A6, A10, Th17 ; :: 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, Th24
.= goto (2 + 2) by A6, A10, Th18
.= 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 )
A11: card (((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) = 4 by SCMFSA6A:35;
thus P . 4 = Bubble-Sort-Algorithm . 4 by A1, Th24
.= (intloc 4) := (intloc 0) by A4, A11, Th17 ; :: 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, Th24
.= goto (4 + 2) by A4, A11, Th18
.= 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 )
A12: card ((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0))) = 6 by Th15;
thus P . 6 = Bubble-Sort-Algorithm . 6 by A1, Th24
.= (intloc 5) := (intloc 0) by A3, A12, Th17 ; :: 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, Th24
.= goto (6 + 2) by A3, A12, Th18
.= goto 8 ; :: thesis: ( 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))) ";" ((intloc 4) := (intloc 0))) ";" ((intloc 5) := (intloc 0))) = 6 + 2 by A12, SCMFSA6A:34;
thus P . 8 = Bubble-Sort-Algorithm . 8 by A1, Th24
.= (intloc 6) := (intloc 0) by A2, A13, Th17 ; :: 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, Th24
.= goto (8 + 2) by A2, A13, Th18
.= goto 10 ; :: thesis: ( 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))) ";" ((intloc 5) := (intloc 0))) ";" ((intloc 6) := (intloc 0))) = 8 + 2 by A13, SCMFSA6A:34;
thus P . 10 = Bubble-Sort-Algorithm . 10 by A1, Th24
.= (intloc 1) :=len (fsloc 0) by A14, Th17 ; :: thesis: P . 11 = goto 12
thus P . 11 = Bubble-Sort-Algorithm . (10 + 1) by A1, Th24
.= goto (10 + 2) by A14, Th18
.= goto 12 ; :: thesis: verum