let p be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for a being read-write Int-Location
for I being MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & s . a <= 0 holds
DataPart (IExec ((while>0 (a,I)),p,s)) = DataPart s
let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for I being MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & s . a <= 0 holds
DataPart (IExec ((while>0 (a,I)),p,s)) = DataPart s
let a be read-write Int-Location; :: thesis: for I being MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & s . a <= 0 holds
DataPart (IExec ((while>0 (a,I)),p,s)) = DataPart s
let I be MacroInstruction of SCM+FSA ; :: thesis: ( s . (intloc 0) = 1 & s . a <= 0 implies DataPart (IExec ((while>0 (a,I)),p,s)) = DataPart s )
assume that
A1: s . (intloc 0) = 1 and
A2: s . a <= 0 ; :: thesis: DataPart (IExec ((while>0 (a,I)),p,s)) = DataPart s
set WH = while>0 (a,I);
set Is = Initialized s;
set pds = p +* (while>0 (a,I));
A3: while>0 (a,I) c= p +* (while>0 (a,I)) by FUNCT_4:25;
A4: Initialized s = Initialize (Initialized s) by MEMSTR_0:44;
(Initialized s) . a = s . a by SCMFSA_M:37;
then while>0 (a,I) is_halting_on Initialized s,p by A2, SCMFSA_9:38;
then A5: p +* (while>0 (a,I)) halts_on Initialized s by A4, SCMFSA7B:def 7;
A6: (Initialized s) . a = s . a by SCMFSA_M:37;
thus DataPart (IExec ((while>0 (a,I)),p,s)) = DataPart (Result ((p +* (while>0 (a,I))),(Initialized s))) by SCMFSA6B:def 1
.= DataPart (Comput ((p +* (while>0 (a,I))),(Initialized s),(LifeSpan ((p +* (while>0 (a,I))),(Initialized s))))) by A5, EXTPRO_1:23
.= DataPart (Initialized s) by A2, A6, Th29, A3
.= DataPart s by A1, SCMFSA_M:19 ; :: thesis: verum