let I be Program of SCM+FSA ; :: thesis: for a being read-write Int-Location
for s being State of SCM+FSA st ( 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 ) ) & ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
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 ) ) holds
( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s )
let a be read-write Int-Location ; :: thesis: for s being State of SCM+FSA st ( 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 ) ) & ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
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 ) ) holds
( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s )
let s be State of SCM+FSA ; :: thesis: ( ( 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 ) ) & ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
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 ) ) implies ( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s ) )
set D = Int-Locations \/ FinSeq-Locations ;
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: ( for f being Function of (product the Object-Kind of SCM+FSA ),NAT holds
not 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 ) ) or ( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s ) )
A2: IC SCM+FSA in dom ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )) by SF_MASTR:65;
set s1 = s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ));
given f being Function of (product the Object-Kind of SCM+FSA ),NAT such that A3: 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: ( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s )
deffunc H₁( Nat) -> Element of NAT = f . ((StepWhile>0 a,I,s) . $1);
A4: for k being Nat holds
( H₁(k + 1) < H₁(k) or H₁(k) = 0 ) by A3;
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₁[ Nat] means ( $1 + 1 <= m implies ex k being Element of NAT st (StepWhile>0 a,I,s) . ($1 + 1) = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),k );

A7: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[k + 1]

now

set sk1 = (StepWhile>0 a,I,s) . (k + 1);
set sk = (StepWhile>0 a,I,s) . k;
assume A9: (k + 1) + 1 <= m ; :: thesis: ex m being Element of NAT st (StepWhile>0 a,I,s) . ((k + 1) + 1) = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),m
k + 0 < k + (1 + 1) by XREAL_1:8;
then k < m by A9, XXREAL_0:2;
then H₁(k) <> 0 by A6;
then A10: ((StepWhile>0 a,I,s) . k) . a > 0 by A3;
A11: I is_halting_on (StepWhile>0 a,I,s) . k by A1;
(k + 1) + 0 < (k + 1) + 1 by XREAL_1:8;
then consider n being Element of NAT such that
A12: (StepWhile>0 a,I,s) . (k + 1) = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),n by A8, A9, XXREAL_0:2;
take m = n + ((LifeSpan (ProgramPart (((StepWhile>0 a,I,s) . (k + 1)) +* (I +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,I,s) . (k + 1)) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3); :: thesis: (StepWhile>0 a,I,s) . ((k + 1) + 1) = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),m
( (StepWhile>0 a,I,s) . (k + 1) = Comput (ProgramPart (((StepWhile>0 a,I,s) . k) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,I,s) . k) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3) & I is_closed_on (StepWhile>0 a,I,s) . k ) by A1, Def5;
then IC ((StepWhile>0 a,I,s) . (k + 1)) = 0 by A11, A10, Th47;
hence (StepWhile>0 a,I,s) . ((k + 1) + 1) = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),m by A12, Th52; :: thesis: verum

end;

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

end;

A13: S₁[ 0 ]

proof

assume 0 + 1 <= m ; :: thesis: ex k being Element of NAT st (StepWhile>0 a,I,s) . (0 + 1) = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),k
take n = (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3; :: thesis: (StepWhile>0 a,I,s) . (0 + 1) = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),n
thus (StepWhile>0 a,I,s) . (0 + 1) = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),n by Th51; :: thesis: verum

end;

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

now

per cases ( m = 0 or m <> 0 ) ;

suppose m = 0 ; :: thesis: ( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s )

then ((StepWhile>0 a,I,s) . 0 ) . a <= 0 by A3, A5;
then s . a <= 0 by Def5;
hence ( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s ) by Th43; :: thesis: verum

end;

suppose A15: m <> 0 ; :: thesis: ( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s )

set p = (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3;
set sm = (StepWhile>0 a,I,s) . m;
set sm1 = ((StepWhile>0 a,I,s) . m) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ));
consider i being Nat such that
A16: m = i + 1 by A15, NAT_1:6;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
m = i + 1 by A16;
then consider n being Element of NAT such that
A17: (StepWhile>0 a,I,s) . m = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),n by A14;
set si = (StepWhile>0 a,I,s) . i;
i < m by A16, NAT_1:13;
then H₁(i) <> 0 by A6;
then A18: ((StepWhile>0 a,I,s) . i) . a > 0 by A3;
A19: ( I is_closed_on (StepWhile>0 a,I,s) . i & I is_halting_on (StepWhile>0 a,I,s) . i ) by A1;
ProgramPart ((StepWhile>0 a,I,s) . m) = ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) by A17, AMI_1:123;
then A20: ( DataPart (((StepWhile>0 a,I,s) . m) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) = DataPart ((StepWhile>0 a,I,s) . m) & ProgramPart (((StepWhile>0 a,I,s) . m) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart ((StepWhile>0 a,I,s) . m) ) by FUNCT_4:100, SCMFSA8A:11;
(StepWhile>0 a,I,s) . m = Comput (ProgramPart (((StepWhile>0 a,I,s) . i) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,I,s) . i) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (((StepWhile>0 a,I,s) . i) +* (I +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,I,s) . i) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3) by A16, Def5;
then A21: IC ((StepWhile>0 a,I,s) . m) = 0 by A19, A18, Th47;
IC (((StepWhile>0 a,I,s) . m) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) = (((StepWhile>0 a,I,s) . m) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) . (IC SCM+FSA )
.= ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )) . (IC SCM+FSA ) by A2, FUNCT_4:14
.= IC ((StepWhile>0 a,I,s) . m) by A21, SF_MASTR:66 ;
then A22: ((StepWhile>0 a,I,s) . m) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )) = (StepWhile>0 a,I,s) . m by A20, Th29;
TX1: ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart ((StepWhile>0 a,I,s) . m) by A17, AMI_1:123;
T: ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),n) by AMI_1:123;
A23: ((StepWhile>0 a,I,s) . m) . a <= 0 by A3, A5;
then while>0 a,I is_halting_on (StepWhile>0 a,I,s) . m by Th43;
then ProgramPart (((StepWhile>0 a,I,s) . m) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) halts_on ((StepWhile>0 a,I,s) . m) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )) by SCMFSA7B:def 8;
then consider j being Element of NAT such that
A24: CurInstr (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart ((StepWhile>0 a,I,s) . m)),((StepWhile>0 a,I,s) . m),j) = halt SCM+FSA by A22, TX1, AMI_1:146;
x: Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(n + j) = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),n),j by AMI_1:51;
CurInstr (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(n + j)) = halt SCM+FSA by A17, A24, x, T;
then ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) halts_on s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )) by AMI_1:146;
hence while>0 a,I is_halting_on s by SCMFSA7B:def 8; :: thesis: while>0 a,I is_closed_on s

now

let q be Element of NAT ; :: thesis: IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),b₁) in dom (while>0 a,I)
A25: 0 < m by A15;

per cases ( q <= (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3 or q > (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3 ) ;

suppose A26: q <= (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3 ; :: thesis: IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),b₁) in dom (while>0 a,I)

A27: (StepWhile>0 a,I,s) . 0 = s by Def5;
then A28: ( I is_closed_on s & I is_halting_on s ) by A1;
H₁( 0 ) <> 0 by A6, A25;
then s . a > 0 by A3, A27;
hence IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),q) in dom (while>0 a,I) by A26, A28, Th47; :: thesis: verum

end;

suppose A29: q > (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3 ; :: thesis: IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),b₁) in dom (while>0 a,I)

A30: now

take k = (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3; :: thesis: ( (StepWhile>0 a,I,s) . 1 = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),k & k <= q )
thus ( (StepWhile>0 a,I,s) . 1 = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),k & k <= q ) by A29, Th51; :: thesis: verum

end;

defpred S₂[ Nat] means ( $1 <= m & $1 <> 0 & ex k being Element of NAT st
( (StepWhile>0 a,I,s) . $1 = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),k & k <= q ) );
A31: for i being Nat st S₂[i] holds
i <= m ;
0 + 1 < m + 1 by A25, XREAL_1:8;
then 1 <= m by NAT_1:13;
then A32: ex t being Nat st S₂[t] by A30;
consider t being Nat such that
A33: ( S₂[t] & ( for i being Nat st S₂[i] holds
i <= t ) ) from NAT_1:sch 6(A31, A32);
reconsider t = t as Element of NAT by ORDINAL1:def 13;

now

per cases ( t = m or t <> m ) ;

suppose t = m ; :: thesis: IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),q) in dom (while>0 a,I)

then consider r being Element of NAT such that
A34: (StepWhile>0 a,I,s) . m = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),r and
A35: r <= q by A33;
consider x being Nat such that
A36: q = r + x by A35, NAT_1:10;
A37: while>0 a,I is_closed_on (StepWhile>0 a,I,s) . m by A23, Th43;
reconsider x = x as Element of NAT by ORDINAL1:def 13;
T: ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (((StepWhile>0 a,I,s) . m) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) by A22, A34, AMI_1:123;
Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),q = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,I,s) . m) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),x by A22, A34, A36, AMI_1:51;
hence IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),q) in dom (while>0 a,I) by A37, T, SCMFSA7B:def 7; :: thesis: verum

end;

suppose A38: t <> m ; :: thesis: IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),q) in dom (while>0 a,I)

set Dt = (StepWhile>0 a,I,s) . t;
A39: t < m by A33, A38, XXREAL_0:1;
then H₁(t) <> 0 by A6;
then A40: ((StepWhile>0 a,I,s) . t) . a > 0 by A3;
consider z being Element of NAT such that
A41: (StepWhile>0 a,I,s) . t = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),z and
A42: z <= q by A33;
set z2 = z + ((LifeSpan (ProgramPart (((StepWhile>0 a,I,s) . t) +* (I +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,I,s) . t) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3);
consider w being Nat such that
A43: q = z + w by A42, NAT_1:10;
A44: ( I is_closed_on (StepWhile>0 a,I,s) . t & I is_halting_on (StepWhile>0 a,I,s) . t ) by A1;
consider y being Nat such that
A45: t = y + 1 by A33, NAT_1:6;
reconsider y = y as Element of NAT by ORDINAL1:def 13;
set Dy = (StepWhile>0 a,I,s) . y;
y + 0 < t by A45, XREAL_1:8;
then y < m by A33, XXREAL_0:2;
then H₁(y) <> 0 by A6;
then A46: ((StepWhile>0 a,I,s) . y) . a > 0 by A3;
A47: ( I is_closed_on (StepWhile>0 a,I,s) . y & I is_halting_on (StepWhile>0 a,I,s) . y ) by A1;
reconsider w = w as Element of NAT by ORDINAL1:def 13;
(StepWhile>0 a,I,s) . t = Comput (ProgramPart (((StepWhile>0 a,I,s) . y) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,I,s) . y) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (((StepWhile>0 a,I,s) . y) +* (I +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,I,s) . y) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3) by A45, Def5;
then A48: IC ((StepWhile>0 a,I,s) . t) = 0 by A47, A46, Th47;

now

assume A49: z + ((LifeSpan (ProgramPart (((StepWhile>0 a,I,s) . t) +* (I +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,I,s) . t) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3) <= q ; :: thesis: contradiction

A50: now

take k = z + ((LifeSpan (ProgramPart (((StepWhile>0 a,I,s) . t) +* (I +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,I,s) . t) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3); :: thesis: ( (StepWhile>0 a,I,s) . (t + 1) = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),k & k <= q )
thus ( (StepWhile>0 a,I,s) . (t + 1) = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),k & k <= q ) by A41, A48, A49, Th52; :: thesis: verum

end;

t + 1 <= m by A39, NAT_1:13;
hence contradiction by A33, A50, XREAL_1:31; :: thesis: verum

end;

then A51: w < (LifeSpan (ProgramPart (((StepWhile>0 a,I,s) . t) +* (I +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,I,s) . t) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3 by A43, XREAL_1:8;
X: ((StepWhile>0 a,I,s) . t) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )) = (StepWhile>0 a,I,s) . t by A41, A48, Th52;
T: ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart ((StepWhile>0 a,I,s) . t) by A41, AMI_1:123;
Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),q = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((StepWhile>0 a,I,s) . t),w by A41, A43, AMI_1:51
.= Comput (ProgramPart (((StepWhile>0 a,I,s) . t) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,I,s) . t) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),w by X, T ;
hence IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),q) in dom (while>0 a,I) by A51, A44, A40, Th47; :: thesis: verum

end;

end;

end;

hence IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),q) in dom (while>0 a,I) ; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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