:: SFMASTR3 semantic presentation

theorem Th1: :: SFMASTR3:1
for b1 being set
for b2 being Permutation of b1
for b3, b4 being Element of b1 holds (b2 +* b3,(b2 . b4)) +* b4,(b2 . b3) is Permutation of b1
proof end;

theorem Th2: :: SFMASTR3:2
for b1 being Function
for b2, b3 being set st b2 in dom b1 & b3 in dom b1 holds
ex b4 being Permutation of dom b1 st (b1 +* b2,(b1 . b3)) +* b3,(b1 . b2) = b1 * b4
proof end;

notation
let c1 be non empty finite real-membered set ;
synonym min c1 for lower_bound c1;
end;

definition
let c1 be non empty finite real-membered set ;
redefine func lower_bound c1 -> set means :Def1: :: SFMASTR3:def 1
( a2 in a1 & ( for b1 being real number st b1 in a1 holds
a2 <= b1 ) );
compatibility
for b1 being set holds
( b1 = min c1 iff ( b1 in c1 & ( for b2 being real number st b2 in c1 holds
b1 <= b2 ) ) )
proof end;
end;

:: deftheorem Def1 defines min SFMASTR3:def 1 :
for b1 being non empty finite real-membered set
for b2 being set holds
( b2 = min b1 iff ( b2 in b1 & ( for b3 being real number st b3 in b1 holds
b2 <= b3 ) ) );

registration
let c1 be non empty finite natural-membered set ;
cluster min a1 -> integer ;
coherence
min c1 is integer
proof end;
end;

definition
let c1 be FinSequence of INT ;
let c2, c3 be Nat;
assume E4: ( 1 <= c2 & c2 <= c3 & c3 <= len c1 ) ;
canceled;
func min_at c1,c2,c3 -> Nat means :Def3: :: SFMASTR3:def 3
ex b1 being non empty finite Subset of INT st
( b1 = rng (a2,a3 -cut a1) & a4 + 1 = ((min b1) .. (a2,a3 -cut a1)) + a2 );
existence
ex b1 being Natex b2 being non empty finite Subset of INT st
( b2 = rng (c2,c3 -cut c1) & b1 + 1 = ((min b2) .. (c2,c3 -cut c1)) + c2 )
proof end;
uniqueness
for b1, b2 being Nat st ex b3 being non empty finite Subset of INT st
( b3 = rng (c2,c3 -cut c1) & b1 + 1 = ((min b3) .. (c2,c3 -cut c1)) + c2 ) & ex b3 being non empty finite Subset of INT st
( b3 = rng (c2,c3 -cut c1) & b2 + 1 = ((min b3) .. (c2,c3 -cut c1)) + c2 ) holds
b1 = b2 ;
end;

:: deftheorem Def2 SFMASTR3:def 2 :
canceled;

:: deftheorem Def3 defines min_at SFMASTR3:def 3 :
for b1 being FinSequence of INT
for b2, b3 being Nat st 1 <= b2 & b2 <= b3 & b3 <= len b1 holds
for b4 being Nat holds
( b4 = min_at b1,b2,b3 iff ex b5 being non empty finite Subset of INT st
( b5 = rng (b2,b3 -cut b1) & b4 + 1 = ((min b5) .. (b2,b3 -cut b1)) + b2 ) );

theorem Th3: :: SFMASTR3:3
for b1 being FinSequence of INT
for b2, b3, b4 being Nat st 1 <= b2 & b2 <= b3 & b3 <= len b1 holds
( b4 = min_at b1,b2,b3 iff ( b2 <= b4 & b4 <= b3 & ( for b5 being Nat st b2 <= b5 & b5 <= b3 holds
b1 . b4 <= b1 . b5 ) & ( for b5 being Nat st b2 <= b5 & b5 < b4 holds
b1 . b4 < b1 . b5 ) ) )
proof end;

theorem Th4: :: SFMASTR3:4
for b1 being FinSequence of INT
for b2 being Nat st 1 <= b2 & b2 <= len b1 holds
min_at b1,b2,b2 = b2
proof end;

definition
let c1 be FinSequence of INT ;
let c2, c3 be Nat;
pred c1 is_non_decreasing_on c2,c3 means :Def4: :: SFMASTR3:def 4
for b1, b2 being Nat st a2 <= b1 & b1 <= b2 & b2 <= a3 holds
a1 . b1 <= a1 . b2;
end;

:: deftheorem Def4 defines is_non_decreasing_on SFMASTR3:def 4 :
for b1 being FinSequence of INT
for b2, b3 being Nat holds
( b1 is_non_decreasing_on b2,b3 iff for b4, b5 being Nat st b2 <= b4 & b4 <= b5 & b5 <= b3 holds
b1 . b4 <= b1 . b5 );

definition
let c1 be FinSequence of INT ;
let c2 be Nat;
pred c1 is_split_at c2 means :Def5: :: SFMASTR3:def 5
for b1, b2 being Nat st 1 <= b1 & b1 <= a2 & a2 < b2 & b2 <= len a1 holds
a1 . b1 <= a1 . b2;
end;

:: deftheorem Def5 defines is_split_at SFMASTR3:def 5 :
for b1 being FinSequence of INT
for b2 being Nat holds
( b1 is_split_at b2 iff for b3, b4 being Nat st 1 <= b3 & b3 <= b2 & b2 < b4 & b4 <= len b1 holds
b1 . b3 <= b1 . b4 );

theorem Th5: :: SFMASTR3:5
for b1, b2 being FinSequence of INT
for b3, b4 being Nat st b3 + 1 <= len b1 & b4 = min_at b1,(b3 + 1),(len b1) & b1 is_split_at b3 & b1 is_non_decreasing_on 1,b3 & b2 = (b1 +* (b3 + 1),(b1 . b4)) +* b4,(b1 . (b3 + 1)) holds
b2 is_non_decreasing_on 1,b3 + 1
proof end;

theorem Th6: :: SFMASTR3:6
for b1, b2 being FinSequence of INT
for b3, b4 being Nat st b3 + 1 <= len b1 & b4 = min_at b1,(b3 + 1),(len b1) & b1 is_split_at b3 & b2 = (b1 +* (b3 + 1),(b1 . b4)) +* b4,(b1 . (b3 + 1)) holds
b2 is_split_at b3 + 1
proof end;

theorem Th7: :: SFMASTR3:7
for b1 being State of SCM+FSA
for b2 being Int-Location
for b3 being Macro-Instruction st b3 is_closed_on Initialize b1 & b3 is_halting_on Initialize b1 & b3 does_not_destroy b2 holds
(IExec b3,b1) . b2 = (Initialize b1) . b2
proof end;

theorem Th8: :: SFMASTR3:8
for b1 being State of SCM+FSA st b1 . (intloc 0) = 1 holds
(IExec SCM+FSA-Stop ,b1) | (Int-Locations \/ FinSeq-Locations ) = b1 | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th9: :: SFMASTR3:9
for b1 being Int-Location holds SCM+FSA-Stop does_not_refer b1
proof end;

theorem Th10: :: SFMASTR3:10
for b1, b2, b3 being Int-Location st b1 <> b2 holds
b3 := b2 does_not_refer b1
proof end;

theorem Th11: :: SFMASTR3:11
for b1 being State of SCM+FSA
for b2 being read-write Int-Location
for b3 being Int-Location
for b4 being FinSeq-Location holds (Exec (b2 := b4,b3),b1) . b2 = (b1 . b4) /. (abs (b1 . b3))
proof end;

theorem Th12: :: SFMASTR3:12
for b1 being State of SCM+FSA
for b2, b3 being Int-Location
for b4 being FinSeq-Location holds (Exec (b4,b2 := b3),b1) . b4 = (b1 . b4) +* (abs (b1 . b2)),(b1 . b3)
proof end;

registration
let c1 be read-write Int-Location ;
let c2 be Int-Location ;
let c3, c4 be good Macro-Instruction;
cluster if>0 a1,a2,a3,a4 -> good ;
coherence
if>0 c1,c2,c3,c4 is good
proof end;
end;

theorem Th13: :: SFMASTR3:13
for b1, b2 being Int-Location
for b3, b4 being Macro-Instruction holds UsedIntLoc (if>0 b1,b2,b3,b4) = ({b1,b2} \/ (UsedIntLoc b3)) \/ (UsedIntLoc b4)
proof end;

theorem Th14: :: SFMASTR3:14
for b1, b2 being Int-Location
for b3 being Macro-Instruction st b3 does_not_destroy b1 holds
while>0 b2,b3 does_not_destroy b1
proof end;

theorem Th15: :: SFMASTR3:15
for b1, b2, b3 being Int-Location
for b4, b5 being Macro-Instruction st b1 <> b2 & b4 does_not_destroy b1 & b5 does_not_destroy b1 holds
if>0 b2,b3,b4,b5 does_not_destroy b1
proof end;

definition
let c1, c2, c3 be Int-Location ;
let c4 be Macro-Instruction;
let c5 be State of SCM+FSA ;
func StepForUp c1,c2,c3,c4,c5 -> Function of NAT , product the Object-Kind of SCM+FSA equals :: SFMASTR3:def 6
 StepWhile>0 (1 -stRWNotIn ({a1,a2,a3} \/ (UsedIntLoc a4))),((a4 ';' (AddTo a1,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a1,a2,a3} \/ (UsedIntLoc a4))),(intloc 0))),((a5 +* (1 -stRWNotIn ({a1,a2,a3} \/ (UsedIntLoc a4))),(((a5 . a3) - (a5 . a2)) + 1)) +* a1,(a5 . a2));
coherence
StepWhile>0 (1 -stRWNotIn ({c1,c2,c3} \/ (UsedIntLoc c4))),((c4 ';' (AddTo c1,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c1,c2,c3} \/ (UsedIntLoc c4))),(intloc 0))),((c5 +* (1 -stRWNotIn ({c1,c2,c3} \/ (UsedIntLoc c4))),(((c5 . c3) - (c5 . c2)) + 1)) +* c1,(c5 . c2)) is Function of NAT , product the Object-Kind of SCM+FSA ;
end;

:: deftheorem Def6 defines StepForUp SFMASTR3:def 6 :
for b1, b2, b3 being Int-Location
for b4 being Macro-Instruction
for b5 being State of SCM+FSA holds StepForUp b1,b2,b3,b4,b5 = StepWhile>0 (1 -stRWNotIn ({b1,b2,b3} \/ (UsedIntLoc b4))),((b4 ';' (AddTo b1,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({b1,b2,b3} \/ (UsedIntLoc b4))),(intloc 0))),((b5 +* (1 -stRWNotIn ({b1,b2,b3} \/ (UsedIntLoc b4))),(((b5 . b3) - (b5 . b2)) + 1)) +* b1,(b5 . b2));

theorem Th16: :: SFMASTR3:16
for b1 being State of SCM+FSA
for b2 being read-write Int-Location
for b3, b4 being Int-Location
for b5 being Macro-Instruction st b1 . (intloc 0) = 1 holds
((StepForUp b2,b3,b4,b5,b1) . 0) . (intloc 0) = 1
proof end;

theorem Th17: :: SFMASTR3:17
for b1 being State of SCM+FSA
for b2 being read-write Int-Location
for b3, b4 being Int-Location
for b5 being Macro-Instruction holds ((StepForUp b2,b3,b4,b5,b1) . 0) . b2 = b1 . b3
proof end;

theorem Th18: :: SFMASTR3:18
for b1 being State of SCM+FSA
for b2 being read-write Int-Location
for b3, b4 being Int-Location
for b5 being Macro-Instruction st b2 <> b3 holds
((StepForUp b2,b3,b4,b5,b1) . 0) . b3 = b1 . b3
proof end;

theorem Th19: :: SFMASTR3:19
for b1 being State of SCM+FSA
for b2 being read-write Int-Location
for b3, b4 being Int-Location
for b5 being Macro-Instruction st b2 <> b3 holds
((StepForUp b2,b4,b3,b5,b1) . 0) . b3 = b1 . b3
proof end;

theorem Th20: :: SFMASTR3:20
for b1 being State of SCM+FSA
for b2 being read-write Int-Location
for b3, b4, b5 being Int-Location
for b6 being Macro-Instruction st b2 <> b3 & b3 in UsedIntLoc b6 holds
((StepForUp b2,b4,b5,b6,b1) . 0) . b3 = b1 . b3
proof end;

theorem Th21: :: SFMASTR3:21
for b1 being State of SCM+FSA
for b2 being read-write Int-Location
for b3, b4 being Int-Location
for b5 being FinSeq-Location
for b6 being Macro-Instruction holds ((StepForUp b2,b3,b4,b6,b1) . 0) . b5 = b1 . b5
proof end;

theorem Th22: :: SFMASTR3:22
for b1 being State of SCM+FSA
for b2 being read-write Int-Location
for b3, b4 being Int-Location
for b5 being Macro-Instruction st b1 . (intloc 0) = 1 holds
for b6 being read-write Int-Location st b6 = 1 -stRWNotIn ({b2,b3,b4} \/ (UsedIntLoc b5)) holds
(IExec ((((b6 := b4) ';' (SubFrom b6,b3)) ';' (AddTo b6,(intloc 0))) ';' (b2 := b3)),b1) | (Int-Locations \/ FinSeq-Locations ) = ((b1 +* b6,(((b1 . b4) - (b1 . b3)) + 1)) +* b2,(b1 . b3)) | (Int-Locations \/ FinSeq-Locations )
proof end;

definition
let c1, c2, c3 be Int-Location ;
let c4 be Macro-Instruction;
let c5 be State of SCM+FSA ;
pred ProperForUpBody c1,c2,c3,c4,c5 means :Def7: :: SFMASTR3:def 7
for b1 being Nat st b1 < ((a5 . a3) - (a5 . a2)) + 1 holds
( a4 is_closed_on (StepForUp a1,a2,a3,a4,a5) . b1 & a4 is_halting_on (StepForUp a1,a2,a3,a4,a5) . b1 );
end;

:: deftheorem Def7 defines ProperForUpBody SFMASTR3:def 7 :
for b1, b2, b3 being Int-Location
for b4 being Macro-Instruction
for b5 being State of SCM+FSA holds
( ProperForUpBody b1,b2,b3,b4,b5 iff for b6 being Nat st b6 < ((b5 . b3) - (b5 . b2)) + 1 holds
( b4 is_closed_on (StepForUp b1,b2,b3,b4,b5) . b6 & b4 is_halting_on (StepForUp b1,b2,b3,b4,b5) . b6 ) );

theorem Th23: :: SFMASTR3:23
for b1 being State of SCM+FSA
for b2, b3, b4 being Int-Location
for b5 being parahalting Macro-Instruction holds ProperForUpBody b2,b3,b4,b5,b1
proof end;

theorem Th24: :: SFMASTR3:24
for b1 being State of SCM+FSA
for b2 being read-write Int-Location
for b3, b4 being Int-Location
for b5 being good Macro-Instruction
for b6 being Nat st ((StepForUp b2,b3,b4,b5,b1) . b6) . (intloc 0) = 1 & b5 is_closed_on (StepForUp b2,b3,b4,b5,b1) . b6 & b5 is_halting_on (StepForUp b2,b3,b4,b5,b1) . b6 holds
((StepForUp b2,b3,b4,b5,b1) . (b6 + 1)) . (intloc 0) = 1
proof end;

theorem Th25: :: SFMASTR3:25
for b1 being State of SCM+FSA
for b2 being read-write Int-Location
for b3, b4 being Int-Location
for b5 being good Macro-Instruction st b1 . (intloc 0) = 1 & ProperForUpBody b2,b3,b4,b5,b1 holds
for b6 being Nat st b6 <= ((b1 . b4) - (b1 . b3)) + 1 holds
( ((StepForUp b2,b3,b4,b5,b1) . b6) . (intloc 0) = 1 & ( b5 does_not_destroy b2 implies ( ((StepForUp b2,b3,b4,b5,b1) . b6) . b2 = b6 + (b1 . b3) & ((StepForUp b2,b3,b4,b5,b1) . b6) . b2 <= (b1 . b4) + 1 ) ) & (((StepForUp b2,b3,b4,b5,b1) . b6) . (1 -stRWNotIn ({b2,b3,b4} \/ (UsedIntLoc b5)))) + b6 = ((b1 . b4) - (b1 . b3)) + 1 )
proof end;

theorem Th26: :: SFMASTR3:26
for b1 being State of SCM+FSA
for b2 being read-write Int-Location
for b3, b4 being Int-Location
for b5 being good Macro-Instruction st b1 . (intloc 0) = 1 & ProperForUpBody b2,b3,b4,b5,b1 holds
for b6 being Nat holds
( ((StepForUp b2,b3,b4,b5,b1) . b6) . (1 -stRWNotIn ({b2,b3,b4} \/ (UsedIntLoc b5))) > 0 iff b6 < ((b1 . b4) - (b1 . b3)) + 1 )
proof end;

theorem Th27: :: SFMASTR3:27
for b1 being State of SCM+FSA
for b2 being read-write Int-Location
for b3, b4 being Int-Location
for b5 being good Macro-Instruction
for b6 being Nat st b1 . (intloc 0) = 1 & ProperForUpBody b2,b3,b4,b5,b1 & b6 < ((b1 . b4) - (b1 . b3)) + 1 holds
((StepForUp b2,b3,b4,b5,b1) . (b6 + 1)) | (({b2,b3,b4} \/ (UsedIntLoc b5)) \/ FinSeq-Locations ) = (IExec (b5 ';' (AddTo b2,(intloc 0))),((StepForUp b2,b3,b4,b5,b1) . b6)) | (({b2,b3,b4} \/ (UsedIntLoc b5)) \/ FinSeq-Locations )
proof end;

definition
let c1, c2, c3 be Int-Location ;
let c4 be Macro-Instruction;
set c5 = 1 -stRWNotIn ({c1,c2,c3} \/ (UsedIntLoc c4));
func for-up c1,c2,c3,c4 -> Macro-Instruction equals :: SFMASTR3:def 8
(((((1 -stRWNotIn ({a1,a2,a3} \/ (UsedIntLoc a4))) := a3) ';' (SubFrom (1 -stRWNotIn ({a1,a2,a3} \/ (UsedIntLoc a4))),a2)) ';' (AddTo (1 -stRWNotIn ({a1,a2,a3} \/ (UsedIntLoc a4))),(intloc 0))) ';' (a1 := a2)) ';' (while>0 (1 -stRWNotIn ({a1,a2,a3} \/ (UsedIntLoc a4))),((a4 ';' (AddTo a1,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a1,a2,a3} \/ (UsedIntLoc a4))),(intloc 0))));
coherence
(((((1 -stRWNotIn ({c1,c2,c3} \/ (UsedIntLoc c4))) := c3) ';' (SubFrom (1 -stRWNotIn ({c1,c2,c3} \/ (UsedIntLoc c4))),c2)) ';' (AddTo (1 -stRWNotIn ({c1,c2,c3} \/ (UsedIntLoc c4))),(intloc 0))) ';' (c1 := c2)) ';' (while>0 (1 -stRWNotIn ({c1,c2,c3} \/ (UsedIntLoc c4))),((c4 ';' (AddTo c1,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c1,c2,c3} \/ (UsedIntLoc c4))),(intloc 0)))) is Macro-Instruction ;
end;

:: deftheorem Def8 defines for-up SFMASTR3:def 8 :
for b1, b2, b3 being Int-Location
for b4 being Macro-Instruction holds for-up b1,b2,b3,b4 = (((((1 -stRWNotIn ({b1,b2,b3} \/ (UsedIntLoc b4))) := b3) ';' (SubFrom (1 -stRWNotIn ({b1,b2,b3} \/ (UsedIntLoc b4))),b2)) ';' (AddTo (1 -stRWNotIn ({b1,b2,b3} \/ (UsedIntLoc b4))),(intloc 0))) ';' (b1 := b2)) ';' (while>0 (1 -stRWNotIn ({b1,b2,b3} \/ (UsedIntLoc b4))),((b4 ';' (AddTo b1,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({b1,b2,b3} \/ (UsedIntLoc b4))),(intloc 0))));

theorem Th28: :: SFMASTR3:28
for b1, b2, b3 being Int-Location
for b4 being Macro-Instruction holds {b1,b2,b3} \/ (UsedIntLoc b4) c= UsedIntLoc (for-up b1,b2,b3,b4)
proof end;

registration
let c1 be read-write Int-Location ;
let c2, c3 be Int-Location ;
let c4 be good Macro-Instruction;
cluster for-up a1,a2,a3,a4 -> good ;
coherence
for-up c1,c2,c3,c4 is good ;
end;

theorem Th29: :: SFMASTR3:29
for b1 being read-write Int-Location
for b2, b3, b4 being Int-Location
for b5 being Macro-Instruction st b1 <> b2 & b2 <> 1 -stRWNotIn ({b1,b3,b4} \/ (UsedIntLoc b5)) & b5 does_not_destroy b2 holds
for-up b1,b3,b4,b5 does_not_destroy b2
proof end;

theorem Th30: :: SFMASTR3:30
for b1 being State of SCM+FSA
for b2 being read-write Int-Location
for b3, b4 being Int-Location
for b5 being Macro-Instruction st b1 . (intloc 0) = 1 & b1 . b3 > b1 . b4 holds
( ( for b6 being Int-Location st b6 <> b2 & b6 in {b3,b4} \/ (UsedIntLoc b5) holds
(IExec (for-up b2,b3,b4,b5),b1) . b6 = b1 . b6 ) & ( for b6 being FinSeq-Location holds (IExec (for-up b2,b3,b4,b5),b1) . b6 = b1 . b6 ) )
proof end;

E36: now
let c1 be State of SCM+FSA ;
let c2 be read-write Int-Location ;
let c3, c4 be Int-Location ;
set c5 = Int-Locations \/ FinSeq-Locations ;
let c6 be good Macro-Instruction;
assume that
E37: c1 . (intloc 0) = 1 and
E38: ( ProperForUpBody c2,c3,c4,c6,c1 or c6 is parahalting ) ;
E39: ProperForUpBody c2,c3,c4,c6,c1 by E38, Th23;
set c7 = 1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6));
set c8 = (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4;
set c9 = SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3;
set c10 = AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0);
set c11 = c2 := c3;
set c12 = (c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0));
set c13 = IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1;
set c14 = (c1 +* (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(((c1 . c4) - (c1 . c3)) + 1)) +* c2,(c1 . c3);
E40: (IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1) | (Int-Locations \/ FinSeq-Locations ) = ((c1 +* (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(((c1 . c4) - (c1 . c3)) + 1)) +* c2,(c1 . c3)) | (Int-Locations \/ FinSeq-Locations ) by E37, Th22;
set c15 = (AddTo c2,(intloc 0)) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0));
set c16 = StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1);
set c17 = StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),((c1 +* (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(((c1 . c4) - (c1 . c3)) + 1)) +* c2,(c1 . c3));
set c18 = StepForUp c2,c3,c4,c6,c1;
set c19 = ((c1 . c4) - (c1 . c3)) + 1;
E41: (c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0)) = c6 ';' ((AddTo c2,(intloc 0)) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) by SCMFSA6A:65;
E42: StepForUp c2,c3,c4,c6,c1 = StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),((c1 +* (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(((c1 . c4) - (c1 . c3)) + 1)) +* c2,(c1 . c3)) ;
E43: ProperBodyWhile>0 1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6)),(c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0)),(c1 +* (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(((c1 . c4) - (c1 . c3)) + 1)) +* c2,(c1 . c3)
proof
let c20 be Nat; :: according to SCMFSA9A:def 4
assume ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),((c1 +* (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(((c1 . c4) - (c1 . c3)) + 1)) +* c2,(c1 . c3))) . c20) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) > 0 ;
then E44: c20 < ((c1 . c4) - (c1 . c3)) + 1 by E37, E39, E42, Th26;
then E45: ((StepForUp c2,c3,c4,c6,c1) . c20) . (intloc 0) = 1 by E37, E39, Th25;
E46: c6 is_closed_on (StepForUp c2,c3,c4,c6,c1) . c20 by E39, E44, Def7;
then E47: c6 is_closed_on Initialize ((StepForUp c2,c3,c4,c6,c1) . c20) by E45, SFMASTR2:4;
c6 is_halting_on (StepForUp c2,c3,c4,c6,c1) . c20 by E39, E44, Def7;
then E48: c6 is_halting_on Initialize ((StepForUp c2,c3,c4,c6,c1) . c20) by E45, E46, SFMASTR2:5;
E49: (AddTo c2,(intloc 0)) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0)) is_closed_on IExec c6,((StepForUp c2,c3,c4,c6,c1) . c20) by SCMFSA7B:24;
then E50: (c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0)) is_closed_on Initialize ((StepForUp c2,c3,c4,c6,c1) . c20) by E41, E47, E48, SFMASTR1:3;
hence (c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0)) is_closed_on (StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),((c1 +* (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(((c1 . c4) - (c1 . c3)) + 1)) +* c2,(c1 . c3))) . c20 by E45, SFMASTR2:4;
(AddTo c2,(intloc 0)) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0)) is_halting_on IExec c6,((StepForUp c2,c3,c4,c6,c1) . c20) by SCMFSA7B:25;
then (c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0)) is_halting_on Initialize ((StepForUp c2,c3,c4,c6,c1) . c20) by E41, E47, E48, E49, SFMASTR1:4;
hence (c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0)) is_halting_on (StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),((c1 +* (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(((c1 . c4) - (c1 . c3)) + 1)) +* c2,(c1 . c3))) . c20 by E45, E50, SFMASTR2:5;
end;
thus ProperBodyWhile>0 1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6)),(c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0)), IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1
proof
let c20 be Nat; :: according to SCMFSA9A:def 4
assume E44: ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . c20) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) > 0 ;
E45: ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),((c1 +* (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(((c1 . c4) - (c1 . c3)) + 1)) +* c2,(c1 . c3))) . c20) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . c20) | (Int-Locations \/ FinSeq-Locations ) by E40, E43, SCMFSA9A:40;
then E46: ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . c20) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) = ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),((c1 +* (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(((c1 . c4) - (c1 . c3)) + 1)) +* c2,(c1 . c3))) . c20) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) by SCMFSA6A:38;
then E47: (c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0)) is_closed_on (StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),((c1 +* (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(((c1 . c4) - (c1 . c3)) + 1)) +* c2,(c1 . c3))) . c20 by E43, E44, SCMFSA9A:def 4;
E48: (c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0)) is_halting_on (StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),((c1 +* (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(((c1 . c4) - (c1 . c3)) + 1)) +* c2,(c1 . c3))) . c20 by E43, E44, E46, SCMFSA9A:def 4;
thus (c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0)) is_closed_on (StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . c20 by E45, E47, SCMFSA8B:6;
thus (c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0)) is_halting_on (StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . c20 by E45, E47, E48, SCMFSA8B:8;
end;
deffunc H1( Element of product the Object-Kind of SCM+FSA ) -> Element of NAT = abs (a1 . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))));
consider c20 being Function of product the Object-Kind of SCM+FSA , NAT such that
E44: for b1 being Element of product the Object-Kind of SCM+FSA holds c20 . b1 = H1(b1) from FUNCT_2:sch 4();
E45: for b1 being Nat holds
( c20 . ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . (b1 + 1)) < c20 . ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . b1) or ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . b1) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) <= 0 )
proof
let c21 be Nat;
E46: ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . c21) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),((c1 +* (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(((c1 . c4) - (c1 . c3)) + 1)) +* c2,(c1 . c3))) . c21) | (Int-Locations \/ FinSeq-Locations ) by E40, E43, SCMFSA9A:40;
then E47: ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . c21) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) = ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),((c1 +* (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(((c1 . c4) - (c1 . c3)) + 1)) +* c2,(c1 . c3))) . c21) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) by SCMFSA6A:38;
((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),((c1 +* (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(((c1 . c4) - (c1 . c3)) + 1)) +* c2,(c1 . c3))) . (c21 + 1)) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . (c21 + 1)) | (Int-Locations \/ FinSeq-Locations ) by E40, E43, SCMFSA9A:40;
then E48: ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . (c21 + 1)) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) = ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),((c1 +* (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(((c1 . c4) - (c1 . c3)) + 1)) +* c2,(c1 . c3))) . (c21 + 1)) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) by SCMFSA6A:38;
now
assume E49: ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . c21) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) > 0 ;
E50: c20 . ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . c21) = abs (((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . c21) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6)))) by E44
.= ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),((c1 +* (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(((c1 . c4) - (c1 . c3)) + 1)) +* c2,(c1 . c3))) . c21) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) by E47, E49, ABSVALUE:def 1 ;
c21 < ((c1 . c4) - (c1 . c3)) + 1 by E37, E39, E42, E47, E49, Th26;
then E51: (((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),((c1 +* (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(((c1 . c4) - (c1 . c3)) + 1)) +* c2,(c1 . c3))) . c21) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6)))) + c21 = ((c1 . c4) - (c1 . c3)) + 1 by E37, E39, E42, Th25;
E52: c21 < ((c1 . c4) - (c1 . c3)) + 1 by E37, E39, E42, E47, E49, Th26;
0 <= ((c1 . c4) - (c1 . c3)) + 1 by E52;
then reconsider c22 = ((c1 . c4) - (c1 . c3)) + 1 as Nat by INT_1:16;
E53: c21 + 1 <= c22 by E52, NAT_1:38;
then E54: (((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),((c1 +* (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(((c1 . c4) - (c1 . c3)) + 1)) +* c2,(c1 . c3))) . (c21 + 1)) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6)))) + (c21 + 1) = ((c1 . c4) - (c1 . c3)) + 1 by E37, E39, E42, Th25;
per cases ( ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . (c21 + 1)) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) > 0 or ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . (c21 + 1)) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) <= 0 ) ;
suppose E55: ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . (c21 + 1)) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) > 0 ;
E56: c20 . ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . (c21 + 1)) = abs (((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . (c21 + 1)) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6)))) by E44
.= ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),((c1 +* (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(((c1 . c4) - (c1 . c3)) + 1)) +* c2,(c1 . c3))) . (c21 + 1)) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) by E48, E55, ABSVALUE:def 1
.= c22 - (c21 + 1) by E54
.= (c22 - c21) - 1 ;
((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),((c1 +* (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(((c1 . c4) - (c1 . c3)) + 1)) +* c2,(c1 . c3))) . c21) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) = c22 - c21 by E51;
hence c20 . ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . (c21 + 1)) < c20 . ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . c21) by E50, E56, XREAL_1:148;
end;
suppose E55: ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . (c21 + 1)) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) <= 0 ;
((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),((c1 +* (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(((c1 . c4) - (c1 . c3)) + 1)) +* c2,(c1 . c3))) . (c21 + 1)) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) = c22 - (c21 + 1) by E54;
then E56: ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . (c21 + 1)) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) = 0 by E48, E53, E55, XREAL_1:50;
c20 . ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . (c21 + 1)) = abs (((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . (c21 + 1)) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6)))) by E44
.= 0 by E56, ABSVALUE:def 1 ;
hence c20 . ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . (c21 + 1)) < c20 . ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . c21) by E46, E49, E50, SCMFSA6A:38;
end;
end;
end;
hence ( c20 . ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . (c21 + 1)) < c20 . ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . c21) or ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . c21) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) <= 0 ) ;
end;
thus WithVariantWhile>0 1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6)),(c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0)), IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1
proof
take c20 ; :: according to SCMFSA9A:def 5
thus for b1 being Element of NAT holds
( not c20 . ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . b1) <= c20 . ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . (b1 + 1)) or ((StepWhile>0 (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),((c6 ';' (AddTo c2,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))),(IExec (((((1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) := c4) ';' (SubFrom (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),c3)) ';' (AddTo (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))),(intloc 0))) ';' (c2 := c3)),c1)) . b1) . (1 -stRWNotIn ({c2,c3,c4} \/ (UsedIntLoc c6))) <= 0 ) by E45;
end;
end;

theorem Th31: :: SFMASTR3:31
for b1 being State of SCM+FSA
for b2 being read-write Int-Location
for b3, b4 being Int-Location
for b5 being good Macro-Instruction
for b6 being Nat st b1 . (intloc 0) = 1 & b6 = ((b1 . b3) - (b1 . b4)) + 1 & ( ProperForUpBody b2,b4,b3,b5,b1 or b5 is parahalting ) holds
(IExec (for-up b2,b4,b3,b5),b1) | (Int-Locations \/ FinSeq-Locations ) = ((StepForUp b2,b4,b3,b5,b1) . b6) | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th32: :: SFMASTR3:32
for b1 being State of SCM+FSA
for b2 being read-write Int-Location
for b3, b4 being Int-Location
for b5 being good Macro-Instruction st b1 . (intloc 0) = 1 & ( ProperForUpBody b2,b3,b4,b5,b1 or b5 is parahalting ) holds
( for-up b2,b3,b4,b5 is_closed_on b1 & for-up b2,b3,b4,b5 is_halting_on b1 )
proof end;

definition
let c1, c2, c3 be Int-Location ;
let c4 be FinSeq-Location ;
set c5 = 1 -stRWNotIn {c1,c2,c3};
set c6 = 2 -ndRWNotIn {c1,c2,c3};
set c7 = 3 -rdRWNotIn {c1,c2,c3};
func FinSeqMin c4,c1,c2,c3 -> Macro-Instruction equals :: SFMASTR3:def 9
(a3 := a1) ';' (for-up (3 -rdRWNotIn {a1,a2,a3}),a1,a2,((((1 -stRWNotIn {a1,a2,a3}) := a4,(3 -rdRWNotIn {a1,a2,a3})) ';' ((2 -ndRWNotIn {a1,a2,a3}) := a4,a3)) ';' (if>0 (2 -ndRWNotIn {a1,a2,a3}),(1 -stRWNotIn {a1,a2,a3}),(Macro (a3 := (3 -rdRWNotIn {a1,a2,a3}))),SCM+FSA-Stop )));
coherence
(c3 := c1) ';' (for-up (3 -rdRWNotIn {c1,c2,c3}),c1,c2,((((1 -stRWNotIn {c1,c2,c3}) := c4,(3 -rdRWNotIn {c1,c2,c3})) ';' ((2 -ndRWNotIn {c1,c2,c3}) := c4,c3)) ';' (if>0 (2 -ndRWNotIn {c1,c2,c3}),(1 -stRWNotIn {c1,c2,c3}),(Macro (c3 := (3 -rdRWNotIn {c1,c2,c3}))),SCM+FSA-Stop ))) is Macro-Instruction ;
end;

:: deftheorem Def9 defines FinSeqMin SFMASTR3:def 9 :
for b1, b2, b3 being Int-Location
for b4 being FinSeq-Location holds FinSeqMin b4,b1,b2,b3 = (b3 := b1) ';' (for-up (3 -rdRWNotIn {b1,b2,b3}),b1,b2,((((1 -stRWNotIn {b1,b2,b3}) := b4,(3 -rdRWNotIn {b1,b2,b3})) ';' ((2 -ndRWNotIn {b1,b2,b3}) := b4,b3)) ';' (if>0 (2 -ndRWNotIn {b1,b2,b3}),(1 -stRWNotIn {b1,b2,b3}),(Macro (b3 := (3 -rdRWNotIn {b1,b2,b3}))),SCM+FSA-Stop )));

registration
let c1, c2 be Int-Location ;
let c3 be read-write Int-Location ;
let c4 be FinSeq-Location ;
cluster FinSeqMin a4,a1,a2,a3 -> good ;
coherence
FinSeqMin c4,c1,c2,c3 is good ;
end;

theorem Th33: :: SFMASTR3:33
for b1 being read-write Int-Location
for b2, b3 being Int-Location
for b4 being FinSeq-Location st b1 <> b2 holds
FinSeqMin b4,b2,b3,b1 does_not_destroy b2
proof end;

theorem Th34: :: SFMASTR3:34
for b1 being read-write Int-Location
for b2, b3 being Int-Location
for b4 being FinSeq-Location holds {b2,b3,b1} c= UsedIntLoc (FinSeqMin b4,b2,b3,b1)
proof end;

theorem Th35: :: SFMASTR3:35
for b1 being State of SCM+FSA
for b2 being read-write Int-Location
for b3, b4 being Int-Location
for b5 being FinSeq-Location st b1 . (intloc 0) = 1 holds
( FinSeqMin b5,b3,b4,b2 is_closed_on b1 & FinSeqMin b5,b3,b4,b2 is_halting_on b1 )
proof end;

theorem Th36: :: SFMASTR3:36
for b1 being State of SCM+FSA
for b2 being read-write Int-Location
for b3, b4 being Int-Location
for b5 being FinSeq-Location st b3 <> b2 & b4 <> b2 & b1 . (intloc 0) = 1 holds
( (IExec (FinSeqMin b5,b3,b4,b2),b1) . b5 = b1 . b5 & (IExec (FinSeqMin b5,b3,b4,b2),b1) . b3 = b1 . b3 & (IExec (FinSeqMin b5,b3,b4,b2),b1) . b4 = b1 . b4 )
proof end;

theorem Th37: :: SFMASTR3:37
for b1 being State of SCM+FSA
for b2 being read-write Int-Location
for b3, b4 being Int-Location
for b5 being FinSeq-Location st 1 <= b1 . b3 & b1 . b3 <= b1 . b4 & b1 . b4 <= len (b1 . b5) & b3 <> b2 & b4 <> b2 & b1 . (intloc 0) = 1 holds
(IExec (FinSeqMin b5,b3,b4,b2),b1) . b2 = min_at (b1 . b5),(abs (b1 . b3)),(abs (b1 . b4))
proof end;

definition
let c1 be FinSeq-Location ;
let c2, c3 be Int-Location ;
set c4 = 1 -stRWNotIn {c2,c3};
set c5 = 2 -ndRWNotIn {c2,c3};
func swap c1,c2,c3 -> Macro-Instruction equals :: SFMASTR3:def 10
((((1 -stRWNotIn {a2,a3}) := a1,a2) ';' ((2 -ndRWNotIn {a2,a3}) := a1,a3)) ';' (a1,a2 := (2 -ndRWNotIn {a2,a3}))) ';' (a1,a3 := (1 -stRWNotIn {a2,a3}));
coherence
((((1 -stRWNotIn {c2,c3}) := c1,c2) ';' ((2 -ndRWNotIn {c2,c3}) := c1,c3)) ';' (c1,c2 := (2 -ndRWNotIn {c2,c3}))) ';' (c1,c3 := (1 -stRWNotIn {c2,c3})) is Macro-Instruction ;
end;

:: deftheorem Def10 defines swap SFMASTR3:def 10 :
for b1 being FinSeq-Location
for b2, b3 being Int-Location holds swap b1,b2,b3 = ((((1 -stRWNotIn {b2,b3}) := b1,b2) ';' ((2 -ndRWNotIn {b2,b3}) := b1,b3)) ';' (b1,b2 := (2 -ndRWNotIn {b2,b3}))) ';' (b1,b3 := (1 -stRWNotIn {b2,b3}));

registration
let c1 be FinSeq-Location ;
let c2, c3 be Int-Location ;
cluster swap a1,a2,a3 -> good parahalting ;
coherence
( swap c1,c2,c3 is good & swap c1,c2,c3 is parahalting ) ;
end;

theorem Th38: :: SFMASTR3:38
for b1, b2, b3 being Int-Location
for b4 being FinSeq-Location st b1 <> 1 -stRWNotIn {b2,b3} & b1 <> 2 -ndRWNotIn {b2,b3} holds
swap b4,b2,b3 does_not_destroy b1
proof end;

theorem Th39: :: SFMASTR3:39
for b1 being State of SCM+FSA
for b2, b3 being Int-Location
for b4 being FinSeq-Location st 1 <= b1 . b2 & b1 . b2 <= len (b1 . b4) & 1 <= b1 . b3 & b1 . b3 <= len (b1 . b4) & b1 . (intloc 0) = 1 holds
(IExec (swap b4,b2,b3),b1) . b4 = ((b1 . b4) +* (b1 . b2),((b1 . b4) . (b1 . b3))) +* (b1 . b3),((b1 . b4) . (b1 . b2))
proof end;

theorem Th40: :: SFMASTR3:40
for b1 being State of SCM+FSA
for b2, b3 being Int-Location
for b4 being FinSeq-Location st 1 <= b1 . b2 & b1 . b2 <= len (b1 . b4) & 1 <= b1 . b3 & b1 . b3 <= len (b1 . b4) & b1 . (intloc 0) = 1 holds
( ((IExec (swap b4,b2,b3),b1) . b4) . (b1 . b2) = (b1 . b4) . (b1 . b3) & ((IExec (swap b4,b2,b3),b1) . b4) . (b1 . b3) = (b1 . b4) . (b1 . b2) )
proof end;

theorem Th41: :: SFMASTR3:41
for b1, b2 being Int-Location
for b3 being FinSeq-Location holds {b1,b2} c= UsedIntLoc (swap b3,b1,b2)
proof end;

theorem Th42: :: SFMASTR3:42
for b1, b2 being Int-Location
for b3 being FinSeq-Location holds UsedInt*Loc (swap b3,b1,b2) = {b3}
proof end;

definition
let c1 be FinSeq-Location ;
set c2 = 1 -stRWNotIn ({} Int-Locations );
set c3 = 2 -ndRWNotIn ({} Int-Locations );
func Selection-sort c1 -> Macro-Instruction equals :: SFMASTR3:def 11
((1 -stNotUsed (swap a1,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len a1) ';' (for-up (1 -stRWNotIn ({} Int-Locations )),(intloc 0),(1 -stNotUsed (swap a1,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin a1,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap a1,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap a1,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))));
coherence
((1 -stNotUsed (swap c1,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len c1) ';' (for-up (1 -stRWNotIn ({} Int-Locations )),(intloc 0),(1 -stNotUsed (swap c1,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin c1,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap c1,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap c1,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))) is Macro-Instruction ;
end;

:: deftheorem Def11 defines Selection-sort SFMASTR3:def 11 :
for b1 being FinSeq-Location holds Selection-sort b1 = ((1 -stNotUsed (swap b1,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len b1) ';' (for-up (1 -stRWNotIn ({} Int-Locations )),(intloc 0),(1 -stNotUsed (swap b1,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin b1,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap b1,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap b1,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))));

theorem Th43: :: SFMASTR3:43
for b1 being State of SCM+FSA
for b2 being FinSeq-Location
for b3 being State of SCM+FSA st b3 = IExec (Selection-sort b2),b1 holds
( b3 . b2 is_non_decreasing_on 1, len (b3 . b2) & ex b4 being Permutation of dom (b1 . b2) st b3 . b2 = (b1 . b2) * b4 )
proof end;