:: SCMBSORT semantic presentation

theorem :: SCMBSORT:1

canceled;

theorem :: SCMBSORT:2

canceled;

theorem Th3: :: SCMBSORT:3

for I being Macro-Instruction
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 Th4: :: SCMBSORT:4

for f being Function
for a, b, n, m being set holds ((f +* (a .--> b)) +* (m .--> n)) . m = n

proof end;

theorem Th5: :: SCMBSORT:5

for f being Function
for n, m being set holds ((f +* (n .--> m)) +* (m .--> n)) . n = m

proof end;

theorem Th6: :: SCMBSORT:6

for f being Function
for a, b, n, m, x being set st x <> m & x <> a holds
((f +* (a .--> b)) +* (m .--> n)) . x = f . x

proof end;

theorem Th7: :: SCMBSORT:7

for f, g being Function
for m, n being set st f . m = g . n & f . n = g . m & m in dom f & n in dom f & dom f = dom g & ( for k being set st k <> m & k <> n & k in dom f holds
f . k = g . k ) holds
f,g are_fiberwise_equipotent

proof end;

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 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 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 SCM+FSA-Stop ,s) . a = s . a & (IExec SCM+FSA-Stop ,s) . f = s . f )

proof end;

theorem Th13: :: SCMBSORT:13

for n being natural number holds
( not n <= 10 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 or n = 7 or n = 8 or n = 9 or n = 10 )

proof end;

theorem Th14: :: SCMBSORT:14

for n being natural number holds
( not n <= 12 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 or n = 7 or n = 8 or n = 9 or n = 10 or n = 11 or n = 12 )

proof end;

theorem Th15: :: SCMBSORT:15

for f, g being Function
for X being set st dom f = dom g & ( for x being set st x in X holds
f . x = g . x ) holds
f | X = g | X

proof end;

theorem Th16: :: SCMBSORT:16

for p being programmed FinPartState 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 programmed FinPartState 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 programmed FinPartState 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

proof end;

theorem Th20: :: SCMBSORT:20

for p being programmed FinPartState 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

proof end;

theorem Th22: :: SCMBSORT:22

for i being Nat
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of N
for p being programmed FinPartState of S
for s1, s2 being State of S st p c= s1 & p c= s2 holds
((Computation s1) . i) | (dom p) = ((Computation s2) . i) | (dom p)

proof end;

theorem Th23: :: SCMBSORT:23

for t being FinPartState of SCM+FSA
for p being Macro-Instruction
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 Nat
for t being FinPartState of SCM+FSA
for p being Macro-Instruction
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 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 Nat
for p being Macro-Instruction
for s1, s2 being State of SCM+FSA st k <= i & p c= s1 & p c= s2 & ( for j being 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 Macro-Instruction
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 Macro-Instruction
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 Macro-Instruction holds UsedIntLoc (Times a,I) = (UsedIntLoc I) \/ {a,(intloc 0)}

proof end;

theorem Th32: :: SCMBSORT:32

for x1, x2, x3 being set holds {x2,x1} \/ {x3,x1} = {x1,x2,x3}

proof end;

theorem :: SCMBSORT:33

canceled;

theorem :: SCMBSORT:34

canceled;

theorem :: SCMBSORT:35

for I, J being Macro-Instruction
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 Macro-Instruction
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 Macro-Instruction 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

proof end;

end;

theorem Th38: :: SCMBSORT:38

for t being FinSequence of INT holds t is FinSequence of REAL

proof end;

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 Macro-Instruction 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 Macro-Instruction 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 Macro-Instruction 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 Macro-Instruction 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 Macro-Instruction holds (Initialized I) +* (f .--> w) starts_at insloc 0

proof end;

theorem Th48: :: SCMBSORT:48

for I, J being Macro-Instruction
for k being 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 Th49: :: 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 Macro-Instruction
for k being Nat
for i being Instruction of SCM+FSA st ( for n being 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 Macro-Instruction
for k being 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 Macro-Instruction
for k being 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 Macro-Instruction 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 Macro-Instruction 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 Macro-Instruction
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 Macro-Instruction
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;

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 -> Macro-Instruction means :Def1: :: SCMBSORT:def 1
it = (((((((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))),SCM+FSA-Stop )))));
correctness ;

end;

:: deftheorem Def1 defines bubble-sort SCMBSORT:def 1 :

definition

func Bubble-Sort-Algorithm -> Macro-Instruction means :Def2: :: SCMBSORT:def 2
it = bubble-sort (fsloc 0);
correctness ;

end;

:: deftheorem Def2 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)),(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 = SCM+FSA-Stop ;

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

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

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

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

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

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Sorting-Function SCMBSORT:def 3 :

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 Nat st k < 63 holds
insloc k in dom (bubble-sort f)

proof end;

Lm1: 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;

proof end;

Lm3: ((((((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)))),SCM+FSA-Stop ) does_not_destroy intloc (1 + 1)

proof end;

Lm4: 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)))),SCM+FSA-Stop )) is good InitHalting Macro-Instruction

proof end;

Lm5: ((((((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)))),SCM+FSA-Stop ) does_not_destroy intloc (0 + 1)

proof end;

Lm6: ((((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)))),SCM+FSA-Stop ))) 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)))),SCM+FSA-Stop ))) is good InitHalting Macro-Instruction

proof end;

Lm8: 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)))),SCM+FSA-Stop )))) is good InitHalting Macro-Instruction

proof end;

theorem Th64: :: SCMBSORT:64

( bubble-sort (fsloc 0) is keepInt0_1 & bubble-sort (fsloc 0) is InitHalting )

proof end;

Lm9: 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)))),SCM+FSA-Stop ),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)))),SCM+FSA-Stop ),s) . (fsloc 0) = s . (fsloc 0) ) )

proof end;

Lm10: 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)))),SCM+FSA-Stop ),s) . (intloc (2 + 1)) = s . (intloc (2 + 1))

proof end;

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

proof end;

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

proof end;

Lm13: for k being 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)))),SCM+FSA-Stop ))),t) . (fsloc 0) 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 . (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)))),SCM+FSA-Stop ))),t) . (fsloc 0)) . 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 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)))),SCM+FSA-Stop ))),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)))),SCM+FSA-Stop ))),t) . (fsloc 0)) . 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 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)))),SCM+FSA-Stop ))),t) . (fsloc 0)) . i = (t . (fsloc 0)) . n ) ) )

proof end;

Lm14: 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;

Lm15: 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)))),SCM+FSA-Stop ))))),s) . (fsloc 0) are_fiberwise_equipotent & ( for i, j being 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)))),SCM+FSA-Stop ))))),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)))),SCM+FSA-Stop ))))),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 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 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;