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

begin

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

theorem :: SCMBSORT:1

canceled;

theorem :: SCMBSORT:2

canceled;

theorem Th3: :: SCMBSORT:3

for I being Program of {INT,(INT *)}
for a, b being Int-Location st not I destroys b & a <> b holds
not Times (a,I) destroys b

proof end;

theorem :: SCMBSORT:4

canceled;

theorem :: SCMBSORT:5

canceled;

theorem :: SCMBSORT:6

canceled;

theorem :: SCMBSORT:7

canceled;

theorem Th8: :: SCMBSORT:8

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))

proof end;

theorem Th9: :: SCMBSORT:9

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))

proof end;

theorem Th10: :: SCMBSORT:10

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))

proof end;

theorem Th11: :: SCMBSORT:11

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))

proof end;

theorem Th12: :: SCMBSORT:12

for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 & (IExec ((Stop SCM+FSA),p,s)) . f = s . f )

proof end;

theorem :: SCMBSORT:13

canceled;

theorem :: SCMBSORT:14

canceled;

theorem :: SCMBSORT:15

canceled;

theorem Th16: :: SCMBSORT:16

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 UsedIntLoc p & b in UsedIntLoc p )

proof end;

theorem Th17: :: SCMBSORT:17

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 & ( ic = a =0_goto la or ic = a >0_goto la ) holds
a in UsedIntLoc p

proof end;

theorem Th18: :: SCMBSORT:18

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 & ( ic = b := (fa,a) or ic = (fa,a) := b ) holds
( a in UsedIntLoc p & b in UsedIntLoc p )

proof end;

theorem Th19: :: SCMBSORT:19

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 & ( ic = b := (fa,a) or ic = (fa,a) := b ) holds
fa in UsedInt*Loc p

proof end;

theorem Th20: :: SCMBSORT:20

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 UsedIntLoc p

proof end;

theorem Th21: :: SCMBSORT:21

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 UsedInt*Loc p

proof end;

theorem :: SCMBSORT:22

canceled;

theorem Th23: :: SCMBSORT:23

for t being FinPartState of SCM+FSA
for p being Program of {INT,(INT *)}
for x being set st dom t c= Int-Locations \/ FinSeq-Locations & x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) & x is not Int-Location holds
x is FinSeq-Location

proof end;

theorem :: SCMBSORT:24

canceled;

theorem Th25: :: SCMBSORT:25

for p1, p2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for i, k being Element of NAT
for t being FinPartState of SCM+FSA
for p being Program of {INT,(INT *)}
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 Element of NAT holds
( IC (Comput (p1,s1,j)) in dom p & IC (Comput (p2,s2,j)) in dom p ) ) & (Comput (p1,s1,k)) . (IC ) = (Comput (p2,s2,k)) . (IC ) & (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 ) & (Comput (p1,s1,i)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Comput (p2,s2,i)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) )

proof end;

theorem Th26: :: SCMBSORT:26

for p1, p2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for i, k being Element of NAT
for p being Program of {INT,(INT *)}
for s1, s2 being State of SCM+FSA st k <= i & p c= p1 & p c= p2 & ( for j being Element of NAT holds
( IC (Comput (p1,s1,j)) in dom p & IC (Comput (p2,s2,j)) in dom p ) ) & (Comput (p1,s1,k)) . (IC ) = (Comput (p2,s2,k)) . (IC ) & (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 ) & (Comput (p1,s1,i)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Comput (p2,s2,i)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) )

proof end;

theorem :: SCMBSORT:27

canceled;

theorem :: SCMBSORT:28

canceled;

theorem Th29: :: SCMBSORT:29

for I, J being Program of {INT,(INT *)}
for a being Int-Location holds
( UsedIntLoc (if=0 (a,I,J)) = ({a} \/ (UsedIntLoc I)) \/ (UsedIntLoc J) & UsedIntLoc (if>0 (a,I,J)) = ({a} \/ (UsedIntLoc I)) \/ (UsedIntLoc J) )

proof end;

theorem Th30: :: SCMBSORT:30

for I being Program of {INT,(INT *)}
for l being Element of NAT holds UsedIntLoc (Directed (I,l)) = UsedIntLoc I

proof end;

theorem Th31: :: SCMBSORT:31

for a being Int-Location
for I being Program of {INT,(INT *)} holds UsedIntLoc (Times (a,I)) = (UsedIntLoc I) \/ {a,(intloc 0)}

proof end;

theorem :: SCMBSORT:32

canceled;

theorem :: SCMBSORT:33

canceled;

theorem :: SCMBSORT:34

canceled;

theorem :: SCMBSORT:35

canceled;

theorem Th36: :: SCMBSORT:36

for I being Program of {INT,(INT *)}
for l being Element of NAT holds UsedInt*Loc (Directed (I,l)) = UsedInt*Loc I

proof end;

theorem Th37: :: SCMBSORT:37

for a being Int-Location
for I being Program of {INT,(INT *)} holds UsedInt*Loc (Times (a,I)) = UsedInt*Loc I

proof end;

definition

let f be FinSeq-Location ;
let t be FinSequence of INT ;
:: original: .-->
redefine func f .--> t -> FinPartState of SCM+FSA;
coherence
f .--> t is FinPartState of SCM+FSA

proof end;

end;

theorem :: SCMBSORT:38

canceled;

theorem :: SCMBSORT:39

canceled;

theorem Th40: :: SCMBSORT:40

dom (Initialize ((intloc 0) .--> 1)) = {(intloc 0),(IC )}

proof end;

theorem Th41: :: SCMBSORT:41

for I being Program of {INT,(INT *)} holds dom (Initialized I) = (dom I) \/ {(intloc 0),(IC )}

proof end;

theorem Th42: :: SCMBSORT:42

for w being FinSequence of INT
for f being FinSeq-Location
for I being Program of {INT,(INT *)} holds dom ((Initialized I) +* (f .--> w)) = (dom I) \/ {(intloc 0),(IC ),f}

proof end;

theorem :: SCMBSORT:43

canceled;

theorem Th44: :: SCMBSORT:44

for a being Int-Location
for I being Program of {INT,(INT *)} holds card (Times (a,I)) = (card I) + 12

proof end;

theorem Th45: :: SCMBSORT:45

for i1, i2, i3 being Instruction of SCM+FSA holds card ((i1 ';' i2) ';' i3) = 6

proof end;

theorem Th46: :: SCMBSORT:46

for t being FinSequence of INT
for f being FinSeq-Location
for I being Program of {INT,(INT *)} holds dom (Initialized I) misses dom (f .--> t)

proof end;

theorem Th47: :: SCMBSORT:47

for w being FinSequence of INT
for f being FinSeq-Location
for I being Program of {INT,(INT *)} holds (Initialized I) +* (f .--> w) is 0 -started

proof end;

theorem Th48: :: SCMBSORT:48

for I, J being Program of {INT,(INT *)}
for k being Element of 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 :: SCMBSORT:49

canceled;

theorem Th50: :: SCMBSORT:50

for I, J being Program of {INT,(INT *)}
for k being Element of NAT
for i being Instruction of SCM+FSA st ( for n being Element of NAT holds IncAddr (i,n) = i ) & i <> halt SCM+FSA & k = card I holds
( ((I ';' i) ';' J) . k = i & ((I ';' i) ';' J) . (k + 1) = goto ((card I) + 2) )

proof end;

theorem Th51: :: SCMBSORT:51

for a, b being Int-Location
for I, J being Program of {INT,(INT *)}
for k being Element of NAT st k = card I holds
( ((I ';' (a := b)) ';' J) . k = a := b & ((I ';' (a := b)) ';' J) . (k + 1) = goto ((card I) + 2) )

proof end;

theorem Th52: :: SCMBSORT:52

for f being FinSeq-Location
for a being Int-Location
for I, J being Program of {INT,(INT *)}
for k being Element of NAT st k = card I holds
( ((I ';' (a :=len f)) ';' J) . k = a :=len f & ((I ';' (a :=len f)) ';' J) . (k + 1) = goto ((card I) + 2) )

proof end;

theorem Th53: :: SCMBSORT:53

for w being FinSequence of INT
for f being FinSeq-Location
for s being State of SCM+FSA
for I being Program of {INT,(INT *)} holds ProgramPart ((Initialized I) +* (f .--> w)) = I

proof end;

theorem Th54: :: SCMBSORT:54

for w being FinSequence of INT
for f being FinSeq-Location
for s being State of SCM+FSA
for I being Program of {INT,(INT *)} st NPP ((Initialized I) +* (f .--> w)) c= s holds
( s . f = w & s . (intloc 0) = 1 )

proof end;

theorem Th55: :: SCMBSORT:55

for f being FinSeq-Location
for a being Int-Location
for s being State of SCM+FSA holds {a,(IC ),f} c= dom s

proof end;

theorem Th56: :: SCMBSORT:56

for p being Program of {INT,(INT *)}
for s being State of SCM+FSA holds (UsedInt*Loc p) \/ (UsedIntLoc p) c= dom s

proof end;

theorem Th57: :: SCMBSORT:57

for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of {INT,(INT *)}
for f being FinSeq-Location holds (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) . 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: intloc 0 <> intloc 2
by SCMFSA_2:128;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

definition

let f be FinSeq-Location ;
func bubble-sort f -> Program of {INT,(INT *)} 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 {INT,(INT *)};
;

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 {INT,(INT *)} equals :: SCMBSORT:def 2
bubble-sort (fsloc 0);
coherence
bubble-sort (fsloc 0) is Program of {INT,(INT *)} ;

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 Th58: :: SCMBSORT:58

for f being FinSeq-Location holds UsedIntLoc (bubble-sort f) = {(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}

proof end;

theorem Th59: :: SCMBSORT:59

for f being FinSeq-Location holds UsedInt*Loc (bubble-sort f) = {f}

proof end;

definition

func Sorting-Function -> PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) means :Def3: :: SCMBSORT:def 3
for p, q being FinPartState of SCM+FSA holds
( [p,q] in it iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) );
existence
ex b₁ being PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) st
for p, q being FinPartState of SCM+FSA holds
( [p,q] in b₁ iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) st ( for p, q being FinPartState of SCM+FSA holds
( [p,q] in b₁ iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) ) ) & ( for p, q being FinPartState of SCM+FSA holds
( [p,q] in b₂ iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Sorting-Function SCMBSORT:def 3 :
for b₁ being PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) holds
( b₁ = Sorting-Function iff for p, q being FinPartState of SCM+FSA holds
( [p,q] in b₁ iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) ) );

theorem Th60: :: SCMBSORT:60

for p being set holds
( p in dom Sorting-Function iff ex t being FinSequence of INT st p = (fsloc 0) .--> t )

proof end;

theorem Th61: :: SCMBSORT:61

for t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & Sorting-Function . ((fsloc 0) .--> t) = (fsloc 0) .--> u )

proof end;

theorem Th62: :: SCMBSORT:62

for f being FinSeq-Location holds card (bubble-sort f) = 63

proof end;

theorem Th63: :: SCMBSORT:63

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT 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

proof end;

Lm20: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st Bubble-Sort-Algorithm c= P holds
( 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 )

proof end;

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

proof end;

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)

proof end;

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 & 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 )

proof end;

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)

proof end;

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)

proof end;

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 & 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 )

proof end;

theorem :: SCMBSORT:64

( bubble-sort (fsloc 0) is keepInt0_1 & bubble-sort (fsloc 0) is InitHalting ) by Lm26;

Lm27: for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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)))) ) & ( 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) ) )

proof end;

Lm28: for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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))

proof end;

Lm29: for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA st s . (intloc (2 + 1)) <= len (s . (fsloc 0)) & 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 & 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 & ( (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) ) & ( (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))) ) & ( (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) ) & ( for k being set st k <> (s . (intloc (2 + 1))) - 1 & k <> s . (intloc (2 + 1)) & 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 ) & 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) & 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))) & x1 >= x2 ) )

proof end;

Lm30: for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 . (fsloc 0)) holds
ex k being Element of 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 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))) )

proof end;

Lm31: for k being Element of NAT
for t being State of SCM+FSA
for q being the Instructions of SCM+FSA -valued ManySortedSet of NAT st k = t . (intloc (1 + 1)) & k < t . (intloc (2 + 1)) & 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 & ( for m being Element of NAT st ( ( m < (t . (intloc (2 + 1))) - k & m >= 1 ) or ( m > t . (intloc (2 + 1)) & 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 ) & ( for m being Element of 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 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) & 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 & x1 >= x2 ) ) & ( for i being Element of NAT st i >= (t . (intloc (2 + 1))) - k & i <= t . (intloc (2 + 1)) holds
ex n being Element of 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 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 ) ) )

proof end;

Lm32: for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 & (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)) & (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) )

proof end;

Lm33: for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 & ( for i, j being Element of NAT st i >= 1 & j <= len (s . (fsloc 0)) & 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 & 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 ) )

proof end;

theorem Th65: :: SCMBSORT:65

for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA holds
( s . (fsloc 0),(IExec ((bubble-sort (fsloc 0)),p,s)) . (fsloc 0) are_fiberwise_equipotent & ( for i, j being Element of NAT st i >= 1 & j <= len (s . (fsloc 0)) & i < j holds
for x1, x2 being Integer st x1 = ((IExec ((bubble-sort (fsloc 0)),p,s)) . (fsloc 0)) . i & x2 = ((IExec ((bubble-sort (fsloc 0)),p,s)) . (fsloc 0)) . j holds
x1 >= x2 ) )

proof end;

theorem Th66: :: SCMBSORT:66

for i being Element of NAT
for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st Bubble-Sort-Algorithm c= P holds
for w being FinSequence of INT st NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s holds
IC (Comput (P,s,i)) in dom Bubble-Sort-Algorithm

proof end;

theorem Th67: :: SCMBSORT:67

for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for t being FinSequence of INT st (Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> 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)) . (fsloc 0) = u )

proof end;

theorem Th68: :: SCMBSORT:68

for w being FinSequence of INT holds (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) is autonomic

proof end;

registration

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

end;

theorem :: SCMBSORT:69

Bubble-Sort-Algorithm , Initialized Bubble-Sort-Algorithm computes Sorting-Function

proof end;