let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
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,p,s)) . k) . a <= 0 holds
DataPart ((StepWhile>0 (a,I,p,s)) . (k + 1)) = DataPart ((StepWhile>0 (a,I,p,s)) . k)
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,p,s)) . k) . a <= 0 holds
DataPart ((StepWhile>0 (a,I,p,s)) . (k + 1)) = DataPart ((StepWhile>0 (a,I,p,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,p,s)) . k) . a <= 0 holds
DataPart ((StepWhile>0 (a,I,p,s)) . (k + 1)) = DataPart ((StepWhile>0 (a,I,p,s)) . k)
let I be Program of SCM+FSA; :: thesis: for k being Element of NAT st ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 holds
DataPart ((StepWhile>0 (a,I,p,s)) . (k + 1)) = DataPart ((StepWhile>0 (a,I,p,s)) . k)
let k be Element of NAT ; :: thesis: ( ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 implies DataPart ((StepWhile>0 (a,I,p,s)) . (k + 1)) = DataPart ((StepWhile>0 (a,I,p,s)) . k) )
assume A1: ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 ; :: thesis: DataPart ((StepWhile>0 (a,I,p,s)) . (k + 1)) = DataPart ((StepWhile>0 (a,I,p,s)) . k)
set SW = StepWhile>0 (a,I,p,s);
set PW = p +* (while>0 (a,I));
A2: (p +* (while>0 (a,I))) +* (while>0 (a,I)) = p +* (while>0 (a,I)) by FUNCT_4:99;
A3: while>0 (a,I) c= p +* (while>0 (a,I)) by FUNCT_4:26;
A4: Initialize (while>0 (a,I)) c= ((StepWhile>0 (a,I,p,s)) . k) +* (Initialize (while>0 (a,I))) by FUNCT_4:26;
A5: DataPart (((StepWhile>0 (a,I,p,s)) . k) +* (Initialize (while>0 (a,I)))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) by SCMFSA8A:11;
then A6: ((StepWhile>0 (a,I,p,s)) . k) . a = (((StepWhile>0 (a,I,p,s)) . k) +* (Initialize (while>0 (a,I)))) . a by SCMFSA6A:38;
thus DataPart ((StepWhile>0 (a,I,p,s)) . (k + 1)) = DataPart (Comput (((p +* (while>0 (a,I))) +* (while>0 (a,I))),(((StepWhile>0 (a,I,p,s)) . k) +* (Initialize (while>0 (a,I)))),((LifeSpan (((p +* (while>0 (a,I))) +* I),(((StepWhile>0 (a,I,p,s)) . k) +* (Initialize I)))) + 3))) by SCMFSA_9:def 5, A2
.= DataPart ((StepWhile>0 (a,I,p,s)) . k) by A1, A5, A6, A4, Th35, A2, A3 ; :: thesis: verum