let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for I being Program of SCM+FSA
for k being Element of NAT st ((StepWhile=0 (a,I,s)) . k) . a <> 0 holds
DataPart ((StepWhile=0 (a,I,s)) . (k + 1)) = DataPart ((StepWhile=0 (a,I,s)) . k)
let a be read-write Int-Location ; :: thesis: for I being Program of SCM+FSA
for k being Element of NAT st ((StepWhile=0 (a,I,s)) . k) . a <> 0 holds
DataPart ((StepWhile=0 (a,I,s)) . (k + 1)) = DataPart ((StepWhile=0 (a,I,s)) . k)
let I be Program of SCM+FSA; :: thesis: for k being Element of NAT st ((StepWhile=0 (a,I,s)) . k) . a <> 0 holds
DataPart ((StepWhile=0 (a,I,s)) . (k + 1)) = DataPart ((StepWhile=0 (a,I,s)) . k)
let k be Element of NAT ; :: thesis: ( ((StepWhile=0 (a,I,s)) . k) . a <> 0 implies DataPart ((StepWhile=0 (a,I,s)) . (k + 1)) = DataPart ((StepWhile=0 (a,I,s)) . k) )
assume A1: ((StepWhile=0 (a,I,s)) . k) . a <> 0 ; :: thesis: DataPart ((StepWhile=0 (a,I,s)) . (k + 1)) = DataPart ((StepWhile=0 (a,I,s)) . k)
set SW = StepWhile=0 (a,I,s);
A2: (while=0 (a,I)) +* (Start-At (0,SCM+FSA)) c= ((StepWhile=0 (a,I,s)) . k) +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
A3: DataPart (((StepWhile=0 (a,I,s)) . k) +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))) = DataPart ((StepWhile=0 (a,I,s)) . k) by SCMFSA8A:11;
then A4: ((StepWhile=0 (a,I,s)) . k) . a = (((StepWhile=0 (a,I,s)) . k) +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))) . a by SCMFSA6A:38;
thus DataPart ((StepWhile=0 (a,I,s)) . (k + 1)) = DataPart (Comput ((ProgramPart (((StepWhile=0 (a,I,s)) . k) +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(((StepWhile=0 (a,I,s)) . k) +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (((StepWhile=0 (a,I,s)) . k) +* (I +* (Start-At (0,SCM+FSA))))),(((StepWhile=0 (a,I,s)) . k) +* (I +* (Start-At (0,SCM+FSA)))))) + 3))) by SCMFSA_9:def 4
.= DataPart ((StepWhile=0 (a,I,s)) . k) by A1, A3, A4, A2, Th22 ; :: thesis: verum