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,I,s) . k) = insloc 0 & (StepWhile>0 a,I,s) . k = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),n holds
( (StepWhile>0 a,I,s) . k = ((StepWhile>0 a,I,s) . k) +* ((while>0 a,I) +* (Start-At (insloc 0 ))) & (StepWhile>0 a,I,s) . (k + 1) = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(n + ((LifeSpan (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At (insloc 0 ))))) + 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,I,s) . k) = insloc 0 & (StepWhile>0 a,I,s) . k = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),n holds
( (StepWhile>0 a,I,s) . k = ((StepWhile>0 a,I,s) . k) +* ((while>0 a,I) +* (Start-At (insloc 0 ))) & (StepWhile>0 a,I,s) . (k + 1) = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(n + ((LifeSpan (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At (insloc 0 ))))) + 3)) )
let s be State of SCM+FSA ; :: thesis: for k, n being Element of NAT st IC ((StepWhile>0 a,I,s) . k) = insloc 0 & (StepWhile>0 a,I,s) . k = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),n holds
( (StepWhile>0 a,I,s) . k = ((StepWhile>0 a,I,s) . k) +* ((while>0 a,I) +* (Start-At (insloc 0 ))) & (StepWhile>0 a,I,s) . (k + 1) = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(n + ((LifeSpan (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At (insloc 0 ))))) + 3)) )
let k, n be Element of NAT ; :: thesis: ( IC ((StepWhile>0 a,I,s) . k) = insloc 0 & (StepWhile>0 a,I,s) . k = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),n implies ( (StepWhile>0 a,I,s) . k = ((StepWhile>0 a,I,s) . k) +* ((while>0 a,I) +* (Start-At (insloc 0 ))) & (StepWhile>0 a,I,s) . (k + 1) = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(n + ((LifeSpan (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At (insloc 0 ))))) + 3)) ) )
set s1 = s +* ((while>0 a,I) +* (Start-At (insloc 0 )));
set sk = (StepWhile>0 a,I,s) . k;
set s2 = ((StepWhile>0 a,I,s) . k) +* ((while>0 a,I) +* (Start-At (insloc 0 )));
assume A1: IC ((StepWhile>0 a,I,s) . k) = insloc 0 ; :: thesis: ( not (StepWhile>0 a,I,s) . k = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),n or ( (StepWhile>0 a,I,s) . k = ((StepWhile>0 a,I,s) . k) +* ((while>0 a,I) +* (Start-At (insloc 0 ))) & (StepWhile>0 a,I,s) . (k + 1) = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(n + ((LifeSpan (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At (insloc 0 ))))) + 3)) ) )
assume A2: (StepWhile>0 a,I,s) . k = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),n ; :: thesis: ( (StepWhile>0 a,I,s) . k = ((StepWhile>0 a,I,s) . k) +* ((while>0 a,I) +* (Start-At (insloc 0 ))) & (StepWhile>0 a,I,s) . (k + 1) = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(n + ((LifeSpan (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At (insloc 0 ))))) + 3)) )
A3: IC SCM+FSA in dom ((while>0 a,I) +* (Start-At (insloc 0 ))) by SF_MASTR:65;
A4: IC (((StepWhile>0 a,I,s) . k) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) = (((StepWhile>0 a,I,s) . k) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . (IC SCM+FSA ) by AMI_1:def 15
.= ((while>0 a,I) +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A3, FUNCT_4:14
.= IC ((StepWhile>0 a,I,s) . k) by A1, SF_MASTR:66 ;
A5: DataPart (((StepWhile>0 a,I,s) . k) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) = DataPart ((StepWhile>0 a,I,s) . k) by SCMFSA8A:11;
((StepWhile>0 a,I,s) . k) | NAT = (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))) | NAT by A2, AMI_1:123;
then (((StepWhile>0 a,I,s) . k) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) | NAT = ((StepWhile>0 a,I,s) . k) | NAT by FUNCT_4:100;
hence ((StepWhile>0 a,I,s) . k) +* ((while>0 a,I) +* (Start-At (insloc 0 ))) = (StepWhile>0 a,I,s) . k by A4, A5, Th29; :: thesis: (StepWhile>0 a,I,s) . (k + 1) = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(n + ((LifeSpan (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At (insloc 0 ))))) + 3))
hence (StepWhile>0 a,I,s) . (k + 1) = Computation ((StepWhile>0 a,I,s) . k),((LifeSpan (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At (insloc 0 ))))) + 3) by Def5
.= Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(n + ((LifeSpan (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At (insloc 0 ))))) + 3)) by A2, AMI_1:51 ;
:: thesis: verum