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