set D = Int-Locations \/ FinSeq-Locations ;
let I be Program of ; :: thesis: for a being read-write Int-Location
for s being State of
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
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 ; :: 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)) ) )
A2: IC SCM+FSA in dom ((while=0 a,I) +* (Start-At (insloc 0 ))) by SF_MASTR:65;
assume A3: (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)) )
then ((StepWhile=0 a,I,s) . k) | NAT = (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))) | NAT by AMI_1:123;
then A4: ( DataPart (((StepWhile=0 a,I,s) . k) +* ((while=0 a,I) +* (Start-At (insloc 0 )))) = DataPart ((StepWhile=0 a,I,s) . k) & (((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, SCMFSA8A:11;
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 A2, FUNCT_4:14
.= IC ((StepWhile=0 a,I,s) . k) by A1, SF_MASTR:66 ;
hence ((StepWhile=0 a,I,s) . k) +* ((while=0 a,I) +* (Start-At (insloc 0 ))) = (StepWhile=0 a,I,s) . k by A4, 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 A3, AMI_1:51 ;
:: thesis: verum