set IL = NAT ;
let I be Program of SCM+FSA ; :: thesis:
let a be read-write Int-Location ; :: thesis:
let s be State of SCM+FSA ; :: thesis:
assume A1: for k being Nat holds
( I is_closed_on (StepWhile=0 a,I,s) . k & I is_halting_on (StepWhile=0 a,I,s) . k ) ; :: thesis:
given f being Function of (product the Object-Kind of SCM+FSA ),NAT such that A2: for k being Nat holds
( ( f . ((StepWhile=0 a,I,s) . (k + 1)) < f . ((StepWhile=0 a,I,s) . k) or f . ((StepWhile=0 a,I,s) . k) = 0 ) & ( f . ((StepWhile=0 a,I,s) . k) = 0 implies ((StepWhile=0 a,I,s) . k) . a <> 0 ) & ( ((StepWhile=0 a,I,s) . k) . a <> 0 implies f . ((StepWhile=0 a,I,s) . k) = 0 ) ) ; :: thesis:
deffunc H₁( Nat) -> Element of NAT = f . ((StepWhile=0 a,I,s) . $1);
set s1 = s +* ((while=0 a,I) +* (Start-At (insloc 0 )));
A4: for k being Nat holds
( H₁(k + 1) < H₁(k) or H₁(k) = 0 ) by A2;
consider m being Nat such that
A5: H₁(m) = 0 and
A6: for n being Nat st H₁(n) = 0 holds
m <= n from NAT_1:sch 17(A4);
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 );
A7: 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 Th30; :: thesis:

end;

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

A9: now

let k be Element of NAT ; :: thesis:
assume A10: S₁[k] ; :: thesis:

now

assume A11: (k + 1) + 1 <= m ; :: thesis:
k + 0 < k + (1 + 1) by XREAL_1:8;
then A12: k < m by A11, XXREAL_0:2;
A13: (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
A14: (StepWhile=0 a,I,s) . (k + 1) = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),n by A10, A11, A13, XXREAL_0:2;
A15: (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 Def4;
A16: ( I is_closed_on (StepWhile=0 a,I,s) . k & I is_halting_on (StepWhile=0 a,I,s) . k ) by A1;
H₁(k) <> 0 by A6, A12;
then ((StepWhile=0 a,I,s) . k) . a = 0 by A2;
then A17: IC ((StepWhile=0 a,I,s) . (k + 1)) = insloc 0 by A15, A16, Th22;
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 A14, A17, Th31; :: thesis:

end;

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

end;

A18: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A7, A9);

now

per cases ;

suppose m = 0 ; :: thesis:

then ((StepWhile=0 a,I,s) . 0 ) . a <> 0 by A2, A5;
then s . a <> 0 by Def4;
hence ( while=0 a,I is_halting_on s & while=0 a,I is_closed_on s ) by Th18; :: thesis:

end;

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

then consider i being Nat such that
A20: m = i + 1 by NAT_1:6;
reconsider m = m, 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 A20;
then consider n being Element of NAT such that
A21: (StepWhile=0 a,I,s) . m = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),n by A18;
reconsider n = n as Element of NAT ;
A22: ((StepWhile=0 a,I,s) . m) . a <> 0 by A2, A5;
A23: (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 A20, Def4;
A24: ( I is_closed_on (StepWhile=0 a,I,s) . i & I is_halting_on (StepWhile=0 a,I,s) . i ) by A1;
i < m by A20, NAT_1:13;
then H₁(i) <> 0 by A6;
then ((StepWhile=0 a,I,s) . i) . a = 0 by A2;
then A25: IC ((StepWhile=0 a,I,s) . m) = insloc 0 by A23, A24, Th22;
A26: 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 A8, FUNCT_4:14
.= IC ((StepWhile=0 a,I,s) . m) by A25, SF_MASTR:66 ;
set D = Int-Locations \/ FinSeq-Locations ;
A27: 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 A21, 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 A28: ((StepWhile=0 a,I,s) . m) +* ((while=0 a,I) +* (Start-At (insloc 0 ))) = (StepWhile=0 a,I,s) . m by A26, A27, Th29;
while=0 a,I is_halting_on (StepWhile=0 a,I,s) . m by A22, Th18;
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
A29: CurInstr (Computation ((StepWhile=0 a,I,s) . m),j) = halt SCM+FSA by A28, AMI_1:def 20;
CurInstr (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),(n + j)) = halt SCM+FSA by A21, A29, 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:
A30: 0 < m by A19, NAT_1:3;

per cases ;

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

A32: (StepWhile=0 a,I,s) . 0 = s by Def4;
H₁( 0 ) <> 0 by A6, A30;
then A33: s . a = 0 by A2, A32;
( I is_closed_on s & I is_halting_on s ) by A1, A32;
hence IC (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),q) in dom (while=0 a,I) by A31, A33, Th22; :: thesis:

end;

suppose A34: 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 ) );
A35: for i being Nat st S₂[i] holds
i <= m ;

A36: 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 A34, Th30; :: thesis:

end;

0 + 1 < m + 1 by A30, XREAL_1:8;
then 1 <= m by NAT_1:13;
then A37: ex t being Nat st S₂[t] by A36;
consider t being Nat such that
A38: ( S₂[t] & ( for i being Nat st S₂[i] holds
i <= t ) ) from NAT_1:sch 6(A35, A37);
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
A39: ( (StepWhile=0 a,I,s) . m = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),r & r <= q ) by A38;
consider x being Nat such that
A40: q = r + x by A39, NAT_1:10;
reconsider x = x as Element of NAT by ORDINAL1:def 13;
A41: 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 A28, A39, A40, AMI_1:51;
while=0 a,I is_closed_on (StepWhile=0 a,I,s) . m by A22, Th18;
hence IC (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),q) in dom (while=0 a,I) by A41, SCMFSA7B:def 7; :: thesis:

end;

suppose t <> m ; :: thesis:

then A42: t < m by A38, XXREAL_0:1;
consider y being Nat such that
A43: t = y + 1 by A38, NAT_1:6;
reconsider y = y as Element of NAT by ORDINAL1:def 13;
consider z being Element of NAT such that
A44: ( (StepWhile=0 a,I,s) . t = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),z & z <= q ) by A38;
y + 0 < t by A43, XREAL_1:8;
then A45: y < m by A38, XXREAL_0:2;
set Dy = (StepWhile=0 a,I,s) . y;
set Dt = (StepWhile=0 a,I,s) . t;
A46: (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 A43, Def4;
A47: ( I is_closed_on (StepWhile=0 a,I,s) . y & I is_halting_on (StepWhile=0 a,I,s) . y ) by A1;
H₁(y) <> 0 by A6, A45;
then ((StepWhile=0 a,I,s) . y) . a = 0 by A2;
then A48: IC ((StepWhile=0 a,I,s) . t) = insloc 0 by A46, A47, Th22;
set z2 = z + ((LifeSpan (((StepWhile=0 a,I,s) . t) +* (I +* (Start-At (insloc 0 ))))) + 3);

A49: now

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

A51: 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 A44, A48, A50, Th31; :: thesis:

end;

t + 1 <= m by A42, NAT_1:13;
hence contradiction by A38, A51, XREAL_1:31; :: thesis:

end;

consider w being Nat such that
A52: q = z + w by A44, NAT_1:10;
reconsider w = w as Element of NAT by ORDINAL1:def 13;
A53: w < (LifeSpan (((StepWhile=0 a,I,s) . t) +* (I +* (Start-At (insloc 0 ))))) + 3 by A49, A52, XREAL_1:8;
A54: Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),q = Computation ((StepWhile=0 a,I,s) . t),w by A44, A52, AMI_1:51
.= Computation (((StepWhile=0 a,I,s) . t) +* ((while=0 a,I) +* (Start-At (insloc 0 )))),w by A44, A48, Th31 ;
A55: ( I is_closed_on (StepWhile=0 a,I,s) . t & I is_halting_on (StepWhile=0 a,I,s) . t ) by A1;
H₁(t) <> 0 by A6, A42;
then ((StepWhile=0 a,I,s) . t) . a = 0 by A2;
hence IC (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),q) in dom (while=0 a,I) by A53, A54, A55, Th22; :: 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: