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 (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)) by SCMFSA_9:def 5
.= DataPart ((StepWhile>0 a,I,s) . k) by A1, A3, A4, A2, Th35 ; :: thesis: verum