let s be State of SCM+FSA; for a being read-write Int-Location
for bb, cc being Int-Location
for k being Nat
for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction of SCM+FSA st ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (intloc 0) = 1 & 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)))))) holds
((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (intloc 0) = 1
let a be read-write Int-Location; for bb, cc being Int-Location
for k being Nat
for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction of SCM+FSA st ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (intloc 0) = 1 & 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)))))) holds
((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (intloc 0) = 1
let bb, cc be Int-Location; for k being Nat
for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction of SCM+FSA st ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (intloc 0) = 1 & 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)))))) holds
((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (intloc 0) = 1
let k be Nat; for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction of SCM+FSA st ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (intloc 0) = 1 & 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)))))) holds
((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (intloc 0) = 1
let p be Instruction-Sequence of SCM+FSA; for Ig being really-closed good MacroInstruction of SCM+FSA st ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (intloc 0) = 1 & 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)))))) holds
((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (intloc 0) = 1
let Ig be really-closed good MacroInstruction of SCM+FSA ; ( ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (intloc 0) = 1 & 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)))))) implies ((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (intloc 0) = 1 )
set I = Ig;
assume that
A1:
((StepForUp (a,bb,cc,Ig,p,s)) . k) . (intloc 0) = 1
and
A2:
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))))))
; ((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (intloc 0) = 1
set aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig));
set IB = (Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)));
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;
per cases
( ((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 or ((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 )
;
suppose
((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
;
((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (intloc 0) = 1then
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 ((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 SCMFSA9A:31;
hence
((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (intloc 0) = 1
by A1, SCMFSA_M:2;
verum end; suppose A4:
((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
;
((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (intloc 0) = 1A5:
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 A1, A2, SCMFSA8B:42;
(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 A6:
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 A1, A3, A4, A5, SCMFSA9A:32, SFMASTR1:3;
(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))) . (intloc 0) =
(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))))) . (intloc 0)
by A3, A5, 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)))))))) . (intloc 0)
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)))))) . (intloc 0)
by 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)))) . (intloc 0)
by SCMFSA_2:64
.=
1
by SCMFSA_M:9
;
hence
((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (intloc 0) = 1
by A6, SCMFSA_M:2;
verum end;