let s be State of SCM+FSA ; :: thesis:
let a be read-write Int-Location ; :: thesis:
let I be Program of SCM+FSA ; :: thesis:
assume A1: for k being Element of NAT st ((StepWhile=0 a,I,s) . k) . a = 0 holds
( I is_closed_on (StepWhile=0 a,I,s) . k & I is_halting_on (StepWhile=0 a,I,s) . k ) ; :: according to SCMFSA9A:def 1 :: thesis:
given f being Function of (product the Object-Kind of SCM+FSA ),NAT such that A2: for k being Element of NAT holds
( f . ((StepWhile=0 a,I,s) . (k + 1)) < f . ((StepWhile=0 a,I,s) . k) or ((StepWhile=0 a,I,s) . k) . a <> 0 ) ; :: according to SCMFSA9A:def 2 :: thesis:
deffunc H₁( Element of NAT ) -> Element of NAT = f . ((StepWhile=0 a,I,s) . $1);
defpred S₁[ Element of NAT ] means ((StepWhile=0 a,I,s) . $1) . a <> 0 ;
set s1 = s +* ((while=0 a,I) +* (Start-At (insloc 0 )));
A3: for k being Element of NAT holds
( H₁(k + 1) < H₁(k) or S₁[k] ) by A2;
consider m being Element of NAT such that
A4: S₁[m] and
A5: for n being Element of NAT st S₁[n] holds
m <= n from SEQ_4:sch 1(A3);
defpred S₂[ Element of NAT ] means ( $1 + 1 <= m implies ex k being Element of NAT st (StepWhile=0 a,I,s) . ($1 + 1) = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),k );
A6: S₂[ 0 ]

proof

assume 0 + 1 <= m ; :: thesis:
take n = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 3; :: thesis:
thus (StepWhile=0 a,I,s) . (0 + 1) = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),n by SCMFSA_9:30; :: thesis:

end;

A7: IC SCM+FSA in dom ((while=0 a,I) +* (Start-At (insloc 0 ))) by SF_MASTR:65;

A8: now

let k be Element of NAT ; :: thesis:
assume A9: S₂[k] ; :: thesis:

now

assume A10: (k + 1) + 1 <= m ; :: thesis:
k + 0 < k + (1 + 1) by XREAL_1:8;
then A11: k < m by A10, XXREAL_0:2;
A12: (k + 1) + 0 < (k + 1) + 1 by XREAL_1:8;
set sk = (StepWhile=0 a,I,s) . k;
set sk1 = (StepWhile=0 a,I,s) . (k + 1);
consider n being Element of NAT such that
A13: (StepWhile=0 a,I,s) . (k + 1) = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),n by A9, A10, A12, XXREAL_0:2;
A14: (StepWhile=0 a,I,s) . (k + 1) = Computation (((StepWhile=0 a,I,s) . k) +* ((while=0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan (((StepWhile=0 a,I,s) . k) +* (I +* (Start-At (insloc 0 ))))) + 3) by SCMFSA_9:def 4;
A15: ((StepWhile=0 a,I,s) . k) . a = 0 by A5, A11;
then ( I is_closed_on (StepWhile=0 a,I,s) . k & I is_halting_on (StepWhile=0 a,I,s) . k ) by A1;
then A16: IC ((StepWhile=0 a,I,s) . (k + 1)) = insloc 0 by A14, A15, SCMFSA_9:22;
take m = n + ((LifeSpan (((StepWhile=0 a,I,s) . (k + 1)) +* (I +* (Start-At (insloc 0 ))))) + 3); :: thesis:
thus (StepWhile=0 a,I,s) . ((k + 1) + 1) = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),m by A13, A16, SCMFSA_9:31; :: thesis:

end;

hence S₂[k + 1] ; :: thesis:

end;

A17: for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A6, A8);

now

per cases ;

suppose m = 0 ; :: thesis:

then s . a <> 0 by A4, SCMFSA_9:def 4;
hence ( while=0 a,I is_halting_on s & while=0 a,I is_closed_on s ) by SCMFSA_9:18; :: thesis:

end;

suppose A18: m <> 0 ; :: thesis:

then consider i being Nat such that
A19: m = i + 1 by NAT_1:6;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
set si = (StepWhile=0 a,I,s) . i;
set sm = (StepWhile=0 a,I,s) . m;
set sm1 = ((StepWhile=0 a,I,s) . m) +* ((while=0 a,I) +* (Start-At (insloc 0 )));
m = i + 1 by A19;
then consider n being Element of NAT such that
A20: (StepWhile=0 a,I,s) . m = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),n by A17;
A21: (StepWhile=0 a,I,s) . m = Computation (((StepWhile=0 a,I,s) . i) +* ((while=0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan (((StepWhile=0 a,I,s) . i) +* (I +* (Start-At (insloc 0 ))))) + 3) by A19, SCMFSA_9:def 4;
i < m by A19, NAT_1:13;
then A22: ((StepWhile=0 a,I,s) . i) . a = 0 by A5;
then ( I is_closed_on (StepWhile=0 a,I,s) . i & I is_halting_on (StepWhile=0 a,I,s) . i ) by A1;
then A23: IC ((StepWhile=0 a,I,s) . m) = insloc 0 by A21, A22, SCMFSA_9:22;
A24: IC (((StepWhile=0 a,I,s) . m) +* ((while=0 a,I) +* (Start-At (insloc 0 )))) = (((StepWhile=0 a,I,s) . m) +* ((while=0 a,I) +* (Start-At (insloc 0 )))) . (IC SCM+FSA ) by AMI_1:def 15
.= ((while=0 a,I) +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A7, FUNCT_4:14
.= IC ((StepWhile=0 a,I,s) . m) by A23, SF_MASTR:66 ;
A25: DataPart (((StepWhile=0 a,I,s) . m) +* ((while=0 a,I) +* (Start-At (insloc 0 )))) = DataPart ((StepWhile=0 a,I,s) . m) by SCMFSA8A:11;
((StepWhile=0 a,I,s) . m) | NAT = (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))) | NAT by A20, AMI_1:123;
then (((StepWhile=0 a,I,s) . m) +* ((while=0 a,I) +* (Start-At (insloc 0 )))) | NAT = ((StepWhile=0 a,I,s) . m) | NAT by FUNCT_4:100;
then A26: ((StepWhile=0 a,I,s) . m) +* ((while=0 a,I) +* (Start-At (insloc 0 ))) = (StepWhile=0 a,I,s) . m by A24, A25, SCMFSA_9:29;
while=0 a,I is_halting_on (StepWhile=0 a,I,s) . m by A4, SCMFSA_9:18;
then ((StepWhile=0 a,I,s) . m) +* ((while=0 a,I) +* (Start-At (insloc 0 ))) is halting by SCMFSA7B:def 8;
then consider j being Element of NAT such that
A27: CurInstr (Computation ((StepWhile=0 a,I,s) . m),j) = halt SCM+FSA by A26, AMI_1:def 20;
CurInstr (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),(n + j)) = halt SCM+FSA by A20, A27, AMI_1:51;
then s +* ((while=0 a,I) +* (Start-At (insloc 0 ))) is halting by AMI_1:def 20;
hence while=0 a,I is_halting_on s by SCMFSA7B:def 8; :: thesis:
set p = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 3;

now

let q be Element of NAT ; :: thesis:
A28: 0 < m by A18;

per cases ;

suppose A29: q <= (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 3 ; :: thesis:

A30: (StepWhile=0 a,I,s) . 0 = s by SCMFSA_9:def 4;
then A31: s . a = 0 by A5, A28;
then ( I is_closed_on s & I is_halting_on s ) by A1, A30;
hence IC (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),q) in dom (while=0 a,I) by A29, A31, SCMFSA_9:22; :: thesis:

end;

suppose A32: q > (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 3 ; :: thesis:

defpred S₃[ Nat] means ( $1 <= m & $1 <> 0 & ex k being Element of NAT st
( (StepWhile=0 a,I,s) . $1 = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),k & k <= q ) );
A33: for i being Nat st S₃[i] holds
i <= m ;

A34: now

take k = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 3; :: thesis:
thus ( (StepWhile=0 a,I,s) . 1 = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),k & k <= q ) by A32, SCMFSA_9:30; :: thesis:

end;

0 + 1 < m + 1 by A28, XREAL_1:8;
then 1 <= m by NAT_1:13;
then A35: ex k being Nat st S₃[k] by A34;
consider t being Nat such that
A36: ( S₃[t] & ( for i being Nat st S₃[i] holds
i <= t ) ) from NAT_1:sch 6(A33, A35);
reconsider t = t as Element of NAT by ORDINAL1:def 13;

now

per cases ;

suppose t = m ; :: thesis:

then consider r being Element of NAT such that
A37: ( (StepWhile=0 a,I,s) . m = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),r & r <= q ) by A36;
consider x being Nat such that
A38: q = r + x by A37, NAT_1:10;
reconsider x = x as Element of NAT by ORDINAL1:def 13;
A39: Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),q = Computation (((StepWhile=0 a,I,s) . m) +* ((while=0 a,I) +* (Start-At (insloc 0 )))),x by A26, A37, A38, AMI_1:51;
while=0 a,I is_closed_on (StepWhile=0 a,I,s) . m by A4, SCMFSA_9:18;
hence IC (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),q) in dom (while=0 a,I) by A39, SCMFSA7B:def 7; :: thesis:

end;

suppose t <> m ; :: thesis:

then A40: t < m by A36, XXREAL_0:1;
consider y being Nat such that
A41: t = y + 1 by A36, NAT_1:6;
reconsider y = y as Element of NAT by ORDINAL1:def 13;
consider z being Element of NAT such that
A42: ( (StepWhile=0 a,I,s) . t = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),z & z <= q ) by A36;
y + 0 < t by A41, XREAL_1:8;
then A43: y < m by A36, XXREAL_0:2;
set Dy = (StepWhile=0 a,I,s) . y;
set Dt = (StepWhile=0 a,I,s) . t;
A44: (StepWhile=0 a,I,s) . t = Computation (((StepWhile=0 a,I,s) . y) +* ((while=0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan (((StepWhile=0 a,I,s) . y) +* (I +* (Start-At (insloc 0 ))))) + 3) by A41, SCMFSA_9:def 4;
A45: ((StepWhile=0 a,I,s) . y) . a = 0 by A5, A43;
then ( I is_closed_on (StepWhile=0 a,I,s) . y & I is_halting_on (StepWhile=0 a,I,s) . y ) by A1;
then A46: IC ((StepWhile=0 a,I,s) . t) = insloc 0 by A44, A45, SCMFSA_9:22;
set z2 = z + ((LifeSpan (((StepWhile=0 a,I,s) . t) +* (I +* (Start-At (insloc 0 ))))) + 3);

A47: now

assume A48: z + ((LifeSpan (((StepWhile=0 a,I,s) . t) +* (I +* (Start-At (insloc 0 ))))) + 3) <= q ; :: thesis:

A49: now

take k = z + ((LifeSpan (((StepWhile=0 a,I,s) . t) +* (I +* (Start-At (insloc 0 ))))) + 3); :: thesis:
thus ( (StepWhile=0 a,I,s) . (t + 1) = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),k & k <= q ) by A42, A46, A48, SCMFSA_9:31; :: thesis:

end;

t + 1 <= m by A40, NAT_1:13;
hence contradiction by A36, A49, XREAL_1:31; :: thesis:

end;

consider w being Nat such that
A50: q = z + w by A42, NAT_1:10;
reconsider w = w as Element of NAT by ORDINAL1:def 13;
A51: w < (LifeSpan (((StepWhile=0 a,I,s) . t) +* (I +* (Start-At (insloc 0 ))))) + 3 by A47, A50, XREAL_1:8;
A52: Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),q = Computation ((StepWhile=0 a,I,s) . t),w by A42, A50, AMI_1:51
.= Computation (((StepWhile=0 a,I,s) . t) +* ((while=0 a,I) +* (Start-At (insloc 0 )))),w by A42, A46, SCMFSA_9:31 ;
A53: ((StepWhile=0 a,I,s) . t) . a = 0 by A5, A40;
then ( I is_closed_on (StepWhile=0 a,I,s) . t & I is_halting_on (StepWhile=0 a,I,s) . t ) by A1;
hence IC (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),q) in dom (while=0 a,I) by A51, A52, A53, SCMFSA_9:22; :: thesis:

end;

hence IC (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),q) in dom (while=0 a,I) ; :: thesis:

end;

hence while=0 a,I is_closed_on s by SCMFSA7B:def 7; :: thesis:

end;

hence ( while=0 a,I is_halting_on s & while=0 a,I is_closed_on s ) ; :: thesis: