:: The { \bf for } (going up) Macro Instruction
:: by Piotr Rudnicki
::
:: Received June 4, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


begin

theorem Th1: :: SFMASTR3:1
for s being State of SCM+FSA
for aa being Int-Location
for I being Program of
for p being Instruction-Sequence of SCM+FSA st I is_closed_on Initialized s,p & I is_halting_on Initialized s,p & not I destroys aa holds
(IExec (I,p,s)) . aa = (Initialized s) . aa
proof end;

theorem Th2: :: SFMASTR3:2
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 holds
DataPart (IExec ((Stop SCM+FSA),p,s)) = DataPart s
proof end;

theorem Th3: :: SFMASTR3:3
for aa being Int-Location holds not Stop SCM+FSA refers aa
proof end;

theorem Th4: :: SFMASTR3:4
for aa, bb, cc being Int-Location st aa <> bb holds
not cc := bb refers aa
proof end;

theorem Th5: :: SFMASTR3:5
for s being State of SCM+FSA
for a being read-write Int-Location
for bb being Int-Location
for f being FinSeq-Location holds (Exec ((a := (f,bb)),s)) . a = (s . f) /. (abs (s . bb))
proof end;

theorem Th6: :: SFMASTR3:6
for s being State of SCM+FSA
for aa, bb being Int-Location
for f being FinSeq-Location holds (Exec (((f,aa) := bb),s)) . f = (s . f) +* ((abs (s . aa)),(s . bb))
proof end;

registration
let a be read-write Int-Location;
let b be Int-Location;
let I, J be good Program of ;
cluster if>0 (a,b,I,J) -> good ;
coherence
if>0 (a,b,I,J) is good
proof end;
end;

theorem Th7: :: SFMASTR3:7
for aa, bb being Int-Location
for I, J being Program of holds UsedIntLoc (if>0 (aa,bb,I,J)) = ({aa,bb} \/ (UsedIntLoc I)) \/ (UsedIntLoc J)
proof end;

theorem Th8: :: SFMASTR3:8
for aa, bb being Int-Location
for I being Program of st not I destroys aa holds
not while>0 (bb,I) destroys aa
proof end;

theorem Th9: :: SFMASTR3:9
for cc, aa, bb being Int-Location
for I, J being Program of st cc <> aa & not I destroys cc & not J destroys cc holds
not if>0 (aa,bb,I,J) destroys cc
proof end;

begin

definition
let p be Instruction-Sequence of SCM+FSA;
let a, b, c be Int-Location;
let I be Program of ;
let s be State of SCM+FSA;
func StepForUp (a,b,c,I,p,s) -> Function of NAT,(product (the_Values_of SCM+FSA)) equals :: SFMASTR3:def 1
 StepWhile>0 ((1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(intloc 0)))),p,((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)))),p,((s +* ((1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(((s . c) - (s . b)) + 1))) +* (a,(s . b)))) is Function of NAT,(product (the_Values_of SCM+FSA)) ;
end;

:: deftheorem defines StepForUp SFMASTR3:def 1 :
for p being Instruction-Sequence of SCM+FSA
for a, b, c being Int-Location
for I being Program of
for s being State of SCM+FSA holds StepForUp (a,b,c,I,p,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)))),p,((s +* ((1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(((s . c) - (s . b)) + 1))) +* (a,(s . b))));

theorem Th10: :: SFMASTR3:10
for s being State of SCM+FSA
for a being read-write Int-Location
for bb, cc being Int-Location
for I being Program of
for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 holds
((StepForUp (a,bb,cc,I,p,s)) . 0) . (intloc 0) = 1
proof end;

theorem Th11: :: SFMASTR3:11
for s being State of SCM+FSA
for a being read-write Int-Location
for bb, cc being Int-Location
for I being Program of
for p being Instruction-Sequence of SCM+FSA holds ((StepForUp (a,bb,cc,I,p,s)) . 0) . a = s . bb
proof end;

theorem Th12: :: SFMASTR3:12
for s being State of SCM+FSA
for a being read-write Int-Location
for bb, cc being Int-Location
for I being Program of
for p being Instruction-Sequence of SCM+FSA st a <> bb holds
((StepForUp (a,bb,cc,I,p,s)) . 0) . bb = s . bb
proof end;

theorem Th13: :: SFMASTR3:13
for s being State of SCM+FSA
for a being read-write Int-Location
for cc, bb being Int-Location
for I being Program of
for p being Instruction-Sequence of SCM+FSA st a <> cc holds
((StepForUp (a,bb,cc,I,p,s)) . 0) . cc = s . cc
proof end;

theorem Th14: :: SFMASTR3:14
for s being State of SCM+FSA
for a being read-write Int-Location
for dd, bb, cc being Int-Location
for I being Program of
for p being Instruction-Sequence of SCM+FSA st a <> dd & dd in UsedIntLoc I holds
((StepForUp (a,bb,cc,I,p,s)) . 0) . dd = s . dd
proof end;

theorem Th15: :: SFMASTR3:15
for s being State of SCM+FSA
for a being read-write Int-Location
for bb, cc being Int-Location
for f being FinSeq-Location
for I being Program of
for p being Instruction-Sequence of SCM+FSA holds ((StepForUp (a,bb,cc,I,p,s)) . 0) . f = s . f
proof end;

theorem Th16: :: SFMASTR3:16
for s being State of SCM+FSA
for a being read-write Int-Location
for bb, cc being Int-Location
for I being Program of
for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 holds
for aux being read-write Int-Location st aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)) holds
DataPart (IExec (((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))) ";" (a := bb)),p,s)) = DataPart ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)))
proof end;

definition
let p be Instruction-Sequence of SCM+FSA;
let a, b, c be Int-Location;
let I be Program of ;
let s be State of SCM+FSA;
pred ProperForUpBody a,b,c,I,s,p means :Def2: :: SFMASTR3:def 2
 for i being Element of NAT st i < ((s . c) - (s . b)) + 1 holds
( I is_closed_on (StepForUp (a,b,c,I,p,s)) . i,p +* (while>0 ((1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(intloc 0)))))) & I is_halting_on (StepForUp (a,b,c,I,p,s)) . i,p +* (while>0 ((1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(intloc 0)))))) );
end;

:: deftheorem Def2 defines ProperForUpBody SFMASTR3:def 2 :
for p being Instruction-Sequence of SCM+FSA
for a, b, c being Int-Location
for I being Program of
for s being State of SCM+FSA holds
( ProperForUpBody a,b,c,I,s,p iff for i being Element of NAT st i < ((s . c) - (s . b)) + 1 holds
( I is_closed_on (StepForUp (a,b,c,I,p,s)) . i,p +* (while>0 ((1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(intloc 0)))))) & I is_halting_on (StepForUp (a,b,c,I,p,s)) . i,p +* (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 Th17: :: SFMASTR3:17
for s being State of SCM+FSA
for aa, bb, cc being Int-Location
for p being Instruction-Sequence of SCM+FSA
for I being parahalting Program of holds ProperForUpBody aa,bb,cc,I,s,p
proof end;

theorem Th18: :: SFMASTR3:18
for s being State of SCM+FSA
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
for p being Instruction-Sequence of SCM+FSA st ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (intloc 0) = 1 & Ig is_closed_on (StepForUp (a,bb,cc,Ig,p,s)) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))))) & Ig is_halting_on (StepForUp (a,bb,cc,Ig,p,s)) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))))) holds
((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (intloc 0) = 1
proof end;

theorem Th19: :: SFMASTR3:19
for s being State of SCM+FSA
for a being read-write Int-Location
for bb, cc being Int-Location
for Ig being good Program of
for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s,p holds
for k being Element of NAT st k <= ((s . cc) - (s . bb)) + 1 holds
( ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (intloc 0) = 1 & ( not Ig destroys a implies ( ((StepForUp (a,bb,cc,Ig,p,s)) . k) . a = k + (s . bb) & ((StepForUp (a,bb,cc,Ig,p,s)) . k) . a <= (s . cc) + 1 ) ) & (((StepForUp (a,bb,cc,Ig,p,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + k = ((s . cc) - (s . bb)) + 1 )
proof end;

theorem Th20: :: SFMASTR3:20
for s being State of SCM+FSA
for a being read-write Int-Location
for bb, cc being Int-Location
for Ig being good Program of
for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s,p holds
for k being Element of NAT holds
( ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0 iff k < ((s . cc) - (s . bb)) + 1 )
proof end;

theorem Th21: :: SFMASTR3:21
for s being State of SCM+FSA
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
for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s,p & k < ((s . cc) - (s . bb)) + 1 holds
((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ";" (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))))))),((StepForUp (a,bb,cc,Ig,p,s)) . k))) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations)
proof end;

definition
let a, b, c be Int-Location;
let I be Program of ;
func for-up (a,b,c,I) -> Program of equals :: SFMASTR3:def 3
(((((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 3 :
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 Th22: :: SFMASTR3:22
for aa, bb, cc being Int-Location
for I being Program of holds {aa,bb,cc} \/ (UsedIntLoc I) c= UsedIntLoc (for-up (aa,bb,cc,I))
proof end;

registration
let a be read-write Int-Location;
let b, c be Int-Location;
let I be good Program of ;
cluster for-up (a,b,c,I) -> good ;
coherence
for-up (a,b,c,I) is good ;
end;

theorem Th23: :: SFMASTR3:23
for a being read-write Int-Location
for aa, bb, cc being Int-Location
for I being Program of st a <> aa & aa <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)) & not I destroys aa holds
not for-up (a,bb,cc,I) destroys aa
proof end;

theorem Th24: :: SFMASTR3:24
for s being State of SCM+FSA
for a being read-write Int-Location
for bb, cc being Int-Location
for I being Program of
for p being Instruction-Sequence of SCM+FSA 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)),p,s)) . x = s . x ) & ( for f being FinSeq-Location holds (IExec ((for-up (a,bb,cc,I)),p,s)) . f = s . f ) )
proof end;

Lm1: now :: thesis: for s being State of SCM+FSA
for a being read-write Int-Location
for bb, cc being Int-Location
for p being Instruction-Sequence of SCM+FSA
for I being good Program of st s . (intloc 0) = 1 & ( ProperForUpBody a,bb,cc,I,s,p 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)),p,s),p & 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)),p,s),p )
let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for bb, cc being Int-Location
for p being Instruction-Sequence of SCM+FSA
for I being good Program of st s . (intloc 0) = 1 & ( ProperForUpBody a,bb,cc,I,s,p 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)),p,s),p & 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)),p,s),p )
let a be read-write Int-Location; :: thesis: for bb, cc being Int-Location
for p being Instruction-Sequence of SCM+FSA
for I being good Program of st s . (intloc 0) = 1 & ( ProperForUpBody a,bb,cc,I,s,p 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)),p,s),p & 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)),p,s),p )
let bb, cc be Int-Location; :: thesis: for p being Instruction-Sequence of SCM+FSA
for I being good Program of st s . (intloc 0) = 1 & ( ProperForUpBody a,bb,cc,I,s,p 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)),p,s),p & 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)),p,s),p )
let p be Instruction-Sequence of SCM+FSA; :: thesis: for I being good Program of st s . (intloc 0) = 1 & ( ProperForUpBody a,bb,cc,I,s,p 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)),p,s),p & 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)),p,s),p )
let I be good Program of ; :: thesis: ( s . (intloc 0) = 1 & ( ProperForUpBody a,bb,cc,I,s,p 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)),p,s),p & 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)),p,s),p ) )
assume that
A1: s . (intloc 0) = 1 and
A2: ( ProperForUpBody a,bb,cc,I,s,p or I is parahalting ) ; :: thesis: ( 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)),p,s),p & 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)),p,s),p )
A3: ProperForUpBody a,bb,cc,I,s,p by A2, Th17;
set scb1 = ((s . cc) - (s . bb)) + 1;
set SF = StepForUp (a,bb,cc,I,p,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 p2 = p;
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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))));
A4: StepForUp (a,bb,cc,I,p,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)))),p,((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:28;
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)),p
proof
let k be Element of NAT ; :: according to SCMFSA9A:def 4 :: thesis: ( ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))),p,((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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((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))) 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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) ) )
A7: (AddTo (a,(intloc 0))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) is_closed_on IExec (I,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))))))),((StepForUp (a,bb,cc,I,p,s)) . k)),p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) by SCMFSA7B:18;
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)))),p,((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 ; :: thesis: ( (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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((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))) 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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) )
then A8: k < ((s . cc) - (s . bb)) + 1 by A1, A3, A4, Th20;
then A9: I is_closed_on (StepForUp (a,bb,cc,I,p,s)) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) by A3, Def2;
A10: ((StepForUp (a,bb,cc,I,p,s)) . k) . (intloc 0) = 1 by A1, A3, A8, Th19;
I is_halting_on (StepForUp (a,bb,cc,I,p,s)) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) by A3, A8, Def2;
then A11: I is_halting_on Initialized ((StepForUp (a,bb,cc,I,p,s)) . k),p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) by A10, A9, SFMASTR2:5;
A12: I is_closed_on Initialized ((StepForUp (a,bb,cc,I,p,s)) . k),p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) 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 Initialized ((StepForUp (a,bb,cc,I,p,s)) . k),p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) by A5, A11, A7, SFMASTR1:2;
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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) by A10, SFMASTR2:4; :: thesis: (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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))))))
(AddTo (a,(intloc 0))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) is_halting_on IExec (I,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))))))),((StepForUp (a,bb,cc,I,p,s)) . k)),p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) by SCMFSA7B:19;
then (I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) is_halting_on Initialized ((StepForUp (a,bb,cc,I,p,s)) . k),p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) by A5, A12, A11, A7, SFMASTR1:3;
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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) by A10, A13, SFMASTR2:5; :: thesis: 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)),p,s);
set p1 = p;
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)))),p,(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)),p,s)));
deffunc H1( State of SCM+FSA) -> Element of NAT = abs ($1 . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))));
consider f being Function of (product (the_Values_of SCM+FSA)),NAT such that
A14: for x being Element of product (the_Values_of SCM+FSA) holds f . x = H1(x) from FUNCT_2:sch 4();
A15: for x being State of SCM+FSA holds f . x = H1(x)
proof
let x be State of SCM+FSA; :: thesis: f . x = H1(x)
reconsider x = x as Element of product (the_Values_of SCM+FSA) by CARD_3:107;
f . x = H1(x) by A14;
hence f . x = H1(x) ; :: thesis: verum
end;
A16: 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)),p,s)) = DataPart ((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) by A1, Th16;
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)),p,s),p :: thesis: 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)),p,s),p
proof
let k be Element of NAT ; :: according to SCMFSA9A:def 4 :: thesis: ( ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))),p,(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)),p,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)))),p,(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)),p,s)))) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((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))) 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)))),p,(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)),p,s)))) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) ) )
assume A17: ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))),p,(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)),p,s)))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) > 0 ; :: thesis: ( (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)))),p,(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)),p,s)))) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((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))) 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)))),p,(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)),p,s)))) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) )
A18: 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)))),p,((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)))),p,(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)),p,s)))) . k) by A16, A6, SCMFSA9A:34;
then A19: ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))),p,(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)),p,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)))),p,((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 SCMFSA_M:2;
then A20: (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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) by A6, A17, 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)))),p,(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)),p,s)))) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) by A18, SCMFSA8B:3; :: thesis: (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)))),p,(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)),p,s)))) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((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))) 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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) by A6, A17, A19, 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)))),p,(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)),p,s)))) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) by A18, A20, SCMFSA8B:5; :: thesis: verum
end;
A21: 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)))),p,(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)),p,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)))),p,(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)),p,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)))),p,(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)),p,s)))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 )
proof
let k be Element of NAT ; :: thesis: ( 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)))),p,(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)),p,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)))),p,(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)),p,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)))),p,(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)),p,s)))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 )
A22: 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)))),p,(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)),p,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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k) by A16, A6, SCMFSA9A:34;
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)))),p,(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)),p,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)))),p,((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 SCMFSA_M:2;
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)))),p,((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)))),p,(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)),p,s)))) . (k + 1)) by A16, A6, SCMFSA9A:34;
then 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)))),p,(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)),p,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)))),p,((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 SCMFSA_M:2;
now :: thesis: ( ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))),p,(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)),p,s)))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) > 0 implies 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)))),p,(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)),p,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)))),p,(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)),p,s)))) . k) )
assume A25: ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))),p,(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)),p,s)))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) > 0 ; :: thesis: 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)))),p,(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)),p,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)))),p,(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)),p,s)))) . k)
then A26: k < ((s . cc) - (s . bb)) + 1 by A1, A3, A4, A23, Th20;
k < ((s . cc) - (s . bb)) + 1 by A1, A3, A4, A23, A25, Th20;
then A27: (((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))),p,((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, Th19;
reconsider scb1 = ((s . cc) - (s . bb)) + 1 as Element of NAT by A26, INT_1:3;
A28: k + 1 <= scb1 by A26, NAT_1:13;
then A29: (((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))),p,((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, Th19;
A30: 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)))),p,(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)),p,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)))),p,(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)),p,s)))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)))) by A15
.= ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))),p,((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 A23, A25, 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)))),p,(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)),p,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)))),p,(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)),p,s)))) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 ) ;
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)))),p,(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)),p,s)))) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) > 0 ; :: thesis: 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)))),p,(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)),p,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)))),p,(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)),p,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)))),p,(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)),p,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)))),p,(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)),p,s)))) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)))) by A15
.= (scb1 - k) - 1 by A24, A29, A31, 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)))),p,(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)),p,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)))),p,(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)),p,s)))) . k) by A30, A27, XREAL_1:146; :: thesis: verum
end;
suppose 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)))),p,(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)),p,s)))) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 ; :: thesis: 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)))),p,(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)),p,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)))),p,(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)),p,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)))),p,((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 A29;
then A33: ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))),p,(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)),p,s)))) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) = 0 by A24, A28, A32, XREAL_1:48;
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)))),p,(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)),p,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)))),p,(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)),p,s)))) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)))) by A15
.= 0 by A33, 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)))),p,(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)),p,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)))),p,(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)),p,s)))) . k) by A22, A25, A30, SCMFSA_M:2; :: thesis: 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)))),p,(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)),p,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)))),p,(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)),p,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)))),p,(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)),p,s)))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 ) ; :: thesis: 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)),p,s),p :: thesis: verum
proof
take f ; :: according to SCMFSA9A:def 5 :: thesis: 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)))),p,(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)),p,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)))),p,(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)),p,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)))),p,(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)),p,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)))),p,(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)),p,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)))),p,(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)),p,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)))),p,(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)),p,s)))) . b1) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 ) by A21; :: thesis: verum
end;
end;

theorem Th25: :: SFMASTR3:25
for s being State of SCM+FSA
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
for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 & k = ((s . cc) - (s . bb)) + 1 & ( ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting ) holds
DataPart (IExec ((for-up (a,bb,cc,Ig)),p,s)) = DataPart ((StepForUp (a,bb,cc,Ig,p,s)) . k)
proof end;

theorem Th26: :: SFMASTR3:26
for s being State of SCM+FSA
for a being read-write Int-Location
for bb, cc being Int-Location
for Ig being good Program of
for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 & ( ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting ) holds
( for-up (a,bb,cc,Ig) is_closed_on s,p & for-up (a,bb,cc,Ig) is_halting_on s,p )
proof end;

begin

definition
let start, finish, minpos be Int-Location;
let f be FinSeq-Location ;
func FinSeqMin (f,start,finish,minpos) -> Program of equals :: SFMASTR3:def 4
(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 4 :
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))))));

:: set aux1 = 1-stRWNotIn {start, finish, min_pos};
:: set aux2 = 2-ndRWNotIn {start, finish, min_pos};
:: set cv = 3-rdRWNotIn {start, finish, min_pos};
registration
let start, finish be Int-Location;
let minpos be read-write Int-Location;
let f be FinSeq-Location ;
cluster FinSeqMin (f,start,finish,minpos) -> good ;
coherence
FinSeqMin (f,start,finish,minpos) is good ;
end;

theorem Th27: :: SFMASTR3:27
for c being read-write Int-Location
for aa, bb being Int-Location
for f being FinSeq-Location st c <> aa holds
not FinSeqMin (f,aa,bb,c) destroys aa
proof end;

theorem Th28: :: SFMASTR3:28
for c being read-write Int-Location
for aa, bb being Int-Location
for f being FinSeq-Location holds {aa,bb,c} c= UsedIntLoc (FinSeqMin (f,aa,bb,c))
proof end;

theorem Th29: :: SFMASTR3:29
for s being State of SCM+FSA
for c being read-write Int-Location
for aa, bb being Int-Location
for f being FinSeq-Location
for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 holds
( FinSeqMin (f,aa,bb,c) is_closed_on s,p & FinSeqMin (f,aa,bb,c) is_halting_on s,p )
proof end;

theorem Th30: :: SFMASTR3:30
for s being State of SCM+FSA
for c being read-write Int-Location
for aa, bb being Int-Location
for f being FinSeq-Location
for p being Instruction-Sequence of SCM+FSA st aa <> c & bb <> c & s . (intloc 0) = 1 holds
( (IExec ((FinSeqMin (f,aa,bb,c)),p,s)) . f = s . f & (IExec ((FinSeqMin (f,aa,bb,c)),p,s)) . aa = s . aa & (IExec ((FinSeqMin (f,aa,bb,c)),p,s)) . bb = s . bb )
proof end;

theorem Th31: :: SFMASTR3:31
for s being State of SCM+FSA
for c being read-write Int-Location
for aa, bb being Int-Location
for f being FinSeq-Location
for p being Instruction-Sequence of SCM+FSA st 1 <= s . aa & s . aa <= s . bb & s . bb <= len (s . f) & aa <> c & bb <> c & s . (intloc 0) = 1 holds
(IExec ((FinSeqMin (f,aa,bb,c)),p,s)) . c = min_at ((s . f),(abs (s . aa)),(abs (s . bb)))
proof end;

begin

definition
let f be FinSeq-Location ;
let a, b be Int-Location;
func swap (f,a,b) -> Program of equals :: SFMASTR3:def 5
((((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 5 :
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}));

registration
let f be FinSeq-Location ;
let a, b be Int-Location;
cluster swap (f,a,b) -> good parahalting ;
coherence
( swap (f,a,b) is good & swap (f,a,b) is parahalting ) ;
end;

theorem Th32: :: SFMASTR3:32
for cc, aa, bb being Int-Location
for f being FinSeq-Location st cc <> 1 -stRWNotIn {aa,bb} & cc <> 2 -ndRWNotIn {aa,bb} holds
not swap (f,aa,bb) destroys cc
proof end;

theorem Th33: :: SFMASTR3:33
for s being State of SCM+FSA
for aa, bb being Int-Location
for f being FinSeq-Location
for p being Instruction-Sequence of SCM+FSA st 1 <= s . aa & s . aa <= len (s . f) & 1 <= s . bb & s . bb <= len (s . f) & s . (intloc 0) = 1 holds
(IExec ((swap (f,aa,bb)),p,s)) . f = ((s . f) +* ((s . aa),((s . f) . (s . bb)))) +* ((s . bb),((s . f) . (s . aa)))
proof end;

theorem :: SFMASTR3:34
for s being State of SCM+FSA
for aa, bb being Int-Location
for f being FinSeq-Location
for p being Instruction-Sequence of SCM+FSA st 1 <= s . aa & s . aa <= len (s . f) & 1 <= s . bb & s . bb <= len (s . f) & s . (intloc 0) = 1 holds
( ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . aa) = (s . f) . (s . bb) & ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . bb) = (s . f) . (s . aa) )
proof end;

theorem Th35: :: SFMASTR3:35
for aa, bb being Int-Location
for f being FinSeq-Location holds {aa,bb} c= UsedIntLoc (swap (f,aa,bb))
proof end;

theorem :: SFMASTR3:36
for aa, bb being Int-Location
for f being FinSeq-Location holds UsedInt*Loc (swap (f,aa,bb)) = {f}
proof end;

begin

definition
let f be FinSeq-Location ;
func Selection-sort f -> Program of equals :: SFMASTR3:def 6
((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 6 :
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 :: SFMASTR3:37
for s being State of SCM+FSA
for f being FinSeq-Location
for p being Instruction-Sequence of SCM+FSA
for S being State of SCM+FSA st S = IExec ((Selection-sort f),p,s) holds
( S . f is_non_decreasing_on 1, len (S . f) & ex p being Permutation of (dom (s . f)) st S . f = (s . f) * p )
proof end;