let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for I being Program of SCM+FSA st ProperBodyWhile>0 a,I,s & WithVariantWhile>0 a,I,s 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 I being Program of SCM+FSA st ProperBodyWhile>0 a,I,s & WithVariantWhile>0 a,I,s holds
( while>0 (a,I) is_halting_on s & while>0 (a,I) is_closed_on s )
let I be Program of SCM+FSA; :: thesis: ( ProperBodyWhile>0 a,I,s & WithVariantWhile>0 a,I,s implies ( while>0 (a,I) is_halting_on s & while>0 (a,I) is_closed_on s ) )
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 4 :: thesis: ( not WithVariantWhile>0 a,I,s or ( while>0 (a,I) is_halting_on s & while>0 (a,I) is_closed_on s ) )
set s1 = s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)));
defpred S₁[ Nat] means ((StepWhile>0 (a,I,s)) . $1) . a <= 0 ;
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 5 :: 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);
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 NAT_1:sch 18(A3);
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) );

A6: now

let k be Element of NAT ; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A7: 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 A8: (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 A8, XXREAL_0:2;
then A9: ((StepWhile>0 (a,I,s)) . k) . a > 0 by A5;
(k + 1) + 0 < (k + 1) + 1 by XREAL_1:8;
then consider n being Element of NAT such that
A10: (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 A7, A8, XXREAL_0:2;
A11: (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)) by SCMFSA_9:def 5;
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)
( I is_closed_on (StepWhile>0 (a,I,s)) . k & I is_halting_on (StepWhile>0 (a,I,s)) . k ) by A1, A9;
then IC ((StepWhile>0 (a,I,s)) . (k + 1)) = 0 by A11, A9, SCMFSA_9:47;
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 A10, SCMFSA_9:52; :: thesis: verum

end;

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

end;

A12: IC SCM+FSA in dom ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by COMPOS_1:141;
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 SCMFSA_9:51; :: thesis: verum

end;

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

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 s . a <= 0 by A4, SCMFSA_9:def 5;
hence ( while>0 (a,I) is_halting_on s & while>0 (a,I) is_closed_on s ) by SCMFSA_9:43; :: 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;
set si = (StepWhile>0 (a,I,s)) . i;
A17: (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, SCMFSA_9:def 5;
m = i + 1 by A16;
then consider n being Element of NAT such that
A18: (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;
i < m by A16, NAT_1:13;
then A19: ((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 A20: IC ((StepWhile>0 (a,I,s)) . m) = 0 by A17, A19, SCMFSA_9:47;
ProgramPart ((StepWhile>0 (a,I,s)) . m) = ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) by A18, AMI_1:123;
then A21: ( 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;
IC (((StepWhile>0 (a,I,s)) . m) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = IC ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by A12, FUNCT_4:14
.= IC ((StepWhile>0 (a,I,s)) . m) by A20, COMPOS_1:142 ;
then A22: ((StepWhile>0 (a,I,s)) . m) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) = (StepWhile>0 (a,I,s)) . m by A21, SCMFSA_9:29;
while>0 (a,I) is_halting_on (StepWhile>0 (a,I,s)) . m by A4, SCMFSA_9:43;
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
A23: CurInstr ((ProgramPart ((StepWhile>0 (a,I,s)) . m)),(Comput ((ProgramPart ((StepWhile>0 (a,I,s)) . m)),((StepWhile>0 (a,I,s)) . m),j))) = halt SCM+FSA by A22, EXTPRO_1:30;
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;
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 EXTPRO_1:5;
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 A18, A23, 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 EXTPRO_1:30;
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))

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 A24: 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))

A25: (StepWhile>0 (a,I,s)) . 0 = s by SCMFSA_9:def 5;
then A26: s . a > 0 by A5, A15;
then ( I is_closed_on s & I is_halting_on s ) by A1, A25;
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 A24, A26, SCMFSA_9:47; :: thesis: verum

end;

suppose A27: 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))

A28: 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 A27, SCMFSA_9:51; :: 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 ) );
A29: for i being Nat st S₃[i] holds
i <= m ;
0 + 1 < m + 1 by A15, XREAL_1:8;
then 1 <= m by NAT_1:13;
then A30: ex k being Nat st S₃[k] by A28;
consider t being Nat such that
A31: ( S₃[t] & ( for i being Nat st S₃[i] holds
i <= t ) ) from NAT_1:sch 6(A29, A30);
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
A32: (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
A33: r <= q by A31;
consider x being Nat such that
A34: q = r + x by A33, NAT_1:10;
A35: while>0 (a,I) is_closed_on (StepWhile>0 (a,I,s)) . m by A4, SCMFSA_9:43;
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, A32, 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, A32, A34, EXTPRO_1:5;
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 A35, T, SCMFSA7B:def 7; :: thesis: verum

end;

suppose A36: 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;
consider y being Nat such that
A37: t = y + 1 by A31, NAT_1:6;
reconsider y = y as Element of NAT by ORDINAL1:def 13;
set Dy = (StepWhile>0 (a,I,s)) . y;
A38: (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 A37, SCMFSA_9:def 5;
y + 0 < t by A37, XREAL_1:8;
then y < m by A31, XXREAL_0:2;
then A39: ((StepWhile>0 (a,I,s)) . y) . a > 0 by A5;
then ( I is_closed_on (StepWhile>0 (a,I,s)) . y & I is_halting_on (StepWhile>0 (a,I,s)) . y ) by A1;
then A40: IC ((StepWhile>0 (a,I,s)) . t) = 0 by A38, A39, SCMFSA_9:47;
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 A31;
consider w being Nat such that
A43: q = z + w by A42, NAT_1:10;
reconsider w = w as Element of NAT by ORDINAL1:def 13;
X: (StepWhile>0 (a,I,s)) . t = ((StepWhile>0 (a,I,s)) . t) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by A41, A40, SCMFSA_9:52;
T: ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = ProgramPart ((StepWhile>0 (a,I,s)) . t) by A41, AMI_1:123;
A44: 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, EXTPRO_1:5
.= 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 ;
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);
A45: t < m by A31, A36, XXREAL_0:1;

now

assume A46: 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

A47: 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, A40, A46, SCMFSA_9:52; :: thesis: verum

end;

t + 1 <= m by A45, NAT_1:13;
hence contradiction by A31, A47, XREAL_1:31; :: thesis: verum

end;

then A48: 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;
A49: ((StepWhile>0 (a,I,s)) . t) . a > 0 by A5, A45;
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 (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 A48, A44, A49, SCMFSA_9:47; :: 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