let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for I being InitHalting Program of SCM+FSA
for a being read-write Int-Location st s . a > 0 holds
ex s2 being State of SCM+FSA ex k being Element of NAT st
( s2 = s +* (Initialize ((intloc 0) .--> 1)) & k = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3 & IC (Comput ((P +* (while>0 (a,I))),s2,k)) = 0 & ( for b being Int-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . f = (IExec (I,P,s)) . f ) )
let s be State of SCM+FSA; :: thesis: for I being InitHalting Program of SCM+FSA
for a being read-write Int-Location st s . a > 0 holds
ex s2 being State of SCM+FSA ex k being Element of NAT st
( s2 = s +* (Initialize ((intloc 0) .--> 1)) & k = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3 & IC (Comput ((P +* (while>0 (a,I))),s2,k)) = 0 & ( for b being Int-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . f = (IExec (I,P,s)) . f ) )
let I be InitHalting Program of SCM+FSA; :: thesis: for a being read-write Int-Location st s . a > 0 holds
ex s2 being State of SCM+FSA ex k being Element of NAT st
( s2 = s +* (Initialize ((intloc 0) .--> 1)) & k = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3 & IC (Comput ((P +* (while>0 (a,I))),s2,k)) = 0 & ( for b being Int-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . f = (IExec (I,P,s)) . f ) )
set D = Data-Locations SCM+FSA;
let a be read-write Int-Location ; :: thesis: ( s . a > 0 implies ex s2 being State of SCM+FSA ex k being Element of NAT st
( s2 = s +* (Initialize ((intloc 0) .--> 1)) & k = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3 & IC (Comput ((P +* (while>0 (a,I))),s2,k)) = 0 & ( for b being Int-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . f = (IExec (I,P,s)) . f ) ) )
assume A1: s . a > 0 ; :: thesis: ex s2 being State of SCM+FSA ex k being Element of NAT st
( s2 = s +* (Initialize ((intloc 0) .--> 1)) & k = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3 & IC (Comput ((P +* (while>0 (a,I))),s2,k)) = 0 & ( for b being Int-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . f = (IExec (I,P,s)) . f ) )
set Is = Initialize (Initialized s);
set Q = while>0 (a,I);
set s1 = s +* (Initialize ((intloc 0) .--> 1));
set P1 = P +* I;
take s2 = s +* (Initialize ((intloc 0) .--> 1)); :: thesis: ex k being Element of NAT st
( s2 = s +* (Initialize ((intloc 0) .--> 1)) & k = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3 & IC (Comput ((P +* (while>0 (a,I))),s2,k)) = 0 & ( for b being Int-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . f = (IExec (I,P,s)) . f ) )
set P2 = P +* (while>0 (a,I));
take k = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3; :: thesis: ( s2 = s +* (Initialize ((intloc 0) .--> 1)) & k = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3 & IC (Comput ((P +* (while>0 (a,I))),s2,k)) = 0 & ( for b being Int-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . f = (IExec (I,P,s)) . f ) )
thus ( s2 = s +* (Initialize ((intloc 0) .--> 1)) & k = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3 ) ; :: thesis: ( IC (Comput ((P +* (while>0 (a,I))),s2,k)) = 0 & ( for b being Int-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . f = (IExec (I,P,s)) . f ) )
A3: I is_halting_onInit s,P by SCM_HALT:36;
then A4: P +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) by SCM_HALT:def 5;
s +* (Initialize ((intloc 0) .--> 1)) = s +* ((Initialize ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))) by FUNCT_4:99
.= (s +* (Initialize ((intloc 0) .--> 1))) +* (Start-At (0,SCM+FSA)) by FUNCT_4:15
.= Initialize (Initialized s) by SCMFSA6A:def 4 ;
then P +* I halts_on Initialize (Initialized s) by A4;
then A5: I is_halting_on Initialized s,P by SCMFSA7B:def 8;
A6: I is_closed_onInit s,P by SCM_HALT:35;
hence IC (Comput ((P +* (while>0 (a,I))),s2,k)) = 0 by A1, A3, Th21; :: thesis: ( ( for b being Int-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . f = (IExec (I,P,s)) . f ) )
set s4 = Comput ((P +* (while>0 (a,I))),s2,k);
set s3 = Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))));
A7: s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s) by SCMFSA8A:13;
A9: Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))) = Comput ((P +* I),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s))))) by A7;
A10: DataPart (Comput ((P +* (while>0 (a,I))),s2,k)) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) by A1, A3, A6, Th21;

hereby :: thesis: for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . f = (IExec (I,P,s)) . f

let b be Int-Location ; :: thesis: (Comput ((P +* (while>0 (a,I))),s2,k)) . b = (IExec (I,P,s)) . b
thus (Comput ((P +* (while>0 (a,I))),s2,k)) . b = (Comput ((P +* I),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s)))))) . b by A9, A10, SCMFSA6A:38
.= (IExec (I,P,s)) . b by A5, Th10 ; :: thesis: verum

end;

hereby :: thesis: verum

let f be FinSeq-Location ; :: thesis: (Comput ((P +* (while>0 (a,I))),s2,k)) . f = (IExec (I,P,s)) . f
thus (Comput ((P +* (while>0 (a,I))),s2,k)) . f = (Comput ((P +* I),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s)))))) . f by A9, A10, SCMFSA6A:38
.= (IExec (I,P,s)) . f by A5, SCMFSA8C:87 ; :: thesis: verum

end;