:: Bubble Sort on SCM+FSA
:: by JingChao Chen and Yatsuka Nakamura
::
:: Received June 17, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


begin

set SA0 = Start-At (0,SCM+FSA);

theorem Th1: :: SCMBSORT:1
for I being Program of
for a, b being Int-Location st not I destroys b &amp; a <> b holds
not Times (a,I) destroys b
proofend;

theorem Th2: :: SCMBSORT:2
for s being State of SCM+FSA
for f being FinSeq-Location
for a, b being Int-Location holds (Exec ((b := (f,a)),s)) . b = (s . f) /. (abs (s . a))
proofend;

theorem Th3: :: SCMBSORT:3
for s being State of SCM+FSA
for f being FinSeq-Location
for a, b being Int-Location holds (Exec (((f,a) := b),s)) . f = (s . f) +* ((abs (s . a)),(s . b))
proofend;

theorem Th4: :: SCMBSORT:4
for s being State of SCM+FSA
for f being FinSeq-Location
for m, n being Element of NAT
for a being Int-Location st m <> n + 1 holds
(Exec (((intloc m) := (f,a)),(Initialized s))) . (intloc (n + 1)) = s . (intloc (n + 1))
proofend;

theorem Th5: :: SCMBSORT:5
for s being State of SCM+FSA
for m, n being Element of NAT
for a being Int-Location st m <> n + 1 holds
(Exec (((intloc m) := a),(Initialized s))) . (intloc (n + 1)) = s . (intloc (n + 1))
proofend;

theorem Th6: :: SCMBSORT:6
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for f being FinSeq-Location
for a being read-write Int-Location holds
( (IExec ((Stop SCM+FSA),p,s)) . a = s . a &amp; (IExec ((Stop SCM+FSA),p,s)) . f = s . f )
proofend;

theorem Th7: :: SCMBSORT:7
for p being preProgram of SCM+FSA
for ic being Instruction of SCM+FSA
for a, b being Int-Location st ic in rng p &amp; ( ic = a := b or ic = AddTo (a,b) or ic = SubFrom (a,b) or ic = MultBy (a,b) or ic = Divide (a,b) ) holds
( a in UsedIntLoc p &amp; b in UsedIntLoc p )
proofend;

theorem Th8: :: SCMBSORT:8
for p being preProgram of SCM+FSA
for ic being Instruction of SCM+FSA
for a being Int-Location
for la being Element of NAT st ic in rng p &amp; ( ic = a =0_goto la or ic = a >0_goto la ) holds
a in UsedIntLoc p
proofend;

theorem Th9: :: SCMBSORT:9
for p being preProgram of SCM+FSA
for ic being Instruction of SCM+FSA
for fa being FinSeq-Location
for b, a being Int-Location st ic in rng p &amp; ( ic = b := (fa,a) or ic = (fa,a) := b ) holds
( a in UsedIntLoc p &amp; b in UsedIntLoc p )
proofend;

theorem Th10: :: SCMBSORT:10
for p being preProgram of SCM+FSA
for ic being Instruction of SCM+FSA
for fa being FinSeq-Location
for b, a being Int-Location st ic in rng p &amp; ( ic = b := (fa,a) or ic = (fa,a) := b ) holds
fa in UsedInt*Loc p
proofend;

theorem Th11: :: SCMBSORT:11
for p being preProgram of SCM+FSA
for ic being Instruction of SCM+FSA
for fa being FinSeq-Location
for a being Int-Location st ic in rng p &amp; ( ic = a :=len fa or ic = fa :=<0,...,0> a ) holds
a in UsedIntLoc p
proofend;

theorem Th12: :: SCMBSORT:12
for p being preProgram of SCM+FSA
for ic being Instruction of SCM+FSA
for fa being FinSeq-Location
for a being Int-Location st ic in rng p &amp; ( ic = a :=len fa or ic = fa :=<0,...,0> a ) holds
fa in UsedInt*Loc p
proofend;

theorem Th13: :: SCMBSORT:13
for t being FinPartState of SCM+FSA
for p being Program of
for x being set st dom t c= Int-Locations \/ FinSeq-Locations &amp; x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) &amp; x is not Int-Location holds
x is FinSeq-Location
proofend;

theorem Th14: :: SCMBSORT:14
for p1, p2 being Instruction-Sequence of SCM+FSA
for i, k being Element of NAT
for t being FinPartState of SCM+FSA
for p being Program of
for s1, s2 being State of SCM+FSA st k <= i &amp; p c= p1 &amp; p c= p2 &amp; dom t c= Int-Locations \/ FinSeq-Locations &amp; ( for j being Element of NAT holds
( IC (Comput (p1,s1,j)) in dom p &amp; IC (Comput (p2,s2,j)) in dom p ) ) &amp; (Comput (p1,s1,k)) . (IC ) = (Comput (p2,s2,k)) . (IC ) &amp; (Comput (p1,s1,k)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Comput (p2,s2,k)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) holds
( (Comput (p1,s1,i)) . (IC ) = (Comput (p2,s2,i)) . (IC ) &amp; (Comput (p1,s1,i)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Comput (p2,s2,i)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) )
proofend;

theorem Th15: :: SCMBSORT:15
for p1, p2 being Instruction-Sequence of SCM+FSA
for i, k being Element of NAT
for p being Program of
for s1, s2 being State of SCM+FSA st k <= i &amp; p c= p1 &amp; p c= p2 &amp; ( for j being Element of NAT holds
( IC (Comput (p1,s1,j)) in dom p &amp; IC (Comput (p2,s2,j)) in dom p ) ) &amp; (Comput (p1,s1,k)) . (IC ) = (Comput (p2,s2,k)) . (IC ) &amp; (Comput (p1,s1,k)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Comput (p2,s2,k)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) holds
( (Comput (p1,s1,i)) . (IC ) = (Comput (p2,s2,i)) . (IC ) &amp; (Comput (p1,s1,i)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Comput (p2,s2,i)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) )
proofend;

theorem Th16: :: SCMBSORT:16
for I, J being Program of
for a being Int-Location holds
( UsedIntLoc (if=0 (a,I,J)) = ({a} \/ (UsedIntLoc I)) \/ (UsedIntLoc J) &amp; UsedIntLoc (if>0 (a,I,J)) = ({a} \/ (UsedIntLoc I)) \/ (UsedIntLoc J) )
proofend;

theorem Th17: :: SCMBSORT:17
for I being Program of
for l being Element of NAT holds UsedIntLoc (Directed (I,l)) = UsedIntLoc I
proofend;

theorem Th18: :: SCMBSORT:18
for a being Int-Location
for I being Program of holds UsedIntLoc (Times (a,I)) = (UsedIntLoc I) \/ {a,(intloc 0)}
proofend;

theorem Th19: :: SCMBSORT:19
for I being Program of
for l being Element of NAT holds UsedInt*Loc (Directed (I,l)) = UsedInt*Loc I
proofend;

theorem Th20: :: SCMBSORT:20
for a being Int-Location
for I being Program of holds UsedInt*Loc (Times (a,I)) = UsedInt*Loc I
proofend;

theorem :: SCMBSORT:21
canceled;

theorem Th22: :: SCMBSORT:22
for a being Int-Location
for I being Program of holds card (Times (a,I)) = (card I) + 12
proofend;

theorem Th23: :: SCMBSORT:23
for i1, i2, i3 being Instruction of SCM+FSA holds card ((i1 ";" i2) ";" i3) = 6
proofend;

theorem :: SCMBSORT:24
canceled;

theorem :: SCMBSORT:25
canceled;

theorem Th26: :: SCMBSORT:26
for I, J being Program of
for k being Element of NAT
for i being Instruction of SCM+FSA st k < card J &amp; i = J . k holds
(I ";" J) . ((card I) + k) = IncAddr (i,(card I))
proofend;

theorem Th27: :: SCMBSORT:27
for I, J being Program of
for i being ins-loc-free Instruction of SCM+FSA st i <> halt SCM+FSA holds
((I ";" i) ";" J) . (card I) = i
proofend;

theorem Th28: :: SCMBSORT:28
for I, J being Program of
for i being Instruction of SCM+FSA holds ((I ";" i) ";" J) . ((card I) + 1) = goto ((card I) + 2)
proofend;

theorem :: SCMBSORT:29
canceled;

theorem :: SCMBSORT:30
canceled;

theorem :: SCMBSORT:31
canceled;

theorem Th32: :: SCMBSORT:32
for p being Program of
for s being State of SCM+FSA holds (UsedInt*Loc p) \/ (UsedIntLoc p) c= dom s
proofend;

theorem Th33: :: SCMBSORT:33
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being Program of
for f being FinSeq-Location holds (Result ((p +* I),(Initialized s))) . f = (IExec (I,p,s)) . f
proofend;

set a0 = intloc 0;

set a1 = intloc 1;

set a2 = intloc 2;

set a3 = intloc 3;

set a4 = intloc 4;

set a5 = intloc 5;

set a6 = intloc 6;

Lm1:  intloc 0 <> intloc 2
by SCMFSA_2:101;

Lm2:  intloc 0 <> intloc 4
by SCMFSA_2:101;

Lm3:  intloc 0 <> intloc 5
by SCMFSA_2:101;

Lm4:  intloc 0 <> intloc 6
by SCMFSA_2:101;

Lm5:  intloc 1 <> intloc 2
by SCMFSA_2:101;

Lm6:  intloc 1 <> intloc 3
by SCMFSA_2:101;

Lm7:  intloc 1 <> intloc 4
by SCMFSA_2:101;

Lm8:  intloc 1 <> intloc 5
by SCMFSA_2:101;

Lm9:  intloc 1 <> intloc 6
by SCMFSA_2:101;

Lm10:  intloc 2 <> intloc 3
by SCMFSA_2:101;

Lm11:  intloc 2 <> intloc 4
by SCMFSA_2:101;

Lm12:  intloc 2 <> intloc 5
by SCMFSA_2:101;

Lm13:  intloc 2 <> intloc 6
by SCMFSA_2:101;

Lm14:  intloc 3 <> intloc 4
by SCMFSA_2:101;

Lm15:  intloc 3 <> intloc 5
by SCMFSA_2:101;

Lm16:  intloc 3 <> intloc 6
by SCMFSA_2:101;

Lm17:  intloc 4 <> intloc 5
by SCMFSA_2:101;

Lm18:  intloc 4 <> intloc 6
by SCMFSA_2:101;

Lm19:  intloc 5 <> intloc 6
by SCMFSA_2:101;

set initializeWorkMem = (((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0))) ";" ((intloc 5) := (intloc 0))) ";" ((intloc 6) := (intloc 0));

:: set a0 = intloc 0;
:: set a1 = intloc 1;
:: set a2 = intloc 2;
:: set a3 = intloc 3;
:: set a4 = intloc 4;
:: set a5 = intloc 5;
:: set a6 = intloc 6;
:: set initializeWorkMem= (a2:= a0) ";" (a3:= a0) ";"
:: (a4:= a0) ";" (a5:= a0) ";" (a6:= a0);
definition
let f be FinSeq-Location ;
func bubble-sort f ->  Program of  equals :: SCMBSORT:def 1
(((((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0))) ";" ((intloc 5) := (intloc 0))) ";" ((intloc 6) := (intloc 0))) ";" ((intloc 1) :=len f)) ";" (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ";" (SubFrom ((intloc 2),(intloc 0)))) ";" ((intloc 3) :=len f)) ";" (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := (f,(intloc 3)))) ";" ((intloc 6) := (f,(intloc 4)))) ";" (SubFrom ((intloc 6),(intloc 5)))) ";" (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ";" ((f,(intloc 3)) := (intloc 6))) ";" ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))))))));
correctness
coherence
(((((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0))) ";" ((intloc 5) := (intloc 0))) ";" ((intloc 6) := (intloc 0))) ";" ((intloc 1) :=len f)) ";" (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ";" (SubFrom ((intloc 2),(intloc 0)))) ";" ((intloc 3) :=len f)) ";" (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := (f,(intloc 3)))) ";" ((intloc 6) := (f,(intloc 4)))) ";" (SubFrom ((intloc 6),(intloc 5)))) ";" (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ";" ((f,(intloc 3)) := (intloc 6))) ";" ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))))))) is Program of ;
;
end;

:: deftheorem  defines bubble-sort SCMBSORT:def_1_:_
 for f being FinSeq-Location holds bubble-sort f = (((((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0))) ";" ((intloc 5) := (intloc 0))) ";" ((intloc 6) := (intloc 0))) ";" ((intloc 1) :=len f)) ";" (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ";" (SubFrom ((intloc 2),(intloc 0)))) ";" ((intloc 3) :=len f)) ";" (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := (f,(intloc 3)))) ";" ((intloc 6) := (f,(intloc 4)))) ";" (SubFrom ((intloc 6),(intloc 5)))) ";" (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ";" ((f,(intloc 3)) := (intloc 6))) ";" ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))))))));

definition
func Bubble-Sort-Algorithm  ->  Program of  equals :: SCMBSORT:def 2
 bubble-sort (fsloc 0);
coherence
 bubble-sort (fsloc 0) is Program of ;
end;

:: deftheorem  defines Bubble-Sort-Algorithm SCMBSORT:def_2_:_
 Bubble-Sort-Algorithm = bubble-sort (fsloc 0);

set b1 = intloc (0 + 1);

set b2 = intloc (1 + 1);

set b3 = intloc (2 + 1);

set b4 = intloc (3 + 1);

set b5 = intloc (4 + 1);

set b6 = intloc (5 + 1);

set f0 = fsloc 0;

set i1 = (intloc (3 + 1)) := (intloc (2 + 1));

set i2 = SubFrom ((intloc (2 + 1)),(intloc 0));

set i3 = (intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1)));

set i4 = (intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)));

set i5 = SubFrom ((intloc (5 + 1)),(intloc (4 + 1)));

set i6 = ((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1));

set i7 = ((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1));

set SS = Stop SCM+FSA;

set ifc = if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA));

set body2 = ((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)));

set T2 = Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))));

set j1 = (intloc (1 + 1)) := (intloc (0 + 1));

set j2 = SubFrom ((intloc (1 + 1)),(intloc 0));

set j3 = (intloc (2 + 1)) :=len (fsloc 0);

set Sb = (((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))) ";" ((intloc (2 + 1)) :=len (fsloc 0));

set body1 = ((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))) ";" ((intloc (2 + 1)) :=len (fsloc 0))) ";" (Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))))));

set T1 = Times ((intloc (0 + 1)),(((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))) ";" ((intloc (2 + 1)) :=len (fsloc 0))) ";" (Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))))))));

set w2 = (intloc (1 + 1)) := (intloc 0);

set w3 = (intloc (2 + 1)) := (intloc 0);

set w4 = (intloc (3 + 1)) := (intloc 0);

set w5 = (intloc (4 + 1)) := (intloc 0);

set w6 = (intloc (5 + 1)) := (intloc 0);

set w7 = (intloc (0 + 1)) :=len (fsloc 0);

theorem Th34: :: SCMBSORT:34
for f being FinSeq-Location holds UsedIntLoc (bubble-sort f) = {(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}
proofend;

theorem Th35: :: SCMBSORT:35
for f being FinSeq-Location holds UsedInt*Loc (bubble-sort f) = {f}
proofend;

theorem :: SCMBSORT:36
canceled;

theorem :: SCMBSORT:37
canceled;

theorem Th38: :: SCMBSORT:38
for f being FinSeq-Location holds card (bubble-sort f) = 63
proofend;

theorem Th39: :: SCMBSORT:39
for P being Instruction-Sequence of SCM+FSA st Bubble-Sort-Algorithm c= P holds
for f being FinSeq-Location
for k being Element of NAT st k < 63 holds
Bubble-Sort-Algorithm . k = P . k
proofend;

Lm20:  for P being Instruction-Sequence of SCM+FSA st Bubble-Sort-Algorithm c= P holds
( P . 0 = (intloc 2) := (intloc 0) &amp; P . 1 = goto 2 &amp; P . 2 = (intloc 3) := (intloc 0) &amp; P . 3 = goto 4 &amp; P . 4 = (intloc 4) := (intloc 0) &amp; P . 5 = goto 6 &amp; P . 6 = (intloc 5) := (intloc 0) &amp; P . 7 = goto 8 &amp; P . 8 = (intloc 6) := (intloc 0) &amp; P . 9 = goto 10 &amp; P . 10 = (intloc 1) :=len (fsloc 0) &amp; P . 11 = goto 12 )
proofend;

Lm21:  for s being 0 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st Bubble-Sort-Algorithm c= P holds
( (Comput (P,s,1)) . (IC ) = 1 &amp; (Comput (P,s,1)) . (intloc 0) = s . (intloc 0) &amp; (Comput (P,s,1)) . (fsloc 0) = s . (fsloc 0) &amp; (Comput (P,s,2)) . (IC ) = 2 &amp; (Comput (P,s,2)) . (intloc 0) = s . (intloc 0) &amp; (Comput (P,s,2)) . (fsloc 0) = s . (fsloc 0) &amp; (Comput (P,s,3)) . (IC ) = 3 &amp; (Comput (P,s,3)) . (intloc 0) = s . (intloc 0) &amp; (Comput (P,s,3)) . (fsloc 0) = s . (fsloc 0) &amp; (Comput (P,s,4)) . (IC ) = 4 &amp; (Comput (P,s,4)) . (intloc 0) = s . (intloc 0) &amp; (Comput (P,s,4)) . (fsloc 0) = s . (fsloc 0) &amp; (Comput (P,s,5)) . (IC ) = 5 &amp; (Comput (P,s,5)) . (intloc 0) = s . (intloc 0) &amp; (Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0) &amp; (Comput (P,s,6)) . (IC ) = 6 &amp; (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) &amp; (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) &amp; (Comput (P,s,7)) . (IC ) = 7 &amp; (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) &amp; (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) &amp; (Comput (P,s,8)) . (IC ) = 8 &amp; (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) &amp; (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) &amp; (Comput (P,s,9)) . (IC ) = 9 &amp; (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) &amp; (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) &amp; (Comput (P,s,10)) . (IC ) = 10 &amp; (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) &amp; (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) &amp; (Comput (P,s,11)) . (IC ) = 11 &amp; (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) &amp; (Comput (P,s,11)) . (fsloc 0) = s . (fsloc 0) &amp; (Comput (P,s,11)) . (intloc 1) = len (s . (fsloc 0)) &amp; (Comput (P,s,11)) . (intloc 2) = s . (intloc 0) &amp; (Comput (P,s,11)) . (intloc 3) = s . (intloc 0) &amp; (Comput (P,s,11)) . (intloc 4) = s . (intloc 0) &amp; (Comput (P,s,11)) . (intloc 5) = s . (intloc 0) &amp; (Comput (P,s,11)) . (intloc 6) = s . (intloc 0) )
proofend;

Lm22:  not ((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))) destroys intloc (1 + 1)
proofend;

Lm23:  ( Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))))) is good &amp; Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))))) is InitHalting )
proofend;

Lm24:  not ((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))) destroys intloc (0 + 1)
proofend;

Lm25:  not ((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))) ";" ((intloc (2 + 1)) :=len (fsloc 0))) ";" (Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))))) destroys intloc (0 + 1)
proofend;

Lm26:  ( Times ((intloc (0 + 1)),(((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))) ";" ((intloc (2 + 1)) :=len (fsloc 0))) ";" (Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))))))) is good &amp; Times ((intloc (0 + 1)),(((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))) ";" ((intloc (2 + 1)) :=len (fsloc 0))) ";" (Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))))))) is InitHalting )
proofend;

theorem :: SCMBSORT:40
( bubble-sort (fsloc 0) is keepInt0_1 &amp; bubble-sort (fsloc 0) is InitHalting ) by Lm26;

Lm27:  for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA holds
( ( s . (intloc (5 + 1)) > 0 implies (IExec ((if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))),p,s)) . (fsloc 0) = ((s . (fsloc 0)) +* ((abs (s . (intloc (2 + 1)))),((s . (fsloc 0)) /. (abs (s . (intloc (3 + 1))))))) +* ((abs (s . (intloc (3 + 1)))),(s . (intloc (4 + 1)))) ) &amp; ( s . (intloc (5 + 1)) <= 0 implies (IExec ((if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))),p,s)) . (fsloc 0) = s . (fsloc 0) ) )
proofend;

Lm28:  for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA holds (IExec ((if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))),p,s)) . (intloc (2 + 1)) = s . (intloc (2 + 1))
proofend;

Lm29:  for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA st s . (intloc (2 + 1)) <= len (s . (fsloc 0)) &amp; s . (intloc (2 + 1)) >= 2 holds
( (IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (intloc (2 + 1)) = (s . (intloc (2 + 1))) - 1 &amp; s . (fsloc 0),(IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0) are_fiberwise_equipotent &amp; ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) ) &amp; ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) ) &amp; ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) ) &amp; ( for k being set st k <> (s . (intloc (2 + 1))) - 1 &amp; k <> s . (intloc (2 + 1)) &amp; k in dom (s . (fsloc 0)) holds
(s . (fsloc 0)) . k = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k ) &amp; ex x1, x2 being Integer st
( x1 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) &amp; x2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) &amp; x1 >= x2 ) )
proofend;

Lm30:  for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA st s . (intloc (1 + 1)) >= 0 &amp; s . (intloc (1 + 1)) < s . (intloc (2 + 1)) &amp; s . (intloc (2 + 1)) <= len (s . (fsloc 0)) holds
ex k being Element of NAT st
( k <= s . (intloc (2 + 1)) &amp; k >= (s . (intloc (2 + 1))) - (s . (intloc (1 + 1))) &amp; ((IExec ((Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))))),p,s)) . (fsloc 0)) . k = (s . (fsloc 0)) . (s . (intloc (2 + 1))) )
proofend;

Lm31:  for k being Element of NAT
for t being State of SCM+FSA
for q being Instruction-Sequence of SCM+FSA st k = t . (intloc (1 + 1)) &amp; k < t . (intloc (2 + 1)) &amp; t . (intloc (2 + 1)) <= len (t . (fsloc 0)) holds
( t . (fsloc 0),(IExec ((Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))))),q,t)) . (fsloc 0) are_fiberwise_equipotent &amp; ( for m being Element of NAT st ( ( m < (t . (intloc (2 + 1))) - k &amp; m >= 1 ) or ( m > t . (intloc (2 + 1)) &amp; m in dom (t . (fsloc 0)) ) ) holds
(t . (fsloc 0)) . m = ((IExec ((Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))))),q,t)) . (fsloc 0)) . m ) &amp; ( for m being Element of NAT st m >= (t . (intloc (2 + 1))) - k &amp; m <= t . (intloc (2 + 1)) holds
ex x1, x2 being Integer st
( x1 = ((IExec ((Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))))),q,t)) . (fsloc 0)) . ((t . (intloc (2 + 1))) - k) &amp; x2 = ((IExec ((Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))))),q,t)) . (fsloc 0)) . m &amp; x1 >= x2 ) ) &amp; ( for i being Element of NAT st i >= (t . (intloc (2 + 1))) - k &amp; i <= t . (intloc (2 + 1)) holds
ex n being Element of NAT st
( n >= (t . (intloc (2 + 1))) - k &amp; n <= t . (intloc (2 + 1)) &amp; ((IExec ((Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))))),q,t)) . (fsloc 0)) . i = (t . (fsloc 0)) . n ) ) )
proofend;

Lm32:  for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA holds
( (IExec (((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))) ";" ((intloc (2 + 1)) :=len (fsloc 0))),p,s)) . (intloc (1 + 1)) = (s . (intloc (0 + 1))) - 1 &amp; (IExec (((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))) ";" ((intloc (2 + 1)) :=len (fsloc 0))),p,s)) . (intloc (2 + 1)) = len (s . (fsloc 0)) &amp; (IExec (((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))) ";" ((intloc (2 + 1)) :=len (fsloc 0))),p,s)) . (fsloc 0) = s . (fsloc 0) )
proofend;

Lm33:  for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA st s . (intloc (0 + 1)) = len (s . (fsloc 0)) holds
( s . (fsloc 0),(IExec ((Times ((intloc (0 + 1)),(((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))) ";" ((intloc (2 + 1)) :=len (fsloc 0))) ";" (Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))))))))),p,s)) . (fsloc 0) are_fiberwise_equipotent &amp; ( for i, j being Element of NAT st i >= 1 &amp; j <= len (s . (fsloc 0)) &amp; i < j holds
for x1, x2 being Integer st x1 = ((IExec ((Times ((intloc (0 + 1)),(((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))) ";" ((intloc (2 + 1)) :=len (fsloc 0))) ";" (Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))))))))),p,s)) . (fsloc 0)) . i &amp; x2 = ((IExec ((Times ((intloc (0 + 1)),(((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))) ";" ((intloc (2 + 1)) :=len (fsloc 0))) ";" (Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))))))))),p,s)) . (fsloc 0)) . j holds
x1 >= x2 ) )
proofend;

theorem Th41: :: SCMBSORT:41
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA holds
( s . (fsloc 0),(IExec ((bubble-sort (fsloc 0)),p,s)) . (fsloc 0) are_fiberwise_equipotent &amp; ( for i, j being Element of NAT st i >= 1 &amp; j <= len (s . (fsloc 0)) &amp; i < j holds
for x1, x2 being Integer st x1 = ((IExec ((bubble-sort (fsloc 0)),p,s)) . (fsloc 0)) . i &amp; x2 = ((IExec ((bubble-sort (fsloc 0)),p,s)) . (fsloc 0)) . j holds
x1 >= x2 ) )
proofend;

theorem Th42: :: SCMBSORT:42
for i being Element of NAT
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st Bubble-Sort-Algorithm c= P holds
for w being FinSequence of INT st Initialized ((fsloc 0) .--> w) c= s holds
IC (Comput (P,s,i)) in dom Bubble-Sort-Algorithm
proofend;

theorem Th43: :: SCMBSORT:43
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for t being FinSequence of INT st (Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t) c= s &amp; Bubble-Sort-Algorithm c= p holds
ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent &amp; u is non-increasing &amp; u is FinSequence of INT &amp; (Result (p,s)) . (fsloc 0) = u )
proofend;

theorem Th44: :: SCMBSORT:44
for w being FinSequence of INT holds Initialized ((fsloc 0) .--> w) is Bubble-Sort-Algorithm -autonomic
proofend;

registration
cluster Bubble-Sort-Algorithm  ->  non halt-free ;
coherence
 not Bubble-Sort-Algorithm is halt-free ;
end;

theorem :: SCMBSORT:45
Bubble-Sort-Algorithm , Initialize ((intloc 0) .--> 1) computes Sorting-Function
proofend;