let s be State of SCM+FSA ; :: thesis: for a being read-write Int-Location
for bb, cc being Int-Location
for Ig being good Program of SCM+FSA
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 )
let a be read-write Int-Location ; :: thesis: for bb, cc being Int-Location
for Ig being good Program of SCM+FSA
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 )
let bb, cc be Int-Location ; :: thesis: for Ig being good Program of SCM+FSA
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 )
let Ig be good Program of SCM+FSA ; :: thesis: 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 )
let k be Element of NAT ; :: thesis: ( s . (intloc 0 ) = 1 & ProperForUpBody a,bb,cc,Ig,s & k < ((s . cc) - (s . bb)) + 1 implies ((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 ) )
set FL = FinSeq-Locations ;
set D = Int-Locations \/ FinSeq-Locations ;
set I = Ig;
assume that
A1: s . (intloc 0 ) = 1 and
A2: ProperForUpBody a,bb,cc,Ig,s and
A3: k < ((s . cc) - (s . bb)) + 1 ; :: thesis: ((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 )
set SF = StepForUp a,bb,cc,Ig,s;
set aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig));
set IB = (Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ));
set s2 = (s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb);
set SW2 = StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb));
set scb1 = ((s . cc) - (s . bb)) + 1;
set Iloc = {a,bb,cc} \/ (UsedIntLoc Ig);
A4: StepForUp a,bb,cc,Ig,s = StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb)) ;
A5: (Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 )) = Ig ';' ((AddTo a,(intloc 0 )) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))) by SCMFSA6A:70;
A6: (((StepForUp a,bb,cc,Ig,s) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + k = ((s . cc) - (s . bb)) + 1 by A1, A2, A3, Th25;
A7: Ig is_closed_on (StepForUp a,bb,cc,Ig,s) . k by A2, A3, Def7;
A8: Ig is_halting_on (StepForUp a,bb,cc,Ig,s) . k by A2, A3, Def7;
A9: ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) . (intloc 0 ) = 1 by A1, A2, A3, A4, Th25;
A10: ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0

proof

assume ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) <= 0 ; :: thesis: contradiction
then (((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + k < 0 + (((s . cc) - (s . bb)) + 1) by A3, XREAL_1:10;
hence contradiction by A6; :: thesis: verum

end;

A11: Ig is_closed_on Initialize ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) by A7, A9, SFMASTR2:4;
A12: Ig is_halting_on Initialize ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) by A7, A8, A9, SFMASTR2:5;
A13: (AddTo a,(intloc 0 )) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 )) is_closed_on IExec Ig,((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) by SCMFSA7B:24;
A14: (AddTo a,(intloc 0 )) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 )) is_halting_on IExec Ig,((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) by SCMFSA7B:25;
A15: (Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 )) is_closed_on Initialize ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) by A5, A11, A12, A13, SFMASTR1:3;
A16: DataPart ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . (k + 1)) = DataPart (IExec ((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)) by A9, A10, A15, A5, A11, A12, A13, A14, SCMFSA9A:38, SFMASTR1:4;
set IB1 = Ig ';' (AddTo a,(intloc 0 ));
set S1 = IExec (Ig ';' (AddTo a,(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k);
set S2 = IExec ((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k);
A18: Macro (AddTo a,(intloc 0 )) is_closed_on IExec Ig,((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) by SCMFSA7B:24;
A19: Macro (AddTo a,(intloc 0 )) is_halting_on IExec Ig,((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) by SCMFSA7B:25;
A21: Ig ';' (AddTo a,(intloc 0 )) is_halting_on Initialize ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) by A11, A12, A18, A19, SFMASTR1:4;

now

hereby :: thesis: for x being FinSeq-Location holds (IExec (Ig ';' (AddTo a,(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)) . x = (IExec ((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)) . x

let x be Int-Location ; :: thesis: ( x in {a,bb,cc} \/ (UsedIntLoc Ig) implies (IExec (Ig ';' (AddTo a,(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)) . x = (IExec ((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)) . x )
assume x in {a,bb,cc} \/ (UsedIntLoc Ig) ; :: thesis: (IExec (Ig ';' (AddTo a,(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)) . x = (IExec ((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)) . x
then A22: x <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)) by SFMASTR1:21;
(IExec ((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)) . x = (Exec (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 )),(IExec (Ig ';' (AddTo a,(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k))) . x by A11, A12, A18, A21, SFMASTR1:3, SFMASTR1:12
.= (IExec (Ig ';' (AddTo a,(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)) . x by A22, SCMFSA_2:91 ;
hence (IExec (Ig ';' (AddTo a,(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)) . x = (IExec ((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)) . x ; :: thesis: verum

end;

let x be FinSeq-Location ; :: thesis: (IExec (Ig ';' (AddTo a,(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)) . x = (IExec ((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)) . x
(IExec ((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)) . x = (Exec (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 )),(IExec (Ig ';' (AddTo a,(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k))) . x by A11, A12, A18, A21, SFMASTR1:3, SFMASTR1:13
.= (IExec (Ig ';' (AddTo a,(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)) . x by SCMFSA_2:91 ;
hence (IExec (Ig ';' (AddTo a,(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)) . x = (IExec ((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)) . x ; :: thesis: verum

end;

then (IExec (Ig ';' (AddTo a,(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations ) = (IExec ((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations ) by SFMASTR2:7;
hence ((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 ) by A16, RELAT_1:188, SCMFSA_2:127, XBOOLE_1:9; :: thesis: verum