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 Ig being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s,p holds
for k being 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} \/ (UsedILoc Ig)))) + k = ((s . cc) - (s . bb)) + 1 )
let a be read-write Int-Location; :: thesis: for bb, cc being Int-Location
for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s,p holds
for k being 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} \/ (UsedILoc Ig)))) + k = ((s . cc) - (s . bb)) + 1 )
let bb, cc be Int-Location; :: thesis: for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s,p holds
for k being 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} \/ (UsedILoc Ig)))) + k = ((s . cc) - (s . bb)) + 1 )
let p be Instruction-Sequence of SCM+FSA; :: thesis: for Ig being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s,p holds
for k being 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} \/ (UsedILoc Ig)))) + k = ((s . cc) - (s . bb)) + 1 )
let Ig be really-closed good MacroInstruction of SCM+FSA ; :: thesis: ( s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s,p implies for k being 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} \/ (UsedILoc Ig)))) + k = ((s . cc) - (s . bb)) + 1 ) )
set I = Ig;
assume that
A1: s . (intloc 0) = 1 and
A2: ProperForUpBody a,bb,cc,Ig,s,p ; :: thesis: for k being 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} \/ (UsedILoc Ig)))) + k = ((s . cc) - (s . bb)) + 1 )
set scb1 = ((s . cc) - (s . bb)) + 1;
set aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig));
set SF = StepForUp (a,bb,cc,Ig,p,s);
set IB = (Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)));
set s2 = (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb));
set p2 = p;
set SW2 = StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))));
A3: (Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))) = Ig ";" ((AddTo (a,(intloc 0))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))) by SCMFSA6A:28;
defpred S1[ Nat] means ( $1 <= ((s . cc) - (s . bb)) + 1 implies ( ((StepForUp (a,bb,cc,Ig,p,s)) . $1) . (intloc 0) = 1 & ( not Ig destroys a implies ( ((StepForUp (a,bb,cc,Ig,p,s)) . $1) . a = $1 + (s . bb) & ((StepForUp (a,bb,cc,Ig,p,s)) . $1) . a <= (s . cc) + 1 ) ) & (((StepForUp (a,bb,cc,Ig,p,s)) . $1) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)))) + $1 = ((s . cc) - (s . bb)) + 1 ) );
a in {a,bb,cc} by ENUMSET1:def 1;
then a in {a,bb,cc} \/ (UsedILoc Ig) by XBOOLE_0:def 3;
then A4: 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)) <> a by SCMFSA_M:25;
A5: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A6: S1[k] ; :: thesis: S1[k + 1]
thus S1[k + 1] :: thesis: verum
proof
A7: not 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)) in UsedILoc Ig
proof
assume 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)) in UsedILoc Ig ; :: thesis: contradiction
then 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)) in {a,bb,cc} \/ (UsedILoc Ig) by XBOOLE_0:def 3;
hence contradiction by SCMFSA_M:25; :: thesis: verum
end;
set k1 = k + 1;
assume A8: k + 1 <= ((s . cc) - (s . bb)) + 1 ; :: thesis: ( ((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (intloc 0) = 1 & ( not Ig destroys a implies ( ((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . a = (k + 1) + (s . bb) & ((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . a <= (s . cc) + 1 ) ) & (((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)))) + (k + 1) = ((s . cc) - (s . bb)) + 1 )
A9: k < k + 1 by XREAL_1:29;
then A10: ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) > 0 by A6, A8, XREAL_1:8, XXREAL_0:2;
A11: k < ((s . cc) - (s . bb)) + 1 by A8, A9, XXREAL_0:2;
A12: Ig is_halting_on (StepForUp (a,bb,cc,Ig,p,s)) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))))) by A2, A11;
then A13: Ig is_halting_on Initialized ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k),p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))))) by A6, A8, A9, SCMFSA8B:42, XXREAL_0:2;
thus ((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (intloc 0) = 1 by A6, A8, A9, A12, Th16, XXREAL_0:2; :: thesis: ( ( not Ig destroys a implies ( ((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . a = (k + 1) + (s . bb) & ((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . a <= (s . cc) + 1 ) ) & (((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)))) + (k + 1) = ((s . cc) - (s . bb)) + 1 )
(AddTo (a,(intloc 0))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))) is_halting_on IExec (Ig,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)),p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))))) by SCMFSA7B:19;
then (Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))) is_halting_on Initialized ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k),p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))))) by A3, A13, SFMASTR1:3;
then A14: DataPart ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . (k + 1)) = DataPart (IExec (((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) by A6, A8, A9, A10, SCMFSA9A:32, XXREAL_0:2;
hereby :: thesis: (((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)))) + (k + 1) = ((s . cc) - (s . bb)) + 1
assume A15: not Ig destroys a ; :: thesis: ( ((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . a = (k + 1) + (s . bb) & ((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . a <= (s . cc) + 1 )
A16: (IExec (((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . a = (IExec (((AddTo (a,(intloc 0))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),(IExec (Ig,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))))) . a by A3, A13, SFMASTR1:7
.= (Exec ((SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))),(Exec ((AddTo (a,(intloc 0))),(Initialized (IExec (Ig,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))))))) . a by SCMFSA6C:8
.= (Exec ((AddTo (a,(intloc 0))),(Initialized (IExec (Ig,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))))) . a by A4, SCMFSA_2:65
.= ((Initialized (IExec (Ig,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))) . a) + ((Initialized (IExec (Ig,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))) . (intloc 0)) by SCMFSA_2:64
.= ((Initialized (IExec (Ig,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))) . a) + 1 by SCMFSA_M:9
.= ((IExec (Ig,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . a) + 1 by SCMFSA_M:37
.= ((Initialized ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)) . a) + 1 by A13, A15, SCMFSA8C:95
.= (((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k) . a) + 1 by SCMFSA_M:37 ;
hence ((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . a = (k + 1) + (s . bb) by A6, A8, A9, A14, A15, SCMFSA_M:2, XXREAL_0:2; :: thesis: ((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . a <= (s . cc) + 1
(k + 1) + (s . bb) <= (((s . cc) + 1) - (s . bb)) + (s . bb) by A8, XREAL_1:6;
hence ((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . a <= (s . cc) + 1 by A6, A8, A9, A14, A15, A16, SCMFSA_M:2, XXREAL_0:2; :: thesis: verum
end;
(IExec (((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) = (IExec (((AddTo (a,(intloc 0))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),(IExec (Ig,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) by A3, A13, SFMASTR1:7
.= (Exec ((SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))),(Exec ((AddTo (a,(intloc 0))),(Initialized (IExec (Ig,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))))))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) by SCMFSA6C:8
.= ((Exec ((AddTo (a,(intloc 0))),(Initialized (IExec (Ig,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)))) - ((Exec ((AddTo (a,(intloc 0))),(Initialized (IExec (Ig,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))))) . (intloc 0)) by SCMFSA_2:65
.= ((Exec ((AddTo (a,(intloc 0))),(Initialized (IExec (Ig,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)))) - ((Initialized (IExec (Ig,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))) . (intloc 0)) by SCMFSA_2:64
.= ((Exec ((AddTo (a,(intloc 0))),(Initialized (IExec (Ig,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)))) - 1 by SCMFSA_M:9
.= ((Initialized (IExec (Ig,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)))) - 1 by A4, SCMFSA_2:64
.= ((IExec (Ig,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)))) - 1 by SCMFSA_M:37
.= ((Initialized ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)))) - 1 by A13, A7, SCMFSA8C:95, SFMASTR1:1
.= (((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)))) - 1 by SCMFSA_M:37 ;
hence (((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)))) + (k + 1) = ((((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)))) - 1) + (k + 1) by A14, SCMFSA_M:2
.= ((s . cc) - (s . bb)) + 1 by A6, A8, A9, XXREAL_0:2 ;
:: thesis: verum
end;
end;
A17: a in dom (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) by SCMFSA_2:42;
A18: 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)) in dom s by SCMFSA_2:42;
A19: S1[ 0 ]
proof
assume A20: 0 <= ((s . cc) - (s . bb)) + 1 ; :: thesis: ( ((StepForUp (a,bb,cc,Ig,p,s)) . 0) . (intloc 0) = 1 & ( not Ig destroys a implies ( ((StepForUp (a,bb,cc,Ig,p,s)) . 0) . a = 0 + (s . bb) & ((StepForUp (a,bb,cc,Ig,p,s)) . 0) . a <= (s . cc) + 1 ) ) & (((StepForUp (a,bb,cc,Ig,p,s)) . 0) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)))) + 0 = ((s . cc) - (s . bb)) + 1 )
A21: (StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . 0 = (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)) by SCMFSA_9:def 5;
hence ((StepForUp (a,bb,cc,Ig,p,s)) . 0) . (intloc 0) = (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) . (intloc 0) by FUNCT_7:32
.= 1 by A1, FUNCT_7:32 ;
:: thesis: ( ( not Ig destroys a implies ( ((StepForUp (a,bb,cc,Ig,p,s)) . 0) . a = 0 + (s . bb) & ((StepForUp (a,bb,cc,Ig,p,s)) . 0) . a <= (s . cc) + 1 ) ) & (((StepForUp (a,bb,cc,Ig,p,s)) . 0) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)))) + 0 = ((s . cc) - (s . bb)) + 1 )
hereby :: thesis: (((StepForUp (a,bb,cc,Ig,p,s)) . 0) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)))) + 0 = ((s . cc) - (s . bb)) + 1
assume not Ig destroys a ; :: thesis: ( ((StepForUp (a,bb,cc,Ig,p,s)) . 0) . a = 0 + (s . bb) & ((StepForUp (a,bb,cc,Ig,p,s)) . 0) . a <= (s . cc) + 1 )
thus ((StepForUp (a,bb,cc,Ig,p,s)) . 0) . a = 0 + (s . bb) by A17, A21, FUNCT_7:31; :: thesis: ((StepForUp (a,bb,cc,Ig,p,s)) . 0) . a <= (s . cc) + 1
0 + (s . bb) <= (((s . cc) + 1) - (s . bb)) + (s . bb) by A20, XREAL_1:6;
hence ((StepForUp (a,bb,cc,Ig,p,s)) . 0) . a <= (s . cc) + 1 by A17, A21, FUNCT_7:31; :: thesis: verum
end;
thus (((StepForUp (a,bb,cc,Ig,p,s)) . 0) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)))) + 0 = (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) by A4, A21, FUNCT_7:32
.= ((s . cc) - (s . bb)) + 1 by A18, FUNCT_7:31 ; :: thesis: verum
end;
thus for k being Nat holds S1[k] from NAT_1:sch 2(A19, A5); :: thesis: verum