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 +* (Initialized (while>0 a,I)) & k = (LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 3 & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for b being Int-Location holds (Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,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 +* (Initialized (while>0 a,I)) & k = (LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 3 & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for b being Int-Location holds (Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) )
set D = Int-Locations \/ FinSeq-Locations ;
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 +* (Initialized (while>0 a,I)) & k = (LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 3 & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for b being Int-Location holds (Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) ) )
assume A1: s . a > 0 ; :: thesis: ex s2 being State of SCM+FSA ex k being Element of NAT st
( s2 = s +* (Initialized (while>0 a,I)) & k = (LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 3 & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for b being Int-Location holds (Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) )
set Is = (Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ));
set P = while>0 a,I;
set s1 = s +* (Initialized I);
take s2 = s +* (Initialized (while>0 a,I)); :: thesis: ex k being Element of NAT st
( s2 = s +* (Initialized (while>0 a,I)) & k = (LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 3 & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for b being Int-Location holds (Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) )
take k = (LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 3; :: thesis: ( s2 = s +* (Initialized (while>0 a,I)) & k = (LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 3 & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for b being Int-Location holds (Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) )
thus ( s2 = s +* (Initialized (while>0 a,I)) & k = (LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 3 ) ; :: thesis: ( IC (Comput (ProgramPart s2),s2,k) = 0 & ( for b being Int-Location holds (Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) )
A2: I is_halting_onInit s by SCM_HALT:36;
then X: ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I) by SCM_HALT:def 5;
s +* (Initialized I) = (Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )) by SCMFSA8A:13;
then ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))) halts_on (Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )) by X;
then A3: I is_halting_on Initialized s by SCMFSA7B:def 8;
A4: I is_closed_onInit s by SCM_HALT:35;
hence IC (Comput (ProgramPart s2),s2,k) = 0 by A1, A2, Th21; :: thesis: ( ( for b being Int-Location holds (Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) )
set s4 = Comput (ProgramPart s2),s2,k;
set s3 = Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)));
X: s +* (Initialized I) = (Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )) by SCMFSA8A:13;
XX: s +* (Initialized I) = (Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )) by SCMFSA8A:13;
A5: Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) = Comput (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) by X
.= Comput (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))) by XX ;
A6: DataPart (Comput (ProgramPart s2),s2,k) = DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) by A1, A2, A4, Th21;

hereby :: thesis: for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f

let b be Int-Location ; :: thesis: (Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b
thus (Comput (ProgramPart s2),s2,k) . b = (Comput (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))))) . b by A5, A6, SCMFSA6A:38
.= (IExec I,s) . b by A3, Th10 ; :: thesis: verum

end;

hereby :: thesis: verum

let f be FinSeq-Location ; :: thesis: (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f
thus (Comput (ProgramPart s2),s2,k) . f = (Comput (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))))) . f by A5, A6, SCMFSA6A:38
.= (IExec I,s) . f by A3, SCMFSA8C:87 ; :: thesis: verum

end;