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 D = Int-Locations \/ FinSeq-Locations ;
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 Def4
.= 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