begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
begin
definition
let a,
b,
c be
Int-Location ;
let I be
Program of ;
let s be
State of ;
canceled;canceled;canceled;canceled;canceled;func StepForUp a,
b,
c,
I,
s -> Function of
NAT ,
product the
Object-Kind of
SCM+FSA equals
StepWhile>0 (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),
((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(intloc 0 ))),
((s +* (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(((s . c) - (s . b)) + 1)) +* a,(s . b));
coherence
StepWhile>0 (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(((s . c) - (s . b)) + 1)) +* a,(s . b)) is Function of NAT , product the Object-Kind of SCM+FSA
;
end;
:: deftheorem SFMASTR3:def 1 :
canceled;
:: deftheorem SFMASTR3:def 2 :
canceled;
:: deftheorem SFMASTR3:def 3 :
canceled;
:: deftheorem SFMASTR3:def 4 :
canceled;
:: deftheorem SFMASTR3:def 5 :
canceled;
:: deftheorem defines StepForUp SFMASTR3:def 6 :
for
a,
b,
c being
Int-Location for
I being
Program of
for
s being
State of holds
StepForUp a,
b,
c,
I,
s = StepWhile>0 (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),
((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(intloc 0 ))),
((s +* (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(((s . c) - (s . b)) + 1)) +* a,(s . b));
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
definition
let a,
b,
c be
Int-Location ;
let I be
Program of ;
let s be
State of ;
pred ProperForUpBody a,
b,
c,
I,
s means :
Def7:
for
i being
Element of
NAT st
i < ((s . c) - (s . b)) + 1 holds
(
I is_closed_on (StepForUp a,b,c,I,s) . i &
I is_halting_on (StepForUp a,b,c,I,s) . i );
end;
:: deftheorem Def7 defines ProperForUpBody SFMASTR3:def 7 :
for
a,
b,
c being
Int-Location for
I being
Program of
for
s being
State of holds
(
ProperForUpBody a,
b,
c,
I,
s iff for
i being
Element of
NAT st
i < ((s . c) - (s . b)) + 1 holds
(
I is_closed_on (StepForUp a,b,c,I,s) . i &
I is_halting_on (StepForUp a,b,c,I,s) . i ) );
theorem Th23:
theorem Th24:
for
s being
State of
for
a being
read-write Int-Location for
bb,
cc being
Int-Location for
Ig being
good Program of
for
k being
Element of
NAT st
((StepForUp a,bb,cc,Ig,s) . k) . (intloc 0 ) = 1 &
Ig is_closed_on (StepForUp a,bb,cc,Ig,s) . k &
Ig is_halting_on (StepForUp a,bb,cc,Ig,s) . k holds
((StepForUp a,bb,cc,Ig,s) . (k + 1)) . (intloc 0 ) = 1
theorem Th25:
for
s being
State of
for
a being
read-write Int-Location for
bb,
cc being
Int-Location for
Ig being
good Program of st
s . (intloc 0 ) = 1 &
ProperForUpBody a,
bb,
cc,
Ig,
s holds
for
k being
Element of
NAT st
k <= ((s . cc) - (s . bb)) + 1 holds
(
((StepForUp a,bb,cc,Ig,s) . k) . (intloc 0 ) = 1 & (
Ig does_not_destroy a implies (
((StepForUp a,bb,cc,Ig,s) . k) . a = k + (s . bb) &
((StepForUp a,bb,cc,Ig,s) . k) . a <= (s . cc) + 1 ) ) &
(((StepForUp a,bb,cc,Ig,s) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + k = ((s . cc) - (s . bb)) + 1 )
theorem Th26:
for
s being
State of
for
a being
read-write Int-Location for
bb,
cc being
Int-Location for
Ig being
good Program of st
s . (intloc 0 ) = 1 &
ProperForUpBody a,
bb,
cc,
Ig,
s holds
for
k being
Element of
NAT holds
(
((StepForUp a,bb,cc,Ig,s) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0 iff
k < ((s . cc) - (s . bb)) + 1 )
theorem Th27:
for
s being
State of
for
a being
read-write Int-Location for
bb,
cc being
Int-Location for
Ig being
good Program of
for
k being
Element of
NAT st
s . (intloc 0 ) = 1 &
ProperForUpBody a,
bb,
cc,
Ig,
s &
k < ((s . cc) - (s . bb)) + 1 holds
((StepForUp a,bb,cc,Ig,s) . (k + 1)) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations ) = (IExec (Ig ';' (AddTo a,(intloc 0 ))),((StepForUp a,bb,cc,Ig,s) . k)) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations )
definition
let a,
b,
c be
Int-Location ;
let I be
Program of ;
func for-up a,
b,
c,
I -> Program of
equals
(((((1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))) := c) ';' (SubFrom (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),b)) ';' (AddTo (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := b)) ';' (while>0 (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(intloc 0 ))));
coherence
(((((1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))) := c) ';' (SubFrom (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),b)) ';' (AddTo (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := b)) ';' (while>0 (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(intloc 0 )))) is Program of
;
end;
:: deftheorem defines for-up SFMASTR3:def 8 :
for
a,
b,
c being
Int-Location for
I being
Program of holds
for-up a,
b,
c,
I = (((((1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))) := c) ';' (SubFrom (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),b)) ';' (AddTo (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := b)) ';' (while>0 (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(intloc 0 ))));
theorem Th28:
theorem Th29:
theorem Th30:
for
s being
State of
for
a being
read-write Int-Location for
bb,
cc being
Int-Location for
I being
Program of st
s . (intloc 0 ) = 1 &
s . bb > s . cc holds
( ( for
x being
Int-Location st
x <> a &
x in {bb,cc} \/ (UsedIntLoc I) holds
(IExec (for-up a,bb,cc,I),s) . x = s . x ) & ( for
f being
FinSeq-Location holds
(IExec (for-up a,bb,cc,I),s) . f = s . f ) )
Lm1:
now
set D =
Int-Locations \/ FinSeq-Locations ;
let s be
State of ;
for a being read-write Int-Location
for bb, cc being Int-Location
for I being good Program of st s . (intloc 0 ) = 1 & ( ProperForUpBody a,bb,cc,I,s or I is parahalting ) holds
( ProperBodyWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )), IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s & WithVariantWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )), IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s )let a be
read-write Int-Location ;
for bb, cc being Int-Location
for I being good Program of st s . (intloc 0 ) = 1 & ( ProperForUpBody a,bb,cc,I,s or I is parahalting ) holds
( ProperBodyWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )), IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s & WithVariantWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )), IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s )let bb,
cc be
Int-Location ;
for I being good Program of st s . (intloc 0 ) = 1 & ( ProperForUpBody a,bb,cc,I,s or I is parahalting ) holds
( ProperBodyWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )), IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s & WithVariantWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )), IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s )let I be
good Program of ;
( s . (intloc 0 ) = 1 & ( ProperForUpBody a,bb,cc,I,s or I is parahalting ) implies ( ProperBodyWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )), IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s & WithVariantWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )), IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s ) )assume that A1:
s . (intloc 0 ) = 1
and A2:
(
ProperForUpBody a,
bb,
cc,
I,
s or
I is
parahalting )
;
( ProperBodyWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )), IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s & WithVariantWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )), IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s )A3:
ProperForUpBody a,
bb,
cc,
I,
s
by A2, Th23;
set scb1 =
((s . cc) - (s . bb)) + 1;
set SF =
StepForUp a,
bb,
cc,
I,
s;
set aux = 1
-stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I));
set IB =
(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ));
set s2 =
(s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,
(s . bb);
set IB2 =
(AddTo a,(intloc 0 )) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ));
set SW2 =
StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),
((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),
((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb));
A4:
StepForUp a,
bb,
cc,
I,
s = StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),
((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),
((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))
;
A5:
(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )) = I ';' ((AddTo a,(intloc 0 )) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )))
by SCMFSA6A:70;
A6:
ProperBodyWhile>0 1
-stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),
(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )),
(s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,
(s . bb)
proof
let k be
Element of
NAT ;
SCMFSA9A:def 4 ( ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 or ( (I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k & (I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k ) )
A7:
(AddTo a,(intloc 0 )) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )) is_closed_on IExec I,
((StepForUp a,bb,cc,I,s) . k)
by SCMFSA7B:24;
assume
((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) > 0
;
( (I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k & (I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k )
then A8:
k < ((s . cc) - (s . bb)) + 1
by A1, A3, A4, Th26;
then A9:
I is_closed_on (StepForUp a,bb,cc,I,s) . k
by A3, Def7;
A10:
((StepForUp a,bb,cc,I,s) . k) . (intloc 0 ) = 1
by A1, A3, A8, Th25;
I is_halting_on (StepForUp a,bb,cc,I,s) . k
by A3, A8, Def7;
then A11:
I is_halting_on Initialize ((StepForUp a,bb,cc,I,s) . k)
by A10, A9, SFMASTR2:5;
A12:
I is_closed_on Initialize ((StepForUp a,bb,cc,I,s) . k)
by A10, A9, SFMASTR2:4;
then A13:
(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )) is_closed_on Initialize ((StepForUp a,bb,cc,I,s) . k)
by A5, A11, A7, SFMASTR1:3;
hence
(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k
by A10, SFMASTR2:4;
(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k
(AddTo a,(intloc 0 )) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )) is_halting_on IExec I,
((StepForUp a,bb,cc,I,s) . k)
by SCMFSA7B:25;
then
(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )) is_halting_on Initialize ((StepForUp a,bb,cc,I,s) . k)
by A5, A12, A11, A7, SFMASTR1:4;
hence
(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k
by A10, A13, SFMASTR2:5;
verum
end;
set i3 =
a := bb;
set i2 =
AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),
(intloc 0 );
set i1 =
SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),
bb;
set i0 =
(1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc;
set s1 =
IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),
s;
set SW1 =
StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),
((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),
(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s);
deffunc H1(
Element of
product the
Object-Kind of
SCM+FSA )
-> Element of
NAT =
abs ($1 . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))));
consider f being
Function of
product the
Object-Kind of
SCM+FSA ,
NAT such that A14:
for
x being
Element of
product the
Object-Kind of
SCM+FSA holds
f . x = H1(
x)
from FUNCT_2:sch 4();
A15:
DataPart (IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s) = DataPart ((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))
by A1, Th22;
thus
ProperBodyWhile>0 1
-stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),
(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )),
IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),
s
WithVariantWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )), IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s
proof
let k be
Element of
NAT ;
SCMFSA9A:def 4 ( ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 or ( (I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k & (I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k ) )
assume A16:
((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) > 0
;
( (I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k & (I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k )
A17:
DataPart ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) = DataPart ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k)
by A15, A6, SCMFSA9A:40;
then A18:
((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) = ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)))
by SCMFSA6A:38;
then A19:
(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k
by A6, A16, SCMFSA9A:def 4;
hence
(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k
by A17, SCMFSA8B:6;
(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k
(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k
by A6, A16, A18, SCMFSA9A:def 4;
hence
(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k
by A17, A19, SCMFSA8B:8;
verum
end;
A20:
for
k being
Element of
NAT holds
(
f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . (k + 1)) < f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k) or
((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 )
proof
let k be
Element of
NAT ;
( f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . (k + 1)) < f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k) or ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 )
A21:
DataPart ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k) = DataPart ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)
by A15, A6, SCMFSA9A:40;
then A22:
((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) = ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)))
by SCMFSA6A:38;
DataPart ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . (k + 1)) = DataPart ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . (k + 1))
by A15, A6, SCMFSA9A:40;
then A23:
((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) = ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)))
by SCMFSA6A:38;
now
assume A24:
((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) > 0
;
f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . (k + 1)) < f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k)then A25:
k < ((s . cc) - (s . bb)) + 1
by A1, A3, A4, A22, Th26;
k < ((s . cc) - (s . bb)) + 1
by A1, A3, A4, A22, A24, Th26;
then A26:
(((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)))) + k = ((s . cc) - (s . bb)) + 1
by A1, A3, A4, Th25;
reconsider scb1 =
((s . cc) - (s . bb)) + 1 as
Element of
NAT by A25, INT_1:16;
A27:
k + 1
<= scb1
by A25, NAT_1:13;
then A28:
(((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)))) + (k + 1) = ((s . cc) - (s . bb)) + 1
by A1, A3, A4, Th25;
A29:
f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k) =
abs (((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))))
by A14
.=
((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)))
by A22, A24, ABSVALUE:def 1
;
per cases
( ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) > 0 or ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 )
;
suppose A30:
((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) > 0
;
f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . (k + 1)) < f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k)
f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . (k + 1)) =
abs (((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))))
by A14
.=
(scb1 - k) - 1
by A23, A28, A30, ABSVALUE:def 1
;
hence
f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . (k + 1)) < f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k)
by A29, A26, XREAL_1:148;
verum
end;
suppose A31:
((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0
;
f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . (k + 1)) < f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k)
((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) = scb1 - (k + 1)
by A28;
then A32:
((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) = 0
by A23, A27, A31, XREAL_1:50;
f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . (k + 1)) =
abs (((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))))
by A14
.=
0
by A32, ABSVALUE:def 1
;
hence
f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . (k + 1)) < f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k)
by A21, A24, A29, SCMFSA6A:38;
verum
end;
end;
end;
hence
(
f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . (k + 1)) < f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k) or
((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 )
;
verum
end;
thus
WithVariantWhile>0 1
-stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),
(I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )),
IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),
s
verum
proof
take
f
;
SCMFSA9A:def 5 for b1 being Element of NAT holds
( not f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . b1) <= f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . (b1 + 1)) or ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . b1) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 )
thus
for
b1 being
Element of
NAT holds
( not
f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . b1) <= f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . (b1 + 1)) or
((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 ))) ';' (a := bb)),s)) . b1) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 )
by A20;
verum
end;
end;
theorem Th31:
for
s being
State of
for
a being
read-write Int-Location for
cc,
bb being
Int-Location for
Ig being
good Program of
for
k being
Element of
NAT st
s . (intloc 0 ) = 1 &
k = ((s . cc) - (s . bb)) + 1 & (
ProperForUpBody a,
bb,
cc,
Ig,
s or
Ig is
parahalting ) holds
DataPart (IExec (for-up a,bb,cc,Ig),s) = DataPart ((StepForUp a,bb,cc,Ig,s) . k)
theorem Th32:
for
s being
State of
for
a being
read-write Int-Location for
bb,
cc being
Int-Location for
Ig being
good Program of st
s . (intloc 0 ) = 1 & (
ProperForUpBody a,
bb,
cc,
Ig,
s or
Ig is
parahalting ) holds
(
for-up a,
bb,
cc,
Ig is_closed_on s &
for-up a,
bb,
cc,
Ig is_halting_on s )
begin
definition
let start,
finish,
minpos be
Int-Location ;
let f be
FinSeq-Location ;
func FinSeqMin f,
start,
finish,
minpos -> Program of
equals
(minpos := start) ';' (for-up (3 -rdRWNotIn {start,finish,minpos}),start,finish,((((1 -stRWNotIn {start,finish,minpos}) := f,(3 -rdRWNotIn {start,finish,minpos})) ';' ((2 -ndRWNotIn {start,finish,minpos}) := f,minpos)) ';' (if>0 (2 -ndRWNotIn {start,finish,minpos}),(1 -stRWNotIn {start,finish,minpos}),(Macro (minpos := (3 -rdRWNotIn {start,finish,minpos}))),(Stop SCM+FSA ))));
coherence
(minpos := start) ';' (for-up (3 -rdRWNotIn {start,finish,minpos}),start,finish,((((1 -stRWNotIn {start,finish,minpos}) := f,(3 -rdRWNotIn {start,finish,minpos})) ';' ((2 -ndRWNotIn {start,finish,minpos}) := f,minpos)) ';' (if>0 (2 -ndRWNotIn {start,finish,minpos}),(1 -stRWNotIn {start,finish,minpos}),(Macro (minpos := (3 -rdRWNotIn {start,finish,minpos}))),(Stop SCM+FSA )))) is Program of
;
end;
:: deftheorem defines FinSeqMin SFMASTR3:def 9 :
for
start,
finish,
minpos being
Int-Location for
f being
FinSeq-Location holds
FinSeqMin f,
start,
finish,
minpos = (minpos := start) ';' (for-up (3 -rdRWNotIn {start,finish,minpos}),start,finish,((((1 -stRWNotIn {start,finish,minpos}) := f,(3 -rdRWNotIn {start,finish,minpos})) ';' ((2 -ndRWNotIn {start,finish,minpos}) := f,minpos)) ';' (if>0 (2 -ndRWNotIn {start,finish,minpos}),(1 -stRWNotIn {start,finish,minpos}),(Macro (minpos := (3 -rdRWNotIn {start,finish,minpos}))),(Stop SCM+FSA ))));
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
for
s being
State of
for
c being
read-write Int-Location for
aa,
bb being
Int-Location for
f being
FinSeq-Location st
aa <> c &
bb <> c &
s . (intloc 0 ) = 1 holds
(
(IExec (FinSeqMin f,aa,bb,c),s) . f = s . f &
(IExec (FinSeqMin f,aa,bb,c),s) . aa = s . aa &
(IExec (FinSeqMin f,aa,bb,c),s) . bb = s . bb )
theorem Th37:
begin
definition
let f be
FinSeq-Location ;
let a,
b be
Int-Location ;
func swap f,
a,
b -> Program of
equals
((((1 -stRWNotIn {a,b}) := f,a) ';' ((2 -ndRWNotIn {a,b}) := f,b)) ';' (f,a := (2 -ndRWNotIn {a,b}))) ';' (f,b := (1 -stRWNotIn {a,b}));
coherence
((((1 -stRWNotIn {a,b}) := f,a) ';' ((2 -ndRWNotIn {a,b}) := f,b)) ';' (f,a := (2 -ndRWNotIn {a,b}))) ';' (f,b := (1 -stRWNotIn {a,b})) is Program of
;
end;
:: deftheorem defines swap SFMASTR3:def 10 :
for
f being
FinSeq-Location for
a,
b being
Int-Location holds
swap f,
a,
b = ((((1 -stRWNotIn {a,b}) := f,a) ';' ((2 -ndRWNotIn {a,b}) := f,b)) ';' (f,a := (2 -ndRWNotIn {a,b}))) ';' (f,b := (1 -stRWNotIn {a,b}));
theorem Th38:
theorem Th39:
theorem
theorem Th41:
theorem
begin
definition
let f be
FinSeq-Location ;
func Selection-sort f -> Program of
equals
((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f) ';' (for-up (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))));
coherence
((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f) ';' (for-up (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))) is Program of
;
end;
:: deftheorem defines Selection-sort SFMASTR3:def 11 :
for
f being
FinSeq-Location holds
Selection-sort f = ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f) ';' (for-up (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))));
theorem