set D = Int-Locations \/ FinSeq-Locations ;
set IL = NAT ;
let I be Program of SCM+FSA ; :: thesis: for a being read-write Int-Location
for s being State of SCM+FSA
for k, n being Element of NAT st IC ((StepWhile>0 a,s,I) . k) = insloc 0 & (StepWhile>0 a,s,I) . k = Computation (s +* (Initialized (while>0 a,I))),n & ((StepWhile>0 a,s,I) . k) . (intloc 0 ) = 1 holds
( (StepWhile>0 a,s,I) . k = ((StepWhile>0 a,s,I) . k) +* (Initialized (while>0 a,I)) & (StepWhile>0 a,s,I) . (k + 1) = Computation (s +* (Initialized (while>0 a,I))),(n + ((LifeSpan (((StepWhile>0 a,s,I) . k) +* (Initialized I))) + 3)) )
let a be read-write Int-Location ; :: thesis: for s being State of SCM+FSA
for k, n being Element of NAT st IC ((StepWhile>0 a,s,I) . k) = insloc 0 & (StepWhile>0 a,s,I) . k = Computation (s +* (Initialized (while>0 a,I))),n & ((StepWhile>0 a,s,I) . k) . (intloc 0 ) = 1 holds
( (StepWhile>0 a,s,I) . k = ((StepWhile>0 a,s,I) . k) +* (Initialized (while>0 a,I)) & (StepWhile>0 a,s,I) . (k + 1) = Computation (s +* (Initialized (while>0 a,I))),(n + ((LifeSpan (((StepWhile>0 a,s,I) . k) +* (Initialized I))) + 3)) )
let s be State of SCM+FSA ; :: thesis: for k, n being Element of NAT st IC ((StepWhile>0 a,s,I) . k) = insloc 0 & (StepWhile>0 a,s,I) . k = Computation (s +* (Initialized (while>0 a,I))),n & ((StepWhile>0 a,s,I) . k) . (intloc 0 ) = 1 holds
( (StepWhile>0 a,s,I) . k = ((StepWhile>0 a,s,I) . k) +* (Initialized (while>0 a,I)) & (StepWhile>0 a,s,I) . (k + 1) = Computation (s +* (Initialized (while>0 a,I))),(n + ((LifeSpan (((StepWhile>0 a,s,I) . k) +* (Initialized I))) + 3)) )
let k, n be Element of NAT ; :: thesis: ( IC ((StepWhile>0 a,s,I) . k) = insloc 0 & (StepWhile>0 a,s,I) . k = Computation (s +* (Initialized (while>0 a,I))),n & ((StepWhile>0 a,s,I) . k) . (intloc 0 ) = 1 implies ( (StepWhile>0 a,s,I) . k = ((StepWhile>0 a,s,I) . k) +* (Initialized (while>0 a,I)) & (StepWhile>0 a,s,I) . (k + 1) = Computation (s +* (Initialized (while>0 a,I))),(n + ((LifeSpan (((StepWhile>0 a,s,I) . k) +* (Initialized I))) + 3)) ) )
set s1 = s +* (Initialized (while>0 a,I));
set sk = (StepWhile>0 a,s,I) . k;
set s0k = Initialize ((StepWhile>0 a,s,I) . k);
set At0 = (while>0 a,I) +* (Start-At (insloc 0 ));
set s2 = (Initialize ((StepWhile>0 a,s,I) . k)) +* ((while>0 a,I) +* (Start-At (insloc 0 )));
set s3 = ((StepWhile>0 a,s,I) . k) +* (Initialized (while>0 a,I));
assume A1: IC ((StepWhile>0 a,s,I) . k) = insloc 0 ; :: thesis: ( not (StepWhile>0 a,s,I) . k = Computation (s +* (Initialized (while>0 a,I))),n or not ((StepWhile>0 a,s,I) . k) . (intloc 0 ) = 1 or ( (StepWhile>0 a,s,I) . k = ((StepWhile>0 a,s,I) . k) +* (Initialized (while>0 a,I)) & (StepWhile>0 a,s,I) . (k + 1) = Computation (s +* (Initialized (while>0 a,I))),(n + ((LifeSpan (((StepWhile>0 a,s,I) . k) +* (Initialized I))) + 3)) ) )
assume A2: (StepWhile>0 a,s,I) . k = Computation (s +* (Initialized (while>0 a,I))),n ; :: thesis: ( not ((StepWhile>0 a,s,I) . k) . (intloc 0 ) = 1 or ( (StepWhile>0 a,s,I) . k = ((StepWhile>0 a,s,I) . k) +* (Initialized (while>0 a,I)) & (StepWhile>0 a,s,I) . (k + 1) = Computation (s +* (Initialized (while>0 a,I))),(n + ((LifeSpan (((StepWhile>0 a,s,I) . k) +* (Initialized I))) + 3)) ) )
assume A3: ((StepWhile>0 a,s,I) . k) . (intloc 0 ) = 1 ; :: thesis: ( (StepWhile>0 a,s,I) . k = ((StepWhile>0 a,s,I) . k) +* (Initialized (while>0 a,I)) & (StepWhile>0 a,s,I) . (k + 1) = Computation (s +* (Initialized (while>0 a,I))),(n + ((LifeSpan (((StepWhile>0 a,s,I) . k) +* (Initialized I))) + 3)) )
A4: IC SCM+FSA in dom ((while>0 a,I) +* (Start-At (insloc 0 ))) by SF_MASTR:65;
A5: IC (((StepWhile>0 a,s,I) . k) +* (Initialized (while>0 a,I))) = ((Initialize ((StepWhile>0 a,s,I) . k)) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . (IC SCM+FSA ) by SCMFSA8A:13
.= ((while>0 a,I) +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A4, FUNCT_4:14
.= IC ((StepWhile>0 a,s,I) . k) by A1, SF_MASTR:66 ;
A6: DataPart (((StepWhile>0 a,s,I) . k) +* (Initialized (while>0 a,I))) = DataPart ((Initialize ((StepWhile>0 a,s,I) . k)) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) by SCMFSA8A:13
.= DataPart (Initialize ((StepWhile>0 a,s,I) . k)) by SCMFSA8A:11
.= DataPart ((StepWhile>0 a,s,I) . k) by A1, A3, SCMFSA8C:14 ;
((StepWhile>0 a,s,I) . k) | NAT = (s +* (Initialized (while>0 a,I))) | NAT by A2, AMI_1:123;
then (((StepWhile>0 a,s,I) . k) +* (Initialized (while>0 a,I))) | NAT = ((StepWhile>0 a,s,I) . k) | NAT by FUNCT_4:100;
hence ((StepWhile>0 a,s,I) . k) +* (Initialized (while>0 a,I)) = (StepWhile>0 a,s,I) . k by A5, A6, SCMFSA_9:29; :: thesis: (StepWhile>0 a,s,I) . (k + 1) = Computation (s +* (Initialized (while>0 a,I))),(n + ((LifeSpan (((StepWhile>0 a,s,I) . k) +* (Initialized I))) + 3))
hence (StepWhile>0 a,s,I) . (k + 1) = Computation ((StepWhile>0 a,s,I) . k),((LifeSpan (((StepWhile>0 a,s,I) . k) +* (Initialized I))) + 3) by Def1
.= Computation (s +* (Initialized (while>0 a,I))),(n + ((LifeSpan (((StepWhile>0 a,s,I) . k) +* (Initialized I))) + 3)) by A2, AMI_1:51 ;
:: thesis: verum