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 (ProgramPart (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )))),(((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 (ProgramPart (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )))),(((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 (ProgramPart (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )))),(((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 (ProgramPart (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)) ) )
set D = Int-Locations \/ FinSeq-Locations ;
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 (ProgramPart (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )))),(((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 (ProgramPart (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)) )
then ProgramPart ((StepWhile>0 a,I,s) . k) = ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) 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) & ProgramPart (((StepWhile>0 a,I,s) . k) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart ((StepWhile>0 a,I,s) . k) ) 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:123;
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 )
.= ((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 (ProgramPart (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )))),(((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 (ProgramPart (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3) by Def5, 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 (ProgramPart (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)) by A3, AMI_1:51 ;
:: thesis: verum