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