:: SCMBSORT semantic presentation

theorem Th1: :: SCMBSORT:1

canceled;

theorem Th2: :: SCMBSORT:2

canceled;

theorem Th3: :: SCMBSORT:3

for b₁ being Macro-Instruction
for b₂, b₃ being Int-Location st b₁ does_not_destroy b₃ & b₂ <> b₃ holds
Times b₂,b₁ does_not_destroy b₃

proof end;

theorem Th4: :: SCMBSORT:4

for b₁ being Function
for b₂, b₃, b₄, b₅ being set holds ((b₁ +* (b₂ .--> b₃)) +* (b₅ .--> b₄)) . b₅ = b₄

proof end;

theorem Th5: :: SCMBSORT:5

for b₁ being Function
for b₂, b₃ being set holds ((b₁ +* (b₂ .--> b₃)) +* (b₃ .--> b₂)) . b₂ = b₃

proof end;

theorem Th6: :: SCMBSORT:6

for b₁ being Function
for b₂, b₃, b₄, b₅, b₆ being set st b₆ <> b₅ & b₆ <> b₂ holds
((b₁ +* (b₂ .--> b₃)) +* (b₅ .--> b₄)) . b₆ = b₁ . b₆

proof end;

theorem Th7: :: SCMBSORT:7

for b₁, b₂ being Function
for b₃, b₄ being set st b₁ . b₃ = b₂ . b₄ & b₁ . b₄ = b₂ . b₃ & b₃ in dom b₁ & b₄ in dom b₁ & dom b₁ = dom b₂ & ( for b₅ being set st b₅ <> b₃ & b₅ <> b₄ & b₅ in dom b₁ holds
b₁ . b₅ = b₂ . b₅ ) holds
b₁,b₂ are_fiberwise_equipotent

proof end;

theorem Th8: :: SCMBSORT:8

for b₁ being State of SCM+FSA
for b₂ being FinSeq-Location
for b₃, b₄ being Int-Location holds (Exec (b₄ := b₂,b₃),b₁) . b₄ = (b₁ . b₂) /. (abs (b₁ . b₃))

proof end;

theorem Th9: :: SCMBSORT:9

for b₁ being State of SCM+FSA
for b₂ being FinSeq-Location
for b₃, b₄ being Int-Location holds (Exec (b₂,b₃ := b₄),b₁) . b₂ = (b₁ . b₂) +* (abs (b₁ . b₃)),(b₁ . b₄)

proof end;

theorem Th10: :: SCMBSORT:10

for b₁ being State of SCM+FSA
for b₂ being FinSeq-Location
for b₃, b₄ being Nat
for b₅ being Int-Location st b₃ <> b₄ + 1 holds
(Exec ((intloc b₃) := b₂,b₅),(Initialize b₁)) . (intloc (b₄ + 1)) = b₁ . (intloc (b₄ + 1))

proof end;

theorem Th11: :: SCMBSORT:11

for b₁ being State of SCM+FSA
for b₂, b₃ being Nat
for b₄ being Int-Location st b₂ <> b₃ + 1 holds
(Exec ((intloc b₂) := b₄),(Initialize b₁)) . (intloc (b₃ + 1)) = b₁ . (intloc (b₃ + 1))

proof end;

theorem Th12: :: SCMBSORT:12

for b₁ being State of SCM+FSA
for b₂ being FinSeq-Location
for b₃ being read-write Int-Location holds
( (IExec SCM+FSA-Stop ,b₁) . b₃ = b₁ . b₃ & (IExec SCM+FSA-Stop ,b₁) . b₂ = b₁ . b₂ )

proof end;

theorem Th13: :: SCMBSORT:13

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

proof end;

theorem Th14: :: SCMBSORT:14

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

proof end;

theorem Th15: :: SCMBSORT:15

for b₁, b₂ being Function
for b₃ being set st dom b₁ = dom b₂ & ( for b₄ being set st b₄ in b₃ holds
b₁ . b₄ = b₂ . b₄ ) holds
b₁ | b₃ = b₂ | b₃

proof end;

theorem Th16: :: SCMBSORT:16

for b₁ being programmed FinPartState of SCM+FSA
for b₂ being Instruction of SCM+FSA
for b₃, b₄ being Int-Location st b₂ in rng b₁ & ( b₂ = b₃ := b₄ or b₂ = AddTo b₃,b₄ or b₂ = SubFrom b₃,b₄ or b₂ = MultBy b₃,b₄ or b₂ = Divide b₃,b₄ ) holds
( b₃ in UsedIntLoc b₁ & b₄ in UsedIntLoc b₁ )

proof end;

theorem Th17: :: SCMBSORT:17

for b₁ being programmed FinPartState of SCM+FSA
for b₂ being Instruction of SCM+FSA
for b₃ being Int-Location
for b₄ being Instruction-Location of SCM+FSA st b₂ in rng b₁ & ( b₂ = b₃ =0_goto b₄ or b₂ = b₃ >0_goto b₄ ) holds
b₃ in UsedIntLoc b₁

proof end;

theorem Th18: :: SCMBSORT:18

for b₁ being programmed FinPartState of SCM+FSA
for b₂ being Instruction of SCM+FSA
for b₃ being FinSeq-Location
for b₄, b₅ being Int-Location st b₂ in rng b₁ & ( b₂ = b₄ := b₃,b₅ or b₂ = b₃,b₅ := b₄ ) holds
( b₅ in UsedIntLoc b₁ & b₄ in UsedIntLoc b₁ )

proof end;

theorem Th19: :: SCMBSORT:19

proof end;

theorem Th20: :: SCMBSORT:20

for b₁ being programmed FinPartState of SCM+FSA
for b₂ being Instruction of SCM+FSA
for b₃ being FinSeq-Location
for b₄ being Int-Location st b₂ in rng b₁ & ( b₂ = b₄ :=len b₃ or b₂ = b₃ :=<0,...,0> b₄ ) holds
b₄ in UsedIntLoc b₁

proof end;

theorem Th21: :: SCMBSORT:21

proof end;

theorem Th22: :: SCMBSORT:22

for b₁ being Nat
for b₂ being with_non-empty_elements set
for b₃ being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of b₂
for b₄ being programmed FinPartState of b₃
for b₅, b₆ being State of b₃ st b₄ c= b₅ & b₄ c= b₆ holds
((Computation b₅) . b₁) | (dom b₄) = ((Computation b₆) . b₁) | (dom b₄)

proof end;

theorem Th23: :: SCMBSORT:23

for b₁ being FinPartState of SCM+FSA
for b₂ being Macro-Instruction
for b₃ being set st dom b₁ c= Int-Locations \/ FinSeq-Locations & b₃ in ((dom b₁) \/ (UsedInt*Loc b₂)) \/ (UsedIntLoc b₂) & b₃ is not Int-Location holds
b₃ is FinSeq-Location

proof end;

theorem Th24: :: SCMBSORT:24

canceled;

theorem Th25: :: SCMBSORT:25

for b₁, b₂ being Nat
for b₃ being FinPartState of SCM+FSA
for b₄ being Macro-Instruction
for b₅, b₆ being State of SCM+FSA st b₂ <= b₁ & b₄ c= b₅ & b₄ c= b₆ & dom b₃ c= Int-Locations \/ FinSeq-Locations & ( for b₇ being Nat holds
( IC ((Computation b₅) . b₇) in dom b₄ & IC ((Computation b₆) . b₇) in dom b₄ ) ) & ((Computation b₅) . b₂) . (IC SCM+FSA ) = ((Computation b₆) . b₂) . (IC SCM+FSA ) & ((Computation b₅) . b₂) | (((dom b₃) \/ (UsedInt*Loc b₄)) \/ (UsedIntLoc b₄)) = ((Computation b₆) . b₂) | (((dom b₃) \/ (UsedInt*Loc b₄)) \/ (UsedIntLoc b₄)) holds
( ((Computation b₅) . b₁) . (IC SCM+FSA ) = ((Computation b₆) . b₁) . (IC SCM+FSA ) & ((Computation b₅) . b₁) | (((dom b₃) \/ (UsedInt*Loc b₄)) \/ (UsedIntLoc b₄)) = ((Computation b₆) . b₁) | (((dom b₃) \/ (UsedInt*Loc b₄)) \/ (UsedIntLoc b₄)) )

proof end;

theorem Th26: :: SCMBSORT:26

for b₁, b₂ being Nat
for b₃ being Macro-Instruction
for b₄, b₅ being State of SCM+FSA st b₂ <= b₁ & b₃ c= b₄ & b₃ c= b₅ & ( for b₆ being Nat holds
( IC ((Computation b₄) . b₆) in dom b₃ & IC ((Computation b₅) . b₆) in dom b₃ ) ) & ((Computation b₄) . b₂) . (IC SCM+FSA ) = ((Computation b₅) . b₂) . (IC SCM+FSA ) & ((Computation b₄) . b₂) | ((UsedInt*Loc b₃) \/ (UsedIntLoc b₃)) = ((Computation b₅) . b₂) | ((UsedInt*Loc b₃) \/ (UsedIntLoc b₃)) holds
( ((Computation b₄) . b₁) . (IC SCM+FSA ) = ((Computation b₅) . b₁) . (IC SCM+FSA ) & ((Computation b₄) . b₁) | ((UsedInt*Loc b₃) \/ (UsedIntLoc b₃)) = ((Computation b₅) . b₁) | ((UsedInt*Loc b₃) \/ (UsedIntLoc b₃)) )

proof end;

theorem Th27: :: SCMBSORT:27

canceled;

theorem Th28: :: SCMBSORT:28

canceled;

theorem Th29: :: SCMBSORT:29

for b₁, b₂ being Macro-Instruction
for b₃ being Int-Location holds
( UsedIntLoc (if=0 b₃,b₁,b₂) = ({b₃} \/ (UsedIntLoc b₁)) \/ (UsedIntLoc b₂) & UsedIntLoc (if>0 b₃,b₁,b₂) = ({b₃} \/ (UsedIntLoc b₁)) \/ (UsedIntLoc b₂) )

proof end;

theorem Th30: :: SCMBSORT:30

for b₁ being Macro-Instruction
for b₂ being Instruction-Location of SCM+FSA holds UsedIntLoc (Directed b₁,b₂) = UsedIntLoc b₁

proof end;

theorem Th31: :: SCMBSORT:31

for b₁ being Int-Location
for b₂ being Macro-Instruction holds UsedIntLoc (Times b₁,b₂) = (UsedIntLoc b₂) \/ {b₁,(intloc 0)}

proof end;

theorem Th32: :: SCMBSORT:32

for b₁, b₂, b₃ being set holds {b₂,b₁} \/ {b₃,b₁} = {b₁,b₂,b₃}

proof end;

theorem Th33: :: SCMBSORT:33

canceled;

theorem Th34: :: SCMBSORT:34

canceled;

theorem Th35: :: SCMBSORT:35

for b₁, b₂ being Macro-Instruction
for b₃ being Int-Location holds
( UsedInt*Loc (if=0 b₃,b₁,b₂) = (UsedInt*Loc b₁) \/ (UsedInt*Loc b₂) & UsedInt*Loc (if>0 b₃,b₁,b₂) = (UsedInt*Loc b₁) \/ (UsedInt*Loc b₂) ) by SCMFSA9A:14, SCMFSA9A:16;

theorem Th36: :: SCMBSORT:36

for b₁ being Macro-Instruction
for b₂ being Instruction-Location of SCM+FSA holds UsedInt*Loc (Directed b₁,b₂) = UsedInt*Loc b₁

proof end;

theorem Th37: :: SCMBSORT:37

for b₁ being Int-Location
for b₂ being Macro-Instruction holds UsedInt*Loc (Times b₁,b₂) = UsedInt*Loc b₂

proof end;

definition

let c₁ be FinSeq-Location ;
let c₂ be FinSequence of INT ;
redefine func .--> as c₁ .--> c₂ -> FinPartState of SCM+FSA ;
coherence

proof end;

end;

theorem Th38: :: SCMBSORT:38

for b₁ being FinSequence of INT holds b₁ is FinSequence of REAL

proof end;

theorem Th39: :: SCMBSORT:39

for b₁ being FinSequence of INT ex b₂ being FinSequence of REAL st
( b₁,b₂ are_fiberwise_equipotent & b₂ is FinSequence of INT & b₂ 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 b₁ being Macro-Instruction holds dom (Initialized b₁) = (dom b₁) \/ {(intloc 0),(IC SCM+FSA )}

proof end;

theorem Th42: :: SCMBSORT:42

for b₁ being FinSequence of INT
for b₂ being FinSeq-Location
for b₃ being Macro-Instruction holds dom ((Initialized b₃) +* (b₂ .--> b₁)) = (dom b₃) \/ {(intloc 0),(IC SCM+FSA ),b₂}

proof end;

theorem Th43: :: SCMBSORT:43

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

proof end;

theorem Th44: :: SCMBSORT:44

for b₁ being Int-Location
for b₂ being Macro-Instruction holds card (Times b₁,b₂) = (card b₂) + 12

proof end;

theorem Th45: :: SCMBSORT:45

for b₁, b₂, b₃ being Instruction of SCM+FSA holds card ((b₁ ';' b₂) ';' b₃) = 6

proof end;

theorem Th46: :: SCMBSORT:46

for b₁ being FinSequence of INT
for b₂ being FinSeq-Location
for b₃ being Macro-Instruction holds dom (Initialized b₃) misses dom (b₂ .--> b₁)

proof end;

theorem Th47: :: SCMBSORT:47

for b₁ being FinSequence of INT
for b₂ being FinSeq-Location
for b₃ being Macro-Instruction holds (Initialized b₃) +* (b₂ .--> b₁) starts_at insloc 0

proof end;

theorem Th48: :: SCMBSORT:48

for b₁, b₂ being Macro-Instruction
for b₃ being Nat
for b₄ being Instruction of SCM+FSA st b₃ < card b₂ & b₄ = b₂ . (insloc b₃) holds
(b₁ ';' b₂) . (insloc ((card b₁) + b₃)) = IncAddr b₄,(card b₁)

proof end;

theorem Th49: :: SCMBSORT:49

for b₁ being Instruction of SCM+FSA
for b₂ being FinSeq-Location
for b₃, b₄ being Int-Location
for b₅ being Instruction-Location of SCM+FSA st ( b₁ = b₃ := b₄ or b₁ = AddTo b₃,b₄ or b₁ = SubFrom b₃,b₄ or b₁ = MultBy b₃,b₄ or b₁ = Divide b₃,b₄ or b₁ = goto b₅ or b₁ = b₃ =0_goto b₅ or b₁ = b₃ >0_goto b₅ or b₁ = b₄ := b₂,b₃ or b₁ = b₂,b₃ := b₄ or b₁ = b₃ :=len b₂ or b₁ = b₂ :=<0,...,0> b₃ ) holds
b₁ <> 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 b₁, b₂ being Macro-Instruction
for b₃ being Nat
for b₄ being Instruction of SCM+FSA st ( for b₅ being Nat holds IncAddr b₄,b₅ = b₄ ) & b₄ <> halt SCM+FSA & b₃ = card b₁ holds
( ((b₁ ';' b₄) ';' b₂) . (insloc b₃) = b₄ & ((b₁ ';' b₄) ';' b₂) . (insloc (b₃ + 1)) = goto (insloc ((card b₁) + 2)) )

proof end;

theorem Th51: :: SCMBSORT:51

for b₁, b₂ being Int-Location
for b₃, b₄ being Macro-Instruction
for b₅ being Nat st b₅ = card b₃ holds
( ((b₃ ';' (b₁ := b₂)) ';' b₄) . (insloc b₅) = b₁ := b₂ & ((b₃ ';' (b₁ := b₂)) ';' b₄) . (insloc (b₅ + 1)) = goto (insloc ((card b₃) + 2)) )

proof end;

theorem Th52: :: SCMBSORT:52

for b₁ being FinSeq-Location
for b₂ being Int-Location
for b₃, b₄ being Macro-Instruction
for b₅ being Nat st b₅ = card b₃ holds
( ((b₃ ';' (b₂ :=len b₁)) ';' b₄) . (insloc b₅) = b₂ :=len b₁ & ((b₃ ';' (b₂ :=len b₁)) ';' b₄) . (insloc (b₅ + 1)) = goto (insloc ((card b₃) + 2)) )

proof end;

theorem Th53: :: SCMBSORT:53

for b₁ being FinSequence of INT
for b₂ being FinSeq-Location
for b₃ being State of SCM+FSA
for b₄ being Macro-Instruction st (Initialized b₄) +* (b₂ .--> b₁) c= b₃ holds
b₄ c= b₃

proof end;

theorem Th54: :: SCMBSORT:54

for b₁ being FinSequence of INT
for b₂ being FinSeq-Location
for b₃ being State of SCM+FSA
for b₄ being Macro-Instruction st (Initialized b₄) +* (b₂ .--> b₁) c= b₃ holds
( b₃ . b₂ = b₁ & b₃ . (intloc 0) = 1 )

proof end;

theorem Th55: :: SCMBSORT:55

for b₁ being FinSeq-Location
for b₂ being Int-Location
for b₃ being State of SCM+FSA holds {b₂,(IC SCM+FSA ),b₁} c= dom b₃

proof end;

theorem Th56: :: SCMBSORT:56

for b₁ being Macro-Instruction
for b₂ being State of SCM+FSA holds (UsedInt*Loc b₁) \/ (UsedIntLoc b₁) c= dom b₂

proof end;

theorem Th57: :: SCMBSORT:57

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction
for b₃ being FinSeq-Location holds (Result (b₁ +* (Initialized b₂))) . b₃ = (IExec b₂,b₁) . b₃

proof end;

set c₁ = intloc 0;

set c₂ = intloc 1;

set c₃ = intloc 2;

set c₄ = intloc 3;

set c₅ = intloc 4;

set c₆ = intloc 5;

set c₇ = intloc 6;

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

definition

let c₉ be FinSeq-Location ;
func bubble-sort c₁ -> Macro-Instruction means :Def1: :: SCMBSORT:def 1
a₂ = (((((((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0))) ';' ((intloc 5) := (intloc 0))) ';' ((intloc 6) := (intloc 0))) ';' ((intloc 1) :=len a₁)) ';' (Times (intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom (intloc 2),(intloc 0))) ';' ((intloc 3) :=len a₁)) ';' (Times (intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0))) ';' ((intloc 5) := a₁,(intloc 3))) ';' ((intloc 6) := a₁,(intloc 4))) ';' (SubFrom (intloc 6),(intloc 5))) ';' (if>0 (intloc 6),((((intloc 6) := a₁,(intloc 4)) ';' (a₁,(intloc 3) := (intloc 6))) ';' (a₁,(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
a₁ = bubble-sort (fsloc 0);
correctness ;

end;

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

set c₉ = intloc (0 + 1);

set c₁₀ = intloc (1 + 1);

set c₁₁ = intloc (2 + 1);

set c₁₂ = intloc (3 + 1);

set c₁₃ = intloc (4 + 1);

set c₁₄ = intloc (5 + 1);

set c₁₅ = fsloc 0;

set c₁₆ = (intloc (3 + 1)) := (intloc (2 + 1));

set c₁₇ = SubFrom (intloc (2 + 1)),(intloc 0);

set c₁₈ = (intloc (4 + 1)) := (fsloc 0),(intloc (2 + 1));

set c₁₉ = (intloc (5 + 1)) := (fsloc 0),(intloc (3 + 1));

set c₂₀ = SubFrom (intloc (5 + 1)),(intloc (4 + 1));

set c₂₁ = (fsloc 0),(intloc (2 + 1)) := (intloc (5 + 1));

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

set c₂₃ = SCM+FSA-Stop ;

set c₂₄ = 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 c₂₅ = ((((((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 c₂₆ = 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 c₂₇ = (intloc (1 + 1)) := (intloc (0 + 1));

set c₂₈ = SubFrom (intloc (1 + 1)),(intloc 0);

set c₂₉ = (intloc (2 + 1)) :=len (fsloc 0);

set c₃₀ = (((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0))) ';' ((intloc (2 + 1)) :=len (fsloc 0));

set c₃₁ = ((((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 c₃₂ = 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 c₃₃ = (intloc (1 + 1)) := (intloc 0);

set c₃₄ = (intloc (2 + 1)) := (intloc 0);

set c₃₅ = (intloc (3 + 1)) := (intloc 0);

set c₃₆ = (intloc (4 + 1)) := (intloc 0);

set c₃₇ = (intloc (5 + 1)) := (intloc 0);

set c₃₈ = (intloc (0 + 1)) :=len (fsloc 0);

theorem Th58: :: SCMBSORT:58

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

proof end;

theorem Th59: :: SCMBSORT:59

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

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

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

theorem Th60: :: SCMBSORT:60

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

proof end;

theorem Th61: :: SCMBSORT:61

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

proof end;

theorem Th62: :: SCMBSORT:62

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

proof end;

theorem Th63: :: SCMBSORT:63

for b₁ being FinSeq-Location
for b₂ being Nat st b₂ < 63 holds
insloc b₂ in dom (bubble-sort b₁)

proof end;

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

proof end;

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

proof end;

Lemma60: ((((((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;

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

Lemma62: ((((((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;

Lemma63: ((((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;

Lemma64: ((((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;

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

Lemma67: for b₁ being State of SCM+FSA holds
( ( b₁ . (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 ),b₁) . (fsloc 0) = ((b₁ . (fsloc 0)) +* (abs (b₁ . (intloc (2 + 1)))),((b₁ . (fsloc 0)) /. (abs (b₁ . (intloc (3 + 1)))))) +* (abs (b₁ . (intloc (3 + 1)))),(b₁ . (intloc (4 + 1))) ) & ( b₁ . (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 ),b₁) . (fsloc 0) = b₁ . (fsloc 0) ) )

proof end;

Lemma68: for b₁ 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 ),b₁) . (intloc (2 + 1)) = b₁ . (intloc (2 + 1))

proof end;

Lemma69: for b₁ being State of SCM+FSA st b₁ . (intloc (2 + 1)) <= len (b₁ . (fsloc 0)) & b₁ . (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 )),b₁) . (intloc (2 + 1)) = (b₁ . (intloc (2 + 1))) - 1 & b₁ . (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 )),b₁) . (fsloc 0) are_fiberwise_equipotent & ( (b₁ . (fsloc 0)) . (b₁ . (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 )),b₁) . (fsloc 0)) . (b₁ . (intloc (2 + 1))) or (b₁ . (fsloc 0)) . (b₁ . (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 )),b₁) . (fsloc 0)) . ((b₁ . (intloc (2 + 1))) - 1) ) & ( (b₁ . (fsloc 0)) . (b₁ . (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 )),b₁) . (fsloc 0)) . (b₁ . (intloc (2 + 1))) or (b₁ . (fsloc 0)) . ((b₁ . (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 )),b₁) . (fsloc 0)) . (b₁ . (intloc (2 + 1))) ) & ( (b₁ . (fsloc 0)) . (b₁ . (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 )),b₁) . (fsloc 0)) . ((b₁ . (intloc (2 + 1))) - 1) or (b₁ . (fsloc 0)) . ((b₁ . (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 )),b₁) . (fsloc 0)) . ((b₁ . (intloc (2 + 1))) - 1) ) & ( for b₂ being set st b₂ <> (b₁ . (intloc (2 + 1))) - 1 & b₂ <> b₁ . (intloc (2 + 1)) & b₂ in dom (b₁ . (fsloc 0)) holds
(b₁ . (fsloc 0)) . b₂ = ((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 )),b₁) . (fsloc 0)) . b₂ ) & ex b₂, b₃ being Integer st
( b₂ = ((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 )),b₁) . (fsloc 0)) . ((b₁ . (intloc (2 + 1))) - 1) & b₃ = ((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 )),b₁) . (fsloc 0)) . (b₁ . (intloc (2 + 1))) & b₂ >= b₃ ) )

proof end;

Lemma70: for b₁ being State of SCM+FSA st b₁ . (intloc (1 + 1)) >= 0 & b₁ . (intloc (1 + 1)) < b₁ . (intloc (2 + 1)) & b₁ . (intloc (2 + 1)) <= len (b₁ . (fsloc 0)) holds
ex b₂ being Nat st
( b₂ <= b₁ . (intloc (2 + 1)) & b₂ >= (b₁ . (intloc (2 + 1))) - (b₁ . (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 ))),b₁) . (fsloc 0)) . b₂ = (b₁ . (fsloc 0)) . (b₁ . (intloc (2 + 1))) )

proof end;

Lemma71: for b₁ being Nat
for b₂ being State of SCM+FSA st b₁ = b₂ . (intloc (1 + 1)) & b₁ < b₂ . (intloc (2 + 1)) & b₂ . (intloc (2 + 1)) <= len (b₂ . (fsloc 0)) holds
( b₂ . (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 ))),b₂) . (fsloc 0) are_fiberwise_equipotent & ( for b₃ being Nat st ( ( b₃ < (b₂ . (intloc (2 + 1))) - b₁ & b₃ >= 1 ) or ( b₃ > b₂ . (intloc (2 + 1)) & b₃ in dom (b₂ . (fsloc 0)) ) ) holds
(b₂ . (fsloc 0)) . b₃ = ((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 ))),b₂) . (fsloc 0)) . b₃ ) & ( for b₃ being Nat st b₃ >= (b₂ . (intloc (2 + 1))) - b₁ & b₃ <= b₂ . (intloc (2 + 1)) holds
ex b₄, b₅ being Integer st
( b₄ = ((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 ))),b₂) . (fsloc 0)) . ((b₂ . (intloc (2 + 1))) - b₁) & b₅ = ((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 ))),b₂) . (fsloc 0)) . b₃ & b₄ >= b₅ ) ) & ( for b₃ being Nat st b₃ >= (b₂ . (intloc (2 + 1))) - b₁ & b₃ <= b₂ . (intloc (2 + 1)) holds
ex b₄ being Nat st
( b₄ >= (b₂ . (intloc (2 + 1))) - b₁ & b₄ <= b₂ . (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 ))),b₂) . (fsloc 0)) . b₃ = (b₂ . (fsloc 0)) . b₄ ) ) )

proof end;

Lemma72: for b₁ 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))),b₁) . (intloc (1 + 1)) = (b₁ . (intloc (0 + 1))) - 1 & (IExec ((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0))) ';' ((intloc (2 + 1)) :=len (fsloc 0))),b₁) . (intloc (2 + 1)) = len (b₁ . (fsloc 0)) & (IExec ((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0))) ';' ((intloc (2 + 1)) :=len (fsloc 0))),b₁) . (fsloc 0) = b₁ . (fsloc 0) )

proof end;

Lemma73: for b₁ being State of SCM+FSA st b₁ . (intloc (0 + 1)) = len (b₁ . (fsloc 0)) holds
( b₁ . (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 ))))),b₁) . (fsloc 0) are_fiberwise_equipotent & ( for b₂, b₃ being Nat st b₂ >= 1 & b₃ <= len (b₁ . (fsloc 0)) & b₂ < b₃ holds
for b₄, b₅ being Integer st b₄ = ((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 ))))),b₁) . (fsloc 0)) . b₂ & b₅ = ((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 ))))),b₁) . (fsloc 0)) . b₃ holds
b₄ >= b₅ ) )

proof end;

theorem Th65: :: SCMBSORT:65

for b₁ being State of SCM+FSA holds
( b₁ . (fsloc 0),(IExec (bubble-sort (fsloc 0)),b₁) . (fsloc 0) are_fiberwise_equipotent & ( for b₂, b₃ being Nat st b₂ >= 1 & b₃ <= len (b₁ . (fsloc 0)) & b₂ < b₃ holds
for b₄, b₅ being Integer st b₄ = ((IExec (bubble-sort (fsloc 0)),b₁) . (fsloc 0)) . b₂ & b₅ = ((IExec (bubble-sort (fsloc 0)),b₁) . (fsloc 0)) . b₃ holds
b₄ >= b₅ ) )

proof end;

theorem Th66: :: SCMBSORT:66

for b₁ being Nat
for b₂ being State of SCM+FSA
for b₃ being FinSequence of INT st (Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0) .--> b₃) c= b₂ holds
IC ((Computation b₂) . b₁) in dom Bubble-Sort-Algorithm

proof end;

theorem Th67: :: SCMBSORT:67

for b₁ being State of SCM+FSA
for b₂ being FinSequence of INT st (Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0) .--> b₂) c= b₁ holds
ex b₃ being FinSequence of REAL st
( b₂,b₃ are_fiberwise_equipotent & b₃ is non-increasing & b₃ is FinSequence of INT & (Result b₁) . (fsloc 0) = b₃ )

proof end;

theorem Th68: :: SCMBSORT:68

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

proof end;

theorem Th69: :: SCMBSORT:69

Initialized Bubble-Sort-Algorithm computes Sorting-Function

proof end;