let P be Instruction-Sequence of SCM+FSA; :: thesis:
let I be Program of ; :: 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,P,s)) . k,P +* (while=0 (a,I)) & I is_halting_on (StepWhile=0 (a,I,P,s)) . k,P +* (while=0 (a,I)) ) ; :: thesis:
set s1 = Initialize s;
set P1 = P +* (while=0 (a,I));
A3: (P +* (while=0 (a,I))) +* (while=0 (a,I)) = P +* (while=0 (a,I)) by FUNCT_4:93;
given f being Function of (product the Object-Kind of SCM+FSA),NAT such that A5: for k being Nat holds
( ( f . ((StepWhile=0 (a,I,P,s)) . (k + 1)) < f . ((StepWhile=0 (a,I,P,s)) . k) or f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) & ( f . ((StepWhile=0 (a,I,P,s)) . k) = 0 implies ((StepWhile=0 (a,I,P,s)) . k) . a <> 0 ) & ( ((StepWhile=0 (a,I,P,s)) . k) . a <> 0 implies f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) ) ; :: thesis:
deffunc H₁( Nat) -> Element of NAT = f . ((StepWhile=0 (a,I,P,s)) . $1);
A6: for k being Nat holds
( H₁(k + 1) < H₁(k) or H₁(k) = 0 ) by A5;
consider m being Nat such that
A7: H₁(m) = 0 and
A8: for n being Nat st H₁(n) = 0 holds
m <= n from NAT_1:sch 17(A6);
defpred S₁[ Nat] means ( $1 + 1 <= m implies ex k being Element of NAT st (StepWhile=0 (a,I,P,s)) . ($1 + 1) = Comput ((P +* (while=0 (a,I))),(Initialize s),k) );

A9: now

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

now

set sk1 = (StepWhile=0 (a,I,P,s)) . (k + 1);
set sk = (StepWhile=0 (a,I,P,s)) . k;
assume A11: (k + 1) + 1 <= m ; :: thesis:
k + 0 < k + (1 + 1) by XREAL_1:6;
then k < m by A11, XXREAL_0:2;
then H₁(k) <> 0 by A8;
then A12: ((StepWhile=0 (a,I,P,s)) . k) . a = 0 by A5;
A13: I is_halting_on (StepWhile=0 (a,I,P,s)) . k,P +* (while=0 (a,I)) by A1;
(k + 1) + 0 < (k + 1) + 1 by XREAL_1:6;
then consider n being Element of NAT such that
A14: (StepWhile=0 (a,I,P,s)) . (k + 1) = Comput ((P +* (while=0 (a,I))),(Initialize s),n) by A10, A11, XXREAL_0:2;
take m = n + ((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,P,s)) . (k + 1))))) + 3); :: thesis:
A15: (P +* (while=0 (a,I))) +* (while=0 (a,I)) = P +* (while=0 (a,I)) by FUNCT_4:93;
( (StepWhile=0 (a,I,P,s)) . (k + 1) = Comput ((P +* (while=0 (a,I))),(Initialize ((StepWhile=0 (a,I,P,s)) . k)),((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,P,s)) . k)))) + 3)) & I is_closed_on (StepWhile=0 (a,I,P,s)) . k,P +* (while=0 (a,I)) ) by A1, Def4;
then IC ((StepWhile=0 (a,I,P,s)) . (k + 1)) = 0 by A13, A12, Th22, A15;
hence (StepWhile=0 (a,I,P,s)) . ((k + 1) + 1) = Comput ((P +* (while=0 (a,I))),(Initialize s),m) by A14, Th31; :: thesis:

end;

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

end;

A16: S₁[ 0 ]

proof

assume 0 + 1 <= m ; :: thesis:
take n = (LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize s))) + 3; :: thesis:
thus (StepWhile=0 (a,I,P,s)) . (0 + 1) = Comput ((P +* (while=0 (a,I))),(Initialize s),n) by Th30; :: thesis:

end;

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

now

per cases ;

suppose m = 0 ; :: thesis:

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

end;

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

then consider i being Nat such that
A19: m = i + 1 by NAT_1:6;
reconsider m = m, i = i as Element of NAT by ORDINAL1:def 12;
set sm = (StepWhile=0 (a,I,P,s)) . m;
set si = (StepWhile=0 (a,I,P,s)) . i;
i < m by A19, NAT_1:13;
then H₁(i) <> 0 by A8;
then A20: ((StepWhile=0 (a,I,P,s)) . i) . a = 0 by A5;
A21: ( I is_closed_on (StepWhile=0 (a,I,P,s)) . i,P +* (while=0 (a,I)) & I is_halting_on (StepWhile=0 (a,I,P,s)) . i,P +* (while=0 (a,I)) ) by A1;
XX: IC in dom ((StepWhile=0 (a,I,P,s)) . m) by MEMSTR_0:2;
(StepWhile=0 (a,I,P,s)) . m = Comput ((P +* (while=0 (a,I))),(Initialize ((StepWhile=0 (a,I,P,s)) . i)),((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,P,s)) . i)))) + 3)) by A19, Def4;
then IC ((StepWhile=0 (a,I,P,s)) . m) = 0 by A21, A20, Th22, A3;
then (StepWhile=0 (a,I,P,s)) . m is 0 -started by XX, MEMSTR_0:def 8;
then B22: Start-At (0,SCM+FSA) c= (StepWhile=0 (a,I,P,s)) . m by MEMSTR_0:29;
set p = (LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize s))) + 3;
set sm1 = Initialize ((StepWhile=0 (a,I,P,s)) . m);
m = i + 1 by A19;
then consider n being Element of NAT such that
A23: (StepWhile=0 (a,I,P,s)) . m = Comput ((P +* (while=0 (a,I))),(Initialize s),n) by A17;
reconsider n = n as Element of NAT ;
A27: Initialize ((StepWhile=0 (a,I,P,s)) . m) = (StepWhile=0 (a,I,P,s)) . m by B22, FUNCT_4:98;
A28: ((StepWhile=0 (a,I,P,s)) . m) . a <> 0 by A5, A7;
then while=0 (a,I) is_halting_on (StepWhile=0 (a,I,P,s)) . m,P by Th18;
then P +* (while=0 (a,I)) halts_on Initialize ((StepWhile=0 (a,I,P,s)) . m) by SCMFSA7B:def 7;
then P +* (while=0 (a,I)) halts_on Initialize ((StepWhile=0 (a,I,P,s)) . m) ;
then P +* (while=0 (a,I)) halts_on Initialize ((StepWhile=0 (a,I,P,s)) . m) ;
then consider j being Element of NAT such that
A29: CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),((StepWhile=0 (a,I,P,s)) . m),j))) = halt SCM+FSA by A27, EXTPRO_1:29;
A30: Comput ((P +* (while=0 (a,I))),(Initialize s),(n + j)) = Comput ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),n)),j) by EXTPRO_1:4;
CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),(n + j)))) = halt SCM+FSA by A23, A29, A30;
then P +* (while=0 (a,I)) halts_on Initialize s by EXTPRO_1:29;
hence while=0 (a,I) is_halting_on s,P by SCMFSA7B:def 7; :: thesis:

now

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

per cases ;

suppose A32: q <= (LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize s))) + 3 ; :: thesis:

A33: (StepWhile=0 (a,I,P,s)) . 0 = s by Def4;
then A34: ( I is_closed_on s,P +* (while=0 (a,I)) & I is_halting_on s,P +* (while=0 (a,I)) ) by A1;
H₁( 0 ) <> 0 by A8, A31;
then s . a = 0 by A5, A33;
hence IC (Comput ((P +* (while=0 (a,I))),(Initialize s),q)) in dom (while=0 (a,I)) by A32, A34, Th22, A3; :: thesis:

end;

suppose A35: q > (LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize s))) + 3 ; :: thesis:

A36: now

take k = (LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize s))) + 3; :: thesis:
thus ( (StepWhile=0 (a,I,P,s)) . 1 = Comput ((P +* (while=0 (a,I))),(Initialize s),k) & k <= q ) by A35, Th30; :: thesis:

end;

defpred S₂[ Nat] means ( $1 <= m & $1 <> 0 & ex k being Element of NAT st
( (StepWhile=0 (a,I,P,s)) . $1 = Comput ((P +* (while=0 (a,I))),(Initialize s),k) & k <= q ) );
A37: for i being Nat st S₂[i] holds
i <= m ;
0 + 1 < m + 1 by A31, XREAL_1:6;
then 1 <= m by NAT_1:13;
then A38: ex t being Nat st S₂[t] by A36;
consider t being Nat such that
A39: ( S₂[t] & ( for i being Nat st S₂[i] holds
i <= t ) ) from NAT_1:sch 6(A37, A38);
reconsider t = t as Element of NAT by ORDINAL1:def 12;

now

per cases ;

suppose t = m ; :: thesis:

then consider r being Element of NAT such that
A40: (StepWhile=0 (a,I,P,s)) . m = Comput ((P +* (while=0 (a,I))),(Initialize s),r) and
A41: r <= q by A39;
consider x being Nat such that
A42: q = r + x by A41, NAT_1:10;
A43: while=0 (a,I) is_closed_on (StepWhile=0 (a,I,P,s)) . m,P by A28, Th18;
reconsider x = x as Element of NAT by ORDINAL1:def 12;
Comput ((P +* (while=0 (a,I))),(Initialize s),q) = Comput ((P +* (while=0 (a,I))),(Initialize ((StepWhile=0 (a,I,P,s)) . m)),x) by A27, A40, A42, EXTPRO_1:4;
hence IC (Comput ((P +* (while=0 (a,I))),(Initialize s),q)) in dom (while=0 (a,I)) by A43, SCMFSA7B:def 6; :: thesis:

end;

suppose A44: t <> m ; :: thesis:

set Dt = (StepWhile=0 (a,I,P,s)) . t;
A45: t < m by A39, A44, XXREAL_0:1;
then H₁(t) <> 0 by A8;
then A46: ((StepWhile=0 (a,I,P,s)) . t) . a = 0 by A5;
consider z being Element of NAT such that
A47: (StepWhile=0 (a,I,P,s)) . t = Comput ((P +* (while=0 (a,I))),(Initialize s),z) and
A48: z <= q by A39;
set z2 = z + ((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,P,s)) . t)))) + 3);
consider w being Nat such that
A49: q = z + w by A48, NAT_1:10;
A50: ( I is_closed_on (StepWhile=0 (a,I,P,s)) . t,P +* (while=0 (a,I)) & I is_halting_on (StepWhile=0 (a,I,P,s)) . t,P +* (while=0 (a,I)) ) by A1;
consider y being Nat such that
A51: t = y + 1 by A39, NAT_1:6;
reconsider y = y as Element of NAT by ORDINAL1:def 12;
set Dy = (StepWhile=0 (a,I,P,s)) . y;
y + 0 < t by A51, XREAL_1:6;
then y < m by A39, XXREAL_0:2;
then H₁(y) <> 0 by A8;
then A52: ((StepWhile=0 (a,I,P,s)) . y) . a = 0 by A5;
A53: ( I is_closed_on (StepWhile=0 (a,I,P,s)) . y,P +* (while=0 (a,I)) & I is_halting_on (StepWhile=0 (a,I,P,s)) . y,P +* (while=0 (a,I)) ) by A1;
reconsider w = w as Element of NAT by ORDINAL1:def 12;
(StepWhile=0 (a,I,P,s)) . t = Comput ((P +* (while=0 (a,I))),(Initialize ((StepWhile=0 (a,I,P,s)) . y)),((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,P,s)) . y)))) + 3)) by A51, Def4;
then A54: IC ((StepWhile=0 (a,I,P,s)) . t) = 0 by A53, A52, Th22, A3;

now

assume A55: z + ((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,P,s)) . t)))) + 3) <= q ; :: thesis:

A56: now

take k = z + ((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,P,s)) . t)))) + 3); :: thesis:
thus ( (StepWhile=0 (a,I,P,s)) . (t + 1) = Comput ((P +* (while=0 (a,I))),(Initialize s),k) & k <= q ) by A47, A54, A55, Th31; :: thesis:

end;

t + 1 <= m by A45, NAT_1:13;
hence contradiction by A39, A56, XREAL_1:29; :: thesis:

end;

then A57: w < (LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,P,s)) . t)))) + 3 by A49, XREAL_1:6;
A58: (StepWhile=0 (a,I,P,s)) . t = Initialize ((StepWhile=0 (a,I,P,s)) . t) by A47, A54, Th31;
Comput ((P +* (while=0 (a,I))),(Initialize s),q) = Comput ((P +* (while=0 (a,I))),(((StepWhile=0 (a,I,P,s)) . t) +* (Start-At (0,SCM+FSA))),w) by A58, A47, A49, EXTPRO_1:4;
hence IC (Comput ((P +* (while=0 (a,I))),(Initialize s),q)) in dom (while=0 (a,I)) by A57, A50, A46, Th22, A3; :: thesis:

end;

hence IC (Comput ((P +* (while=0 (a,I))),(Initialize s),q)) in dom (while=0 (a,I)) ; :: thesis:

end;

hence while=0 (a,I) is_closed_on s,P by SCMFSA7B:def 6; :: thesis:

end;

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