:: Bubble Sort on SCM+FSA
:: by JingChao Chen and Yatsuka Nakamura
::
:: Copyright (c) 1998-2021 Association of Mizar Users

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

theorem :: SCMBSORT:1
canceled;

::$CT theorem Th1: :: 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) /. |.(s . a).| proof end; theorem Th2: :: 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) +* (|.(s . a).|,(s . b)) proof end; theorem Th3: :: SCMBSORT:4 for s being State of SCM+FSA for f being FinSeq-Location for m, n being Nat for a being Int-Location st m <> n + 1 holds (Exec ((() := (f,a)),())) . (intloc (n + 1)) = s . (intloc (n + 1)) proof end; theorem Th4: :: SCMBSORT:5 for s being State of SCM+FSA for m, n being Nat for a being Int-Location st m <> n + 1 holds (Exec ((() := a),())) . (intloc (n + 1)) = s . (intloc (n + 1)) proof end; theorem Th5: :: 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 ((),p,s)) . a = s . a & (IExec ((),p,s)) . f = s . f ) proof end; theorem Th6: :: 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 & ( 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 UsedILoc p & b in UsedILoc p ) proof end; theorem Th7: :: SCMBSORT:8 for p being preProgram of SCM+FSA for ic being Instruction of SCM+FSA for a being Int-Location for la being Nat st ic in rng p & ( ic = a =0_goto la or ic = a >0_goto la ) holds a in UsedILoc p proof end; theorem Th8: :: SCMBSORT:9 for p being preProgram of SCM+FSA for ic being Instruction of SCM+FSA for fa being FinSeq-Location for a, b being Int-Location st ic in rng p & ( ic = b := (fa,a) or ic = (fa,a) := b ) holds ( a in UsedILoc p & b in UsedILoc p ) proof end; theorem Th9: :: SCMBSORT:10 for p being preProgram of SCM+FSA for ic being Instruction of SCM+FSA for fa being FinSeq-Location for a, b being Int-Location st ic in rng p & ( ic = b := (fa,a) or ic = (fa,a) := b ) holds fa in UsedI*Loc p proof end; theorem Th10: :: 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 & ( ic = a :=len fa or ic = fa :=<0,...,0> a ) holds a in UsedILoc p proof end; theorem Th11: :: 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 & ( ic = a :=len fa or ic = fa :=<0,...,0> a ) holds fa in UsedI*Loc p proof end; theorem Th12: :: 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 & x in ((dom t) \/ ()) \/ () & x is not Int-Location holds x is FinSeq-Location proof end; theorem Th13: :: SCMBSORT:14 for p1, p2 being Instruction-Sequence of SCM+FSA for i, k being Nat for t being FinPartState of SCM+FSA for p being Program of for s1, s2 being State of SCM+FSA st k <= i & p c= p1 & p c= p2 & dom t c= Int-Locations \/ FinSeq-Locations & ( for j being Nat holds ( IC (Comput (p1,s1,j)) in dom p & IC (Comput (p2,s2,j)) in dom p ) ) & (Comput (p1,s1,k)) . () = (Comput (p2,s2,k)) . () & (Comput (p1,s1,k)) | (((dom t) \/ ()) \/ ()) = (Comput (p2,s2,k)) | (((dom t) \/ ()) \/ ()) holds ( (Comput (p1,s1,i)) . () = (Comput (p2,s2,i)) . () & (Comput (p1,s1,i)) | (((dom t) \/ ()) \/ ()) = (Comput (p2,s2,i)) | (((dom t) \/ ()) \/ ()) ) proof end; theorem Th14: :: SCMBSORT:15 for p1, p2 being Instruction-Sequence of SCM+FSA for i, k being Nat for p being Program of for s1, s2 being State of SCM+FSA st k <= i & p c= p1 & p c= p2 & ( for j being Nat holds ( IC (Comput (p1,s1,j)) in dom p & IC (Comput (p2,s2,j)) in dom p ) ) & (Comput (p1,s1,k)) . () = (Comput (p2,s2,k)) . () & (Comput (p1,s1,k)) | (() \/ ()) = (Comput (p2,s2,k)) | (() \/ ()) holds ( (Comput (p1,s1,i)) . () = (Comput (p2,s2,i)) . () & (Comput (p1,s1,i)) | (() \/ ()) = (Comput (p2,s2,i)) | (() \/ ()) ) proof end; theorem :: SCMBSORT:16 canceled; theorem :: SCMBSORT:17 canceled; theorem :: SCMBSORT:18 canceled; theorem :: SCMBSORT:19 canceled; theorem :: SCMBSORT:20 canceled; theorem :: SCMBSORT:21 canceled; theorem :: SCMBSORT:22 canceled; ::$CT 7
theorem Th15: :: SCMBSORT:23
for i1, i2, i3 being Instruction of SCM+FSA holds card ((i1 ";" i2) ";" i3) = 6
proof end;

theorem :: SCMBSORT:24
canceled;

theorem :: SCMBSORT:25
canceled;

::$CT 2 theorem Th16: :: SCMBSORT:26 for I, J being Program of for k being Nat for i being Instruction of SCM+FSA st k < card J & i = J . k holds (I ";" J) . ((card I) + k) = IncAddr (i,(card I)) proof end; theorem Th17: :: 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 proof end; theorem Th18: :: 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) proof end; theorem :: SCMBSORT:29 canceled; theorem :: SCMBSORT:30 canceled; theorem :: SCMBSORT:31 canceled; ::$CT 3
theorem Th19: :: SCMBSORT:32
for p being Program of
for s being State of SCM+FSA holds () \/ () c= dom s
proof end;

theorem Th20: :: 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),())) . f = (IExec (I,p,s)) . f
proof end;

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:
by SCMFSA_2:101;

Lm2:
by SCMFSA_2:101;

Lm3:
by SCMFSA_2:101;

Lm4:
by SCMFSA_2:101;

Lm5:
by SCMFSA_2:101;

Lm6:
by SCMFSA_2:101;

Lm7:
by SCMFSA_2:101;

Lm8:
by SCMFSA_2:101;

Lm9:
by SCMFSA_2:101;

Lm10:
by SCMFSA_2:101;

Lm11:
by SCMFSA_2:101;

Lm12:
by SCMFSA_2:101;

Lm13:
by SCMFSA_2:101;

Lm14:
by SCMFSA_2:101;

Lm15:
by SCMFSA_2:101;

Lm16:
by SCMFSA_2:101;

Lm17:
by SCMFSA_2:101;

Lm18:
by SCMFSA_2:101;

Lm19:
by SCMFSA_2:101;

set initializeWorkMem = ((((() := ()) ";" (() := ())) ";" (() := ())) ";" (() := ())) ";" (() := ());

:: 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
((((((() := ()) ";" (() := ())) ";" (() := ())) ";" (() := ())) ";" (() := ())) ";" (() :=len f)) ";" (Times ((),((((() := ()) ";" (SubFrom ((),()))) ";" (() :=len f)) ";" (Times ((),((((((() := ()) ";" (SubFrom ((),()))) ";" (() := (f,()))) ";" (() := (f,()))) ";" (SubFrom ((),()))) ";" (if>0 ((),(((() := (f,())) ";" ((f,()) := ())) ";" ((f,()) := ())),()))))))));
correctness
coherence
((((((() := ()) ";" (() := ())) ";" (() := ())) ";" (() := ())) ";" (() := ())) ";" (() :=len f)) ";" (Times ((),((((() := ()) ";" (SubFrom ((),()))) ";" (() :=len f)) ";" (Times ((),((((((() := ()) ";" (SubFrom ((),()))) ";" (() := (f,()))) ";" (() := (f,()))) ";" (SubFrom ((),()))) ";" (if>0 ((),(((() := (f,())) ";" ((f,()) := ())) ";" ((f,()) := ())),())))))))) is Program of
;
;
end;

:: deftheorem defines bubble-sort SCMBSORT:def 1 :
for f being FinSeq-Location holds bubble-sort f = ((((((() := ()) ";" (() := ())) ";" (() := ())) ";" (() := ())) ";" (() := ())) ";" (() :=len f)) ";" (Times ((),((((() := ()) ";" (SubFrom ((),()))) ";" (() :=len f)) ";" (Times ((),((((((() := ()) ";" (SubFrom ((),()))) ";" (() := (f,()))) ";" (() := (f,()))) ";" (SubFrom ((),()))) ";" (if>0 ((),(((() := (f,())) ";" ((f,()) := ())) ";" ((f,()) := ())),()))))))));

definition
coherence
bubble-sort () is Program of
;
end;

:: deftheorem defines Bubble-Sort-Algorithm SCMBSORT:def 2 :

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)),());

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

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

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

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

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

set SS = Stop SCM+FSA;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Th21: :: SCMBSORT:34
for f being FinSeq-Location holds UsedILoc () = {(),(),(),(),(),(),()}
proof end;

theorem Th22: :: SCMBSORT:35
for f being FinSeq-Location holds UsedI*Loc () = {f}
proof end;

theorem :: SCMBSORT:36
canceled;

theorem :: SCMBSORT:37
canceled;

::\$CT 2
theorem Th23: :: SCMBSORT:38
for f being FinSeq-Location holds card () = 53
proof end;

theorem Th24: :: 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 Nat st k < 53 holds
Bubble-Sort-Algorithm . k = P . k
proof end;

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

proof end;

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)) . () = 1 & (Comput (P,s,1)) . () = s . () & (Comput (P,s,1)) . () = s . () & (Comput (P,s,2)) . () = 2 & (Comput (P,s,2)) . () = s . () & (Comput (P,s,2)) . () = s . () & (Comput (P,s,3)) . () = 3 & (Comput (P,s,3)) . () = s . () & (Comput (P,s,3)) . () = s . () & (Comput (P,s,4)) . () = 4 & (Comput (P,s,4)) . () = s . () & (Comput (P,s,4)) . () = s . () & (Comput (P,s,5)) . () = 5 & (Comput (P,s,5)) . () = s . () & (Comput (P,s,5)) . () = s . () & (Comput (P,s,6)) . () = 6 & (Comput (P,s,6)) . () = s . () & (Comput (P,s,6)) . () = s . () & (Comput (P,s,7)) . () = 7 & (Comput (P,s,7)) . () = s . () & (Comput (P,s,7)) . () = s . () & (Comput (P,s,8)) . () = 8 & (Comput (P,s,8)) . () = s . () & (Comput (P,s,8)) . () = s . () & (Comput (P,s,9)) . () = 9 & (Comput (P,s,9)) . () = s . () & (Comput (P,s,9)) . () = s . () & (Comput (P,s,10)) . () = 10 & (Comput (P,s,10)) . () = s . () & (Comput (P,s,10)) . () = s . () & (Comput (P,s,11)) . () = 11 & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = len (s . ()) & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () )

proof end;

Lm22: not ((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((),(intloc (3 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (3 + 1))) := (intloc (4 + 1)))),())) destroys intloc (1 + 1)
proof end;

Lm23: ( Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((),(intloc (3 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (3 + 1))) := (intloc (4 + 1)))),())))) is good & Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((),(intloc (3 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (3 + 1))) := (intloc (4 + 1)))),())))) is InitHalting )
proof end;

Lm24: not ((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((),(intloc (3 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (3 + 1))) := (intloc (4 + 1)))),())) destroys intloc (0 + 1)
proof end;

Lm25: not ((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),()))) ";" ((intloc (2 + 1)) :=len ())) ";" (Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((),(intloc (3 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (3 + 1))) := (intloc (4 + 1)))),()))))) destroys intloc (0 + 1)
proof end;

Lm26: ( Times ((intloc (0 + 1)),(((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),()))) ";" ((intloc (2 + 1)) :=len ())) ";" (Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((),(intloc (3 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (3 + 1))) := (intloc (4 + 1)))),()))))))) is good & Times ((intloc (0 + 1)),(((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),()))) ";" ((intloc (2 + 1)) :=len ())) ";" (Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((),(intloc (3 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (3 + 1))) := (intloc (4 + 1)))),()))))))) is InitHalting )
proof end;

theorem :: SCMBSORT:40
( bubble-sort () is keepInt0_1 & bubble-sort () 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)) := ((),(intloc (3 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (3 + 1))) := (intloc (4 + 1)))),())),p,s)) . () = ((s . ()) +* (|.(s . (intloc (2 + 1))).|,((s . ()) /. |.(s . (intloc (3 + 1))).|))) +* (|.(s . (intloc (3 + 1))).|,(s . (intloc (4 + 1)))) ) & ( s . (intloc (5 + 1)) <= 0 implies (IExec ((if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((),(intloc (3 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (3 + 1))) := (intloc (4 + 1)))),())),p,s)) . () = s . () ) )

proof end;

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)) := ((),(intloc (3 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (3 + 1))) := (intloc (4 + 1)))),())),p,s)) . (intloc (2 + 1)) = s . (intloc (2 + 1))

proof end;

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

proof end;

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

proof end;

Lm31: for k being Nat
for t being State of SCM+FSA
for q being Instruction-Sequence of SCM+FSA st k = t . (intloc (1 + 1)) & k < t . (intloc (2 + 1)) & t . (intloc (2 + 1)) <= len (t . ()) holds
( t . (),(IExec ((Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((),(intloc (3 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (3 + 1))) := (intloc (4 + 1)))),()))))),q,t)) . () are_fiberwise_equipotent & ( for m being Nat st ( ( m < (t . (intloc (2 + 1))) - k & m >= 1 ) or ( m > t . (intloc (2 + 1)) & m in dom (t . ()) ) ) holds
(t . ()) . m = ((IExec ((Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((),(intloc (3 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (3 + 1))) := (intloc (4 + 1)))),()))))),q,t)) . ()) . m ) & ( for m being Nat st m >= (t . (intloc (2 + 1))) - k & 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 (4 + 1)) := ((),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((),(intloc (3 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (3 + 1))) := (intloc (4 + 1)))),()))))),q,t)) . ()) . ((t . (intloc (2 + 1))) - k) & x2 = ((IExec ((Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((),(intloc (3 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (3 + 1))) := (intloc (4 + 1)))),()))))),q,t)) . ()) . m & x1 >= x2 ) ) & ( for i being Nat st i >= (t . (intloc (2 + 1))) - k & i <= t . (intloc (2 + 1)) holds
ex n being Nat st
( n >= (t . (intloc (2 + 1))) - k & n <= t . (intloc (2 + 1)) & ((IExec ((Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((),(intloc (3 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (3 + 1))) := (intloc (4 + 1)))),()))))),q,t)) . ()) . i = (t . ()) . n ) ) )

proof end;

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 (2 + 1)) :=len ())),p,s)) . (intloc (1 + 1)) = (s . (intloc (0 + 1))) - 1 & (IExec (((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),()))) ";" ((intloc (2 + 1)) :=len ())),p,s)) . (intloc (2 + 1)) = len (s . ()) & (IExec (((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),()))) ";" ((intloc (2 + 1)) :=len ())),p,s)) . () = s . () )

proof end;

Lm33: for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA st s . (intloc (0 + 1)) = len (s . ()) holds
( s . (),(IExec ((Times ((intloc (0 + 1)),(((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),()))) ";" ((intloc (2 + 1)) :=len ())) ";" (Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((),(intloc (3 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (3 + 1))) := (intloc (4 + 1)))),())))))))),p,s)) . () are_fiberwise_equipotent & ( for i, j being Nat st i >= 1 & j <= len (s . ()) & 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 (2 + 1)) :=len ())) ";" (Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((),(intloc (3 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (3 + 1))) := (intloc (4 + 1)))),())))))))),p,s)) . ()) . i & x2 = ((IExec ((Times ((intloc (0 + 1)),(((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),()))) ";" ((intloc (2 + 1)) :=len ())) ";" (Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((),(intloc (3 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (3 + 1))) := (intloc (4 + 1)))),())))))))),p,s)) . ()) . j holds
x1 >= x2 ) )

proof end;

theorem Th26: :: SCMBSORT:41
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA holds
( s . (),(IExec ((),p,s)) . () are_fiberwise_equipotent & ( for i, j being Nat st i >= 1 & j <= len (s . ()) & i < j holds
for x1, x2 being Integer st x1 = ((IExec ((),p,s)) . ()) . i & x2 = ((IExec ((),p,s)) . ()) . j holds
x1 >= x2 ) )
proof end;

theorem Th27: :: SCMBSORT:42
for i being 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 (() .--> w) c= s holds
IC (Comput (P,s,i)) in dom Bubble-Sort-Algorithm
proof end;

theorem Th28: :: 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 (() .--> 1)) +* (() .--> t) c= s & Bubble-Sort-Algorithm c= p holds
ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result (p,s)) . () = u )
proof end;

theorem Th29: :: SCMBSORT:44
for w being FinSequence of INT holds Initialized (() .--> w) is Bubble-Sort-Algorithm -autonomic
proof end;

registration end;

theorem :: SCMBSORT:45
proof end;