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

theorem :: SCMBSORT:1

canceled;

theorem :: SCMBSORT:2

canceled;

theorem Th3: :: SCMBSORT:3

for I being Program of SCM+FSA
for a, b being Int-Location st I does_not_destroy b & a <> b holds
Times a,I does_not_destroy 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),(Initialize 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),(Initialize s)) . (intloc (n + 1)) = s . (intloc (n + 1))

proof end;

theorem Th12: :: SCMBSORT:12

for s being State of SCM+FSA
for f being FinSeq-Location
for a being read-write Int-Location holds
( (IExec (Stop SCM+FSA ),s) . a = s . a & (IExec (Stop SCM+FSA ),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 Instruction-Location of SCM+FSA 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 SCM+FSA
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 i, k being Element of NAT
for t being FinPartState of SCM+FSA
for p being Program of SCM+FSA
for s1, s2 being State of SCM+FSA st k <= i & p c= s1 & p c= s2 & dom t c= Int-Locations \/ FinSeq-Locations & ( for j being Element of NAT holds
( IC (Computation s1,j) in dom p & IC (Computation s2,j) in dom p ) ) & (Computation s1,k) . (IC SCM+FSA ) = (Computation s2,k) . (IC SCM+FSA ) & (Computation s1,k) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Computation s2,k) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) holds
( (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Computation s2,i) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) )

proof end;

theorem Th26: :: SCMBSORT:26

for i, k being Element of NAT
for p being Program of SCM+FSA
for s1, s2 being State of SCM+FSA st k <= i & p c= s1 & p c= s2 & ( for j being Element of NAT holds
( IC (Computation s1,j) in dom p & IC (Computation s2,j) in dom p ) ) & (Computation s1,k) . (IC SCM+FSA ) = (Computation s2,k) . (IC SCM+FSA ) & (Computation s1,k) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Computation s2,k) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) holds
( (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Computation 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 SCM+FSA
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 SCM+FSA
for l being Instruction-Location of SCM+FSA holds UsedIntLoc (Directed I,l) = UsedIntLoc I

proof end;

theorem Th31: :: SCMBSORT:31

for a being Int-Location
for I being Program of SCM+FSA 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

for I, J being Program of SCM+FSA
for a being Int-Location holds
( UsedInt*Loc (if=0 a,I,J) = (UsedInt*Loc I) \/ (UsedInt*Loc J) & UsedInt*Loc (if>0 a,I,J) = (UsedInt*Loc I) \/ (UsedInt*Loc J) ) by SCMFSA9A:14, SCMFSA9A:16;

theorem Th36: :: SCMBSORT:36

for I being Program of SCM+FSA
for l being Instruction-Location of SCM+FSA 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 SCM+FSA 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

for t being FinSequence of INT holds t is FinSequence of REAL by FINSEQ_3:126;

theorem Th39: :: SCMBSORT:39

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

proof end;

theorem Th40: :: SCMBSORT:40

dom (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) = {(intloc 0 ),(IC SCM+FSA )}

proof end;

theorem Th41: :: SCMBSORT:41

for I being Program of SCM+FSA holds dom (Initialized I) = (dom I) \/ {(intloc 0 ),(IC SCM+FSA )}

proof end;

theorem Th42: :: SCMBSORT:42

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

proof end;

theorem :: SCMBSORT:43

for l being Instruction-Location of SCM+FSA holds IC SCM+FSA <> l

proof end;

theorem Th44: :: SCMBSORT:44

for a being Int-Location
for I being Program of SCM+FSA 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 SCM+FSA 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 SCM+FSA holds (Initialized I) +* (f .--> w) starts_at 0

proof end;

theorem Th48: :: SCMBSORT:48

for I, J being Program of SCM+FSA
for k being Element of NAT
for i being Instruction of SCM+FSA st k < card J & i = J . (insloc k) holds
(I ';' J) . (insloc ((card I) + k)) = IncAddr i,(card I)

proof end;

theorem :: SCMBSORT:49

for ic being Instruction of SCM+FSA
for f being FinSeq-Location
for a, b being Int-Location
for la being Instruction-Location of SCM+FSA st ( ic = a := b or ic = AddTo a,b or ic = SubFrom a,b or ic = MultBy a,b or ic = Divide a,b or ic = goto la or ic = a =0_goto la or ic = a >0_goto la or ic = b := f,a or ic = f,a := b or ic = a :=len f or ic = f :=<0,...,0> a ) holds
ic <> halt SCM+FSA by SCMFSA_2:42, SCMFSA_2:43, SCMFSA_2:44, SCMFSA_2:45, SCMFSA_2:46, SCMFSA_2:47, SCMFSA_2:48, SCMFSA_2:49, SCMFSA_2:50, SCMFSA_2:51, SCMFSA_2:52, SCMFSA_2:53, SCMFSA_2:124;

theorem Th50: :: SCMBSORT:50

for I, J being Program of SCM+FSA
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) . (insloc k) = i & ((I ';' i) ';' J) . (insloc (k + 1)) = goto (insloc ((card I) + 2)) )

proof end;

theorem Th51: :: SCMBSORT:51

for a, b being Int-Location
for I, J being Program of SCM+FSA
for k being Element of NAT st k = card I holds
( ((I ';' (a := b)) ';' J) . (insloc k) = a := b & ((I ';' (a := b)) ';' J) . (insloc (k + 1)) = goto (insloc ((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 SCM+FSA
for k being Element of NAT st k = card I holds
( ((I ';' (a :=len f)) ';' J) . (insloc k) = a :=len f & ((I ';' (a :=len f)) ';' J) . (insloc (k + 1)) = goto (insloc ((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 SCM+FSA st (Initialized I) +* (f .--> w) c= s holds
I c= s

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 SCM+FSA st (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 SCM+FSA ),f} c= dom s

proof end;

theorem Th56: :: SCMBSORT:56

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

proof end;

theorem Th57: :: SCMBSORT:57

for s being State of SCM+FSA
for I being Program of SCM+FSA
for f being FinSeq-Location holds (Result (s +* (Initialized I))) . f = (IExec I,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 1 & intloc 0 <> intloc 2 & intloc 0 <> intloc 3 & intloc 0 <> intloc 4 & intloc 0 <> intloc 5 & intloc 0 <> intloc 6 & intloc 1 <> intloc 2 & intloc 1 <> intloc 3 & intloc 1 <> intloc 4 & intloc 1 <> intloc 5 & intloc 1 <> intloc 6 & intloc 2 <> intloc 3 & intloc 2 <> intloc 4 & intloc 2 <> intloc 5 & intloc 2 <> intloc 6 & intloc 3 <> intloc 4 & intloc 3 <> intloc 5 & intloc 3 <> intloc 6 & intloc 4 <> intloc 5 & intloc 4 <> intloc 6 & intloc 5 <> intloc 6 )
by AMI_3:52;

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 SCM+FSA 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 SCM+FSA ;
;

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 SCM+FSA equals :: SCMBSORT:def 2
bubble-sort (fsloc 0 );
coherence
bubble-sort (fsloc 0 ) is Program of SCM+FSA ;

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 f being FinSeq-Location
for k being Element of NAT st k < 63 holds
insloc k in dom (bubble-sort f)

proof end;

Lm2: for s being State of SCM+FSA st Bubble-Sort-Algorithm c= s holds
( s . (insloc 0 ) = (intloc 2) := (intloc 0 ) & s . (insloc 1) = goto (insloc 2) & s . (insloc 2) = (intloc 3) := (intloc 0 ) & s . (insloc 3) = goto (insloc 4) & s . (insloc 4) = (intloc 4) := (intloc 0 ) & s . (insloc 5) = goto (insloc 6) & s . (insloc 6) = (intloc 5) := (intloc 0 ) & s . (insloc 7) = goto (insloc 8) & s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )

proof end;

Lm3: for s being State of SCM+FSA st Bubble-Sort-Algorithm c= s & s starts_at 0 holds
( (Computation s,1) . (IC SCM+FSA ) = insloc 1 & (Computation s,1) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,1) . (fsloc 0 ) = s . (fsloc 0 ) & (Computation s,2) . (IC SCM+FSA ) = insloc 2 & (Computation s,2) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,2) . (fsloc 0 ) = s . (fsloc 0 ) & (Computation s,3) . (IC SCM+FSA ) = insloc 3 & (Computation s,3) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,3) . (fsloc 0 ) = s . (fsloc 0 ) & (Computation s,4) . (IC SCM+FSA ) = insloc 4 & (Computation s,4) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,4) . (fsloc 0 ) = s . (fsloc 0 ) & (Computation s,5) . (IC SCM+FSA ) = insloc 5 & (Computation s,5) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,5) . (fsloc 0 ) = s . (fsloc 0 ) & (Computation s,6) . (IC SCM+FSA ) = insloc 6 & (Computation s,6) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,6) . (fsloc 0 ) = s . (fsloc 0 ) & (Computation s,7) . (IC SCM+FSA ) = insloc 7 & (Computation s,7) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,7) . (fsloc 0 ) = s . (fsloc 0 ) & (Computation s,8) . (IC SCM+FSA ) = insloc 8 & (Computation s,8) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,8) . (fsloc 0 ) = s . (fsloc 0 ) & (Computation s,9) . (IC SCM+FSA ) = insloc 9 & (Computation s,9) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,9) . (fsloc 0 ) = s . (fsloc 0 ) & (Computation s,10) . (IC SCM+FSA ) = insloc 10 & (Computation s,10) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,10) . (fsloc 0 ) = s . (fsloc 0 ) & (Computation s,11) . (IC SCM+FSA ) = insloc 11 & (Computation s,11) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,11) . (fsloc 0 ) = s . (fsloc 0 ) & (Computation s,11) . (intloc 1) = len (s . (fsloc 0 )) & (Computation s,11) . (intloc 2) = s . (intloc 0 ) & (Computation s,11) . (intloc 3) = s . (intloc 0 ) & (Computation s,11) . (intloc 4) = s . (intloc 0 ) & (Computation s,11) . (intloc 5) = s . (intloc 0 ) & (Computation s,11) . (intloc 6) = s . (intloc 0 ) )

proof end;

Lm4: ((((((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 )) does_not_destroy intloc (1 + 1)

proof end;

Lm5: 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 InitHalting Program of SCM+FSA

proof end;

Lm6: ((((((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 )) does_not_destroy intloc (0 + 1)

proof end;

Lm7: ((((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 )))) does_not_destroy intloc (0 + 1)

proof end;

Lm8: ((((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 InitHalting Program of SCM+FSA
by Lm5;

Lm9: 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 InitHalting Program of SCM+FSA

proof end;

theorem Th64: :: SCMBSORT:64

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

Lm10: 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 )),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 )),s) . (fsloc 0 ) = s . (fsloc 0 ) ) )

proof end;

Lm11: 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 )),s) . (intloc (2 + 1)) = s . (intloc (2 + 1))

proof end;

Lm12: 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 ))),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 ))),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 ))),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 ))),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 ))),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 ))),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 ))),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 ))),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 ))),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 ))),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 ))),s) . (fsloc 0 )) . (s . (intloc (2 + 1))) & x1 >= x2 ) )

proof end;

Lm13: 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 )))),s) . (fsloc 0 )) . k = (s . (fsloc 0 )) . (s . (intloc (2 + 1))) )

proof end;

Lm14: for k being Element of NAT
for t being State of SCM+FSA 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 )))),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 )))),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 )))),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 )))),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 )))),t) . (fsloc 0 )) . i = (t . (fsloc 0 )) . n ) ) )

proof end;

Lm15: 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 ))),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 ))),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 ))),s) . (fsloc 0 ) = s . (fsloc 0 ) )

proof end;

Lm16: 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 )))))),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 )))))),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 )))))),s) . (fsloc 0 )) . j holds
x1 >= x2 ) )

proof end;

theorem Th65: :: SCMBSORT:65

for s being State of SCM+FSA holds
( s . (fsloc 0 ),(IExec (bubble-sort (fsloc 0 )),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 )),s) . (fsloc 0 )) . i & x2 = ((IExec (bubble-sort (fsloc 0 )),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 w being FinSequence of INT st (Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s holds
IC (Computation s,i) in dom Bubble-Sort-Algorithm

proof end;

theorem Th67: :: SCMBSORT:67

for s being State of SCM+FSA
for t being FinSequence of INT st (Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0 ) .--> t) c= s holds
ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result 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;

theorem :: SCMBSORT:69

Initialized Bubble-Sort-Algorithm computes Sorting-Function

proof end;