let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA

for I being InitHalting really-closed MacroInstruction 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 Nat st

( s2 = Initialized s & k = (LifeSpan ((P +* I),(Initialized s))) + 2 & 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 really-closed MacroInstruction 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 Nat st

( s2 = Initialized s & k = (LifeSpan ((P +* I),(Initialized s))) + 2 & 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 really-closed MacroInstruction 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 Nat st

( s2 = Initialized s & k = (LifeSpan ((P +* I),(Initialized s))) + 2 & 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 ;

let a be read-write Int-Location; :: thesis: ( s . a > 0 implies ex s2 being State of SCM+FSA ex k being Nat st

( s2 = Initialized s & k = (LifeSpan ((P +* I),(Initialized s))) + 2 & 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 Nat st

( s2 = Initialized s & k = (LifeSpan ((P +* I),(Initialized s))) + 2 & 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 = Initialized s;

set P1 = P +* I;

take Initialized s ; :: thesis: ex k being Nat st

( Initialized s = Initialized s & k = (LifeSpan ((P +* I),(Initialized s))) + 2 & IC (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) = 0 & ( for b being Int-Location holds (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) . f = (IExec (I,P,s)) . f ) )

set P2 = P +* (while>0 (a,I));

take k = (LifeSpan ((P +* I),(Initialized s))) + 2; :: thesis: ( Initialized s = Initialized s & k = (LifeSpan ((P +* I),(Initialized s))) + 2 & IC (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) = 0 & ( for b being Int-Location holds (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) . f = (IExec (I,P,s)) . f ) )

thus ( Initialized s = Initialized s & k = (LifeSpan ((P +* I),(Initialized s))) + 2 ) ; :: thesis: ( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) = 0 & ( for b being Int-Location holds (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) . f = (IExec (I,P,s)) . f ) )

A2: I is_halting_onInit s,P by SCM_HALT:26;

then A3: P +* I halts_on Initialized s ;

Initialized s = Initialize (Initialized s) by MEMSTR_0:44

.= Initialize (Initialized s)

.= Initialize (Initialized s) ;

then P +* I halts_on Initialize (Initialized s) by A3;

then A4: I is_halting_on Initialized s,P by SCMFSA7B:def 7;

thus IC (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) = 0 by A1, A2, SCM_HALT:74; :: thesis: ( ( for b being Int-Location holds (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) . f = (IExec (I,P,s)) . f ) )

set s4 = Comput ((P +* (while>0 (a,I))),(Initialized s),k);

set s3 = Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))));

A5: Initialized s = Initialize (Initialized s) by MEMSTR_0:44;

A6: Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))) = Comput ((P +* I),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s))))) by A5;

A7: DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) = DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) by A1, A2, SCM_HALT:74;

for I being InitHalting really-closed MacroInstruction 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 Nat st

( s2 = Initialized s & k = (LifeSpan ((P +* I),(Initialized s))) + 2 & 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 really-closed MacroInstruction 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 Nat st

( s2 = Initialized s & k = (LifeSpan ((P +* I),(Initialized s))) + 2 & 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 really-closed MacroInstruction 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 Nat st

( s2 = Initialized s & k = (LifeSpan ((P +* I),(Initialized s))) + 2 & 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 ;

let a be read-write Int-Location; :: thesis: ( s . a > 0 implies ex s2 being State of SCM+FSA ex k being Nat st

( s2 = Initialized s & k = (LifeSpan ((P +* I),(Initialized s))) + 2 & 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 Nat st

( s2 = Initialized s & k = (LifeSpan ((P +* I),(Initialized s))) + 2 & 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 = Initialized s;

set P1 = P +* I;

take Initialized s ; :: thesis: ex k being Nat st

( Initialized s = Initialized s & k = (LifeSpan ((P +* I),(Initialized s))) + 2 & IC (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) = 0 & ( for b being Int-Location holds (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) . f = (IExec (I,P,s)) . f ) )

set P2 = P +* (while>0 (a,I));

take k = (LifeSpan ((P +* I),(Initialized s))) + 2; :: thesis: ( Initialized s = Initialized s & k = (LifeSpan ((P +* I),(Initialized s))) + 2 & IC (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) = 0 & ( for b being Int-Location holds (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) . f = (IExec (I,P,s)) . f ) )

thus ( Initialized s = Initialized s & k = (LifeSpan ((P +* I),(Initialized s))) + 2 ) ; :: thesis: ( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) = 0 & ( for b being Int-Location holds (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) . f = (IExec (I,P,s)) . f ) )

A2: I is_halting_onInit s,P by SCM_HALT:26;

then A3: P +* I halts_on Initialized s ;

Initialized s = Initialize (Initialized s) by MEMSTR_0:44

.= Initialize (Initialized s)

.= Initialize (Initialized s) ;

then P +* I halts_on Initialize (Initialized s) by A3;

then A4: I is_halting_on Initialized s,P by SCMFSA7B:def 7;

thus IC (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) = 0 by A1, A2, SCM_HALT:74; :: thesis: ( ( for b being Int-Location holds (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) . f = (IExec (I,P,s)) . f ) )

set s4 = Comput ((P +* (while>0 (a,I))),(Initialized s),k);

set s3 = Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))));

A5: Initialized s = Initialize (Initialized s) by MEMSTR_0:44;

A6: Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))) = Comput ((P +* I),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s))))) by A5;

A7: DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) = DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) by A1, A2, SCM_HALT:74;

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

let b be Int-Location; :: thesis: (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) . b = (IExec (I,P,s)) . b

thus (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) . b = (Comput ((P +* I),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s)))))) . b by A6, A7, SCMFSA_M:2

.= (IExec (I,P,s)) . b by A4, Th1 ; :: thesis: verum

end;thus (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) . b = (Comput ((P +* I),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s)))))) . b by A6, A7, SCMFSA_M:2

.= (IExec (I,P,s)) . b by A4, Th1 ; :: thesis: verum

hereby :: thesis: verum

let f be FinSeq-Location ; :: thesis: (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) . f = (IExec (I,P,s)) . f

thus (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) . f = (Comput ((P +* I),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s)))))) . f by A6, A7, SCMFSA_M:2

.= (IExec (I,P,s)) . f by A4, SCMFSA8C:58 ; :: thesis: verum

end;thus (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) . f = (Comput ((P +* I),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s)))))) . f by A6, A7, SCMFSA_M:2

.= (IExec (I,P,s)) . f by A4, SCMFSA8C:58 ; :: thesis: verum