let s be 0 -started State of SCMPDS; :: thesis: for I being halt-free shiftable Program of SCMPDS
for a, b, c being Int_position
for n, i, p0 being Element of NAT
for f being FinSequence of INT st card I > 0 & f is_FinSequence_on s,p0 & len f = n & s . b = 0 & s . a = 0 & s . (intpos i) = - n & s . c = p0 + 1 & ( for t being State of SCMPDS st ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = (t . (intpos i)) + n & t . b = Sum g & t . c = (p0 + 1) + (len g) ) & t . a = 0 & t . (intpos i) < 0 & ( for i being Element of NAT st i > p0 holds
t . (intpos i) = s . (intpos i) ) holds
( (IExec (I,t)) . a = 0 & I is_closed_on t & I is_halting_on t & (IExec (I,t)) . (intpos i) = (t . (intpos i)) + 1 & ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = ((t . (intpos i)) + n) + 1 & (IExec (I,t)) . c = (p0 + 1) + (len g) & (IExec (I,t)) . b = Sum g ) & ( for i being Element of NAT st i > p0 holds
(IExec (I,t)) . (intpos i) = s . (intpos i) ) ) ) holds
( (IExec ((while<0 (a,i,I)),s)) . b = Sum f & while<0 (a,i,I) is_closed_on s & while<0 (a,i,I) is_halting_on s )
let I be halt-free shiftable Program of SCMPDS; :: thesis: for a, b, c being Int_position
for n, i, p0 being Element of NAT
for f being FinSequence of INT st card I > 0 & f is_FinSequence_on s,p0 & len f = n & s . b = 0 & s . a = 0 & s . (intpos i) = - n & s . c = p0 + 1 & ( for t being State of SCMPDS st ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = (t . (intpos i)) + n & t . b = Sum g & t . c = (p0 + 1) + (len g) ) & t . a = 0 & t . (intpos i) < 0 & ( for i being Element of NAT st i > p0 holds
t . (intpos i) = s . (intpos i) ) holds
( (IExec (I,t)) . a = 0 & I is_closed_on t & I is_halting_on t & (IExec (I,t)) . (intpos i) = (t . (intpos i)) + 1 & ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = ((t . (intpos i)) + n) + 1 & (IExec (I,t)) . c = (p0 + 1) + (len g) & (IExec (I,t)) . b = Sum g ) & ( for i being Element of NAT st i > p0 holds
(IExec (I,t)) . (intpos i) = s . (intpos i) ) ) ) holds
( (IExec ((while<0 (a,i,I)),s)) . b = Sum f & while<0 (a,i,I) is_closed_on s & while<0 (a,i,I) is_halting_on s )
let a, b, c be Int_position ; :: thesis: for n, i, p0 being Element of NAT
for f being FinSequence of INT st card I > 0 & f is_FinSequence_on s,p0 & len f = n & s . b = 0 & s . a = 0 & s . (intpos i) = - n & s . c = p0 + 1 & ( for t being State of SCMPDS st ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = (t . (intpos i)) + n & t . b = Sum g & t . c = (p0 + 1) + (len g) ) & t . a = 0 & t . (intpos i) < 0 & ( for i being Element of NAT st i > p0 holds
t . (intpos i) = s . (intpos i) ) holds
( (IExec (I,t)) . a = 0 & I is_closed_on t & I is_halting_on t & (IExec (I,t)) . (intpos i) = (t . (intpos i)) + 1 & ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = ((t . (intpos i)) + n) + 1 & (IExec (I,t)) . c = (p0 + 1) + (len g) & (IExec (I,t)) . b = Sum g ) & ( for i being Element of NAT st i > p0 holds
(IExec (I,t)) . (intpos i) = s . (intpos i) ) ) ) holds
( (IExec ((while<0 (a,i,I)),s)) . b = Sum f & while<0 (a,i,I) is_closed_on s & while<0 (a,i,I) is_halting_on s )
let n, i, p0 be Element of NAT ; :: thesis: for f being FinSequence of INT st card I > 0 & f is_FinSequence_on s,p0 & len f = n & s . b = 0 & s . a = 0 & s . (intpos i) = - n & s . c = p0 + 1 & ( for t being State of SCMPDS st ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = (t . (intpos i)) + n & t . b = Sum g & t . c = (p0 + 1) + (len g) ) & t . a = 0 & t . (intpos i) < 0 & ( for i being Element of NAT st i > p0 holds
t . (intpos i) = s . (intpos i) ) holds
( (IExec (I,t)) . a = 0 & I is_closed_on t & I is_halting_on t & (IExec (I,t)) . (intpos i) = (t . (intpos i)) + 1 & ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = ((t . (intpos i)) + n) + 1 & (IExec (I,t)) . c = (p0 + 1) + (len g) & (IExec (I,t)) . b = Sum g ) & ( for i being Element of NAT st i > p0 holds
(IExec (I,t)) . (intpos i) = s . (intpos i) ) ) ) holds
( (IExec ((while<0 (a,i,I)),s)) . b = Sum f & while<0 (a,i,I) is_closed_on s & while<0 (a,i,I) is_halting_on s )
let f be FinSequence of INT ; :: thesis: ( card I > 0 & f is_FinSequence_on s,p0 & len f = n & s . b = 0 & s . a = 0 & s . (intpos i) = - n & s . c = p0 + 1 & ( for t being State of SCMPDS st ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = (t . (intpos i)) + n & t . b = Sum g & t . c = (p0 + 1) + (len g) ) & t . a = 0 & t . (intpos i) < 0 & ( for i being Element of NAT st i > p0 holds
t . (intpos i) = s . (intpos i) ) holds
( (IExec (I,t)) . a = 0 & I is_closed_on t & I is_halting_on t & (IExec (I,t)) . (intpos i) = (t . (intpos i)) + 1 & ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = ((t . (intpos i)) + n) + 1 & (IExec (I,t)) . c = (p0 + 1) + (len g) & (IExec (I,t)) . b = Sum g ) & ( for i being Element of NAT st i > p0 holds
(IExec (I,t)) . (intpos i) = s . (intpos i) ) ) ) implies ( (IExec ((while<0 (a,i,I)),s)) . b = Sum f & while<0 (a,i,I) is_closed_on s & while<0 (a,i,I) is_halting_on s ) )
assume A1: card I > 0 ; :: thesis: ( not f is_FinSequence_on s,p0 or not len f = n or not s . b = 0 or not s . a = 0 or not s . (intpos i) = - n or not s . c = p0 + 1 or ex t being State of SCMPDS st
( ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = (t . (intpos i)) + n & t . b = Sum g & t . c = (p0 + 1) + (len g) ) & t . a = 0 & t . (intpos i) < 0 & ( for i being Element of NAT st i > p0 holds
t . (intpos i) = s . (intpos i) ) & not ( (IExec (I,t)) . a = 0 & I is_closed_on t & I is_halting_on t & (IExec (I,t)) . (intpos i) = (t . (intpos i)) + 1 & ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = ((t . (intpos i)) + n) + 1 & (IExec (I,t)) . c = (p0 + 1) + (len g) & (IExec (I,t)) . b = Sum g ) & ( for i being Element of NAT st i > p0 holds
(IExec (I,t)) . (intpos i) = s . (intpos i) ) ) ) or ( (IExec ((while<0 (a,i,I)),s)) . b = Sum f & while<0 (a,i,I) is_closed_on s & while<0 (a,i,I) is_halting_on s ) )
set Iw = IExec ((while<0 (a,i,I)),s);
set Dw = Dstate (IExec ((while<0 (a,i,I)),s));
set da = DataLoc ((s . a),i);
defpred S₁[ State of SCMPDS] means ( ( for i being Element of NAT st i > p0 holds
$1 . (intpos i) = s . (intpos i) ) & ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = ($1 . (intpos i)) + n & $1 . b = Sum g & $1 . (intpos i) <= 0 & $1 . c = (p0 + 1) + (len g) ) );
assume that
A2: f is_FinSequence_on s,p0 and
A3: len f = n and
A4: s . b = 0 and
A5: s . a = 0 and
A6: s . (intpos i) = - n and
A7: s . c = p0 + 1 ; :: thesis: ( ex t being State of SCMPDS st
( ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = (t . (intpos i)) + n & t . b = Sum g & t . c = (p0 + 1) + (len g) ) & t . a = 0 & t . (intpos i) < 0 & ( for i being Element of NAT st i > p0 holds
t . (intpos i) = s . (intpos i) ) & not ( (IExec (I,t)) . a = 0 & I is_closed_on t & I is_halting_on t & (IExec (I,t)) . (intpos i) = (t . (intpos i)) + 1 & ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = ((t . (intpos i)) + n) + 1 & (IExec (I,t)) . c = (p0 + 1) + (len g) & (IExec (I,t)) . b = Sum g ) & ( for i being Element of NAT st i > p0 holds
(IExec (I,t)) . (intpos i) = s . (intpos i) ) ) ) or ( (IExec ((while<0 (a,i,I)),s)) . b = Sum f & while<0 (a,i,I) is_closed_on s & while<0 (a,i,I) is_halting_on s ) )
consider ff being Function of (product the Object-Kind of SCMPDS),NAT such that
A8: for t being State of SCMPDS holds
( ( t . (DataLoc ((s . a),i)) >= 0 implies ff . t = 0 ) & ( t . (DataLoc ((s . a),i)) < 0 implies ff . t = - (t . (DataLoc ((s . a),i))) ) ) by Th7;
deffunc H₁( State of SCMPDS) -> Element of NAT = ff . $1;
assume A9: for t being State of SCMPDS st ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = (t . (intpos i)) + n & t . b = Sum g & t . c = (p0 + 1) + (len g) ) & t . a = 0 & t . (intpos i) < 0 & ( for i being Element of NAT st i > p0 holds
t . (intpos i) = s . (intpos i) ) holds
( (IExec (I,t)) . a = 0 & I is_closed_on t & I is_halting_on t & (IExec (I,t)) . (intpos i) = (t . (intpos i)) + 1 & ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = ((t . (intpos i)) + n) + 1 & (IExec (I,t)) . c = (p0 + 1) + (len g) & (IExec (I,t)) . b = Sum g ) & ( for i being Element of NAT st i > p0 holds
(IExec (I,t)) . (intpos i) = s . (intpos i) ) ) ; :: thesis: ( (IExec ((while<0 (a,i,I)),s)) . b = Sum f & while<0 (a,i,I) is_closed_on s & while<0 (a,i,I) is_halting_on s )

A10: now

let t be State of SCMPDS; :: thesis: ( S₁[ Dstate t] implies ( ( H₁( Dstate t) = 0 implies not t . (DataLoc ((s . a),i)) < 0 ) & ( t . (DataLoc ((s . a),i)) >= 0 implies H₁( Dstate t) = 0 ) ) )
set dt = Dstate t;
assume S₁[ Dstate t] ; :: thesis: ( ( H₁( Dstate t) = 0 implies not t . (DataLoc ((s . a),i)) < 0 ) & ( t . (DataLoc ((s . a),i)) >= 0 implies H₁( Dstate t) = 0 ) )

hereby :: thesis: ( t . (DataLoc ((s . a),i)) >= 0 implies H₁( Dstate t) = 0 )

assume A11: H₁( Dstate t) = 0 ; :: thesis: not t . (DataLoc ((s . a),i)) < 0
assume A12: t . (DataLoc ((s . a),i)) < 0 ; :: thesis: contradiction
then (Dstate t) . (DataLoc ((s . a),i)) < 0 by SCMPDS_8:4;
then H₁( Dstate t) = - ((Dstate t) . (DataLoc ((s . a),i))) by A8;
hence contradiction by A11, A12, SCMPDS_8:4; :: thesis: verum

end;

assume t . (DataLoc ((s . a),i)) >= 0 ; :: thesis: H₁( Dstate t) = 0
then (Dstate t) . (DataLoc ((s . a),i)) >= 0 by SCMPDS_8:4;
hence H₁( Dstate t) = 0 by A8; :: thesis: verum

end;

A13: now

let t be State of SCMPDS; :: thesis: ( S₁[ Dstate t] & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 implies ( (IExec (I,t)) . a = t . a & I is_closed_on t & I is_halting_on t & H₁( Dstate (IExec (I,t))) < H₁( Dstate t) & S₁[ Dstate (IExec (I,t))] ) )
set Dt = Dstate t;
assume that
A14: S₁[ Dstate t] and
A15: t . a = s . a and
A16: t . (DataLoc ((s . a),i)) < 0 ; :: thesis: ( (IExec (I,t)) . a = t . a & I is_closed_on t & I is_halting_on t & H₁( Dstate (IExec (I,t))) < H₁( Dstate t) & S₁[ Dstate (IExec (I,t))] )
consider h being FinSequence of INT such that
A17: h is_FinSequence_on s,p0 and
A18: ( len h = ((Dstate t) . (intpos i)) + n & (Dstate t) . b = Sum h ) and
A19: (Dstate t) . c = (p0 + 1) + (len h) by A14;
A20: t . c = (p0 + 1) + (len h) by A19, SCMPDS_8:4;
set It = IExec (I,t);
set Dit = Dstate (IExec (I,t));

A21: now

let i be Element of NAT ; :: thesis: ( i > p0 implies t . (intpos i) = s . (intpos i) )
assume A22: i > p0 ; :: thesis: t . (intpos i) = s . (intpos i)
thus t . (intpos i) = (Dstate t) . (intpos i) by SCMPDS_8:4
.= s . (intpos i) by A14, A22 ; :: thesis: verum

end;

A23: intpos (0 + i) = DataLoc ((s . a),i) by A5, SCMP_GCD:5;
A24: ( len h = (t . (intpos i)) + n & t . b = Sum h ) by A18, SCMPDS_8:4;
hence (IExec (I,t)) . a = t . a by A5, A9, A15, A16, A21, A17, A20, A23; :: thesis: ( I is_closed_on t & I is_halting_on t & H₁( Dstate (IExec (I,t))) < H₁( Dstate t) & S₁[ Dstate (IExec (I,t))] )
consider g being FinSequence of INT such that
A25: g is_FinSequence_on s,p0 and
A26: len g = ((t . (intpos i)) + n) + 1 and
A27: (IExec (I,t)) . c = (p0 + 1) + (len g) and
A28: (IExec (I,t)) . b = Sum g by A5, A9, A15, A16, A21, A17, A24, A20, A23;
thus ( I is_closed_on t & I is_halting_on t ) by A5, A9, A15, A16, A21, A17, A24, A20, A23; :: thesis: ( H₁( Dstate (IExec (I,t))) < H₁( Dstate t) & S₁[ Dstate (IExec (I,t))] )
A29: (IExec (I,t)) . (intpos i) = (t . (intpos i)) + 1 by A5, A9, A15, A16, A21, A17, A24, A20, A23;

hereby :: thesis: S₁[ Dstate (IExec (I,t))]

per cases ( (IExec (I,t)) . (intpos i) >= 0 or (IExec (I,t)) . (intpos i) < 0 ) ;

suppose (IExec (I,t)) . (intpos i) >= 0 ; :: thesis: H₁( Dstate (IExec (I,t))) < H₁( Dstate t)

then (Dstate (IExec (I,t))) . (DataLoc ((s . a),i)) >= 0 by A23, SCMPDS_8:4;
then A30: H₁( Dstate (IExec (I,t))) = 0 by A8;
H₁( Dstate t) <> 0 by A10, A14, A16;
hence H₁( Dstate (IExec (I,t))) < H₁( Dstate t) by A30, NAT_1:3; :: thesis: verum

end;

suppose A31: (IExec (I,t)) . (intpos i) < 0 ; :: thesis: H₁( Dstate (IExec (I,t))) < H₁( Dstate t)

(Dstate t) . (DataLoc ((s . a),i)) < 0 by A16, SCMPDS_8:4;
then A32: H₁( Dstate t) = - ((Dstate t) . (DataLoc ((s . a),i))) by A8
.= - (t . (intpos i)) by A23, SCMPDS_8:4 ;
(Dstate (IExec (I,t))) . (DataLoc ((s . a),i)) < 0 by A23, A31, SCMPDS_8:4;
then H₁( Dstate (IExec (I,t))) = - ((Dstate (IExec (I,t))) . (DataLoc ((s . a),i))) by A8
.= - ((t . (intpos i)) + 1) by A23, A29, SCMPDS_8:4
.= (- (t . (intpos i))) - 1 ;
hence H₁( Dstate (IExec (I,t))) < H₁( Dstate t) by A32, XREAL_1:148; :: thesis: verum

end;

end;

end;

thus S₁[ Dstate (IExec (I,t))] :: thesis: verum

proof

hereby :: thesis: ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = ((Dstate (IExec (I,t))) . (intpos i)) + n & (Dstate (IExec (I,t))) . b = Sum g & (Dstate (IExec (I,t))) . (intpos i) <= 0 & (Dstate (IExec (I,t))) . c = (p0 + 1) + (len g) )

let i be Element of NAT ; :: thesis: ( i > p0 implies (Dstate (IExec (I,t))) . (intpos i) = s . (intpos i) )
assume A33: i > p0 ; :: thesis: (Dstate (IExec (I,t))) . (intpos i) = s . (intpos i)
thus (Dstate (IExec (I,t))) . (intpos i) = (IExec (I,t)) . (intpos i) by SCMPDS_8:4
.= s . (intpos i) by A5, A9, A15, A16, A21, A17, A24, A20, A23, A33 ; :: thesis: verum

end;

take g ; :: thesis: ( g is_FinSequence_on s,p0 & len g = ((Dstate (IExec (I,t))) . (intpos i)) + n & (Dstate (IExec (I,t))) . b = Sum g & (Dstate (IExec (I,t))) . (intpos i) <= 0 & (Dstate (IExec (I,t))) . c = (p0 + 1) + (len g) )
thus g is_FinSequence_on s,p0 by A25; :: thesis: ( len g = ((Dstate (IExec (I,t))) . (intpos i)) + n & (Dstate (IExec (I,t))) . b = Sum g & (Dstate (IExec (I,t))) . (intpos i) <= 0 & (Dstate (IExec (I,t))) . c = (p0 + 1) + (len g) )
thus len g = ((IExec (I,t)) . (intpos i)) + n by A29, A26
.= ((Dstate (IExec (I,t))) . (intpos i)) + n by SCMPDS_8:4 ; :: thesis: ( (Dstate (IExec (I,t))) . b = Sum g & (Dstate (IExec (I,t))) . (intpos i) <= 0 & (Dstate (IExec (I,t))) . c = (p0 + 1) + (len g) )
thus (Dstate (IExec (I,t))) . b = Sum g by A28, SCMPDS_8:4; :: thesis: ( (Dstate (IExec (I,t))) . (intpos i) <= 0 & (Dstate (IExec (I,t))) . c = (p0 + 1) + (len g) )
(Dstate (IExec (I,t))) . (intpos i) = (t . (intpos i)) + 1 by A29, SCMPDS_8:4;
hence (Dstate (IExec (I,t))) . (intpos i) <= 0 by A16, A23, INT_1:20; :: thesis: (Dstate (IExec (I,t))) . c = (p0 + 1) + (len g)
thus (Dstate (IExec (I,t))) . c = (p0 + 1) + (len g) by A27, SCMPDS_8:4; :: thesis: verum

end;

end;

A34: S₁[ Dstate s]

proof

set Ds = Dstate s;
thus for i being Element of NAT st i > p0 holds
(Dstate s) . (intpos i) = s . (intpos i) by SCMPDS_8:4; :: thesis: ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = ((Dstate s) . (intpos i)) + n & (Dstate s) . b = Sum g & (Dstate s) . (intpos i) <= 0 & (Dstate s) . c = (p0 + 1) + (len g) )
consider h being FinSequence of INT such that
A35: len h = 0 and
A36: h is_FinSequence_on s,p0 by SCPISORT:3;
take h ; :: thesis: ( h is_FinSequence_on s,p0 & len h = ((Dstate s) . (intpos i)) + n & (Dstate s) . b = Sum h & (Dstate s) . (intpos i) <= 0 & (Dstate s) . c = (p0 + 1) + (len h) )
thus h is_FinSequence_on s,p0 by A36; :: thesis: ( len h = ((Dstate s) . (intpos i)) + n & (Dstate s) . b = Sum h & (Dstate s) . (intpos i) <= 0 & (Dstate s) . c = (p0 + 1) + (len h) )
thus len h = (s . (intpos i)) + n by A6, A35
.= ((Dstate s) . (intpos i)) + n by SCMPDS_8:4 ; :: thesis: ( (Dstate s) . b = Sum h & (Dstate s) . (intpos i) <= 0 & (Dstate s) . c = (p0 + 1) + (len h) )
h = <*> REAL by A35;
hence (Dstate s) . b = Sum h by A4, RVSUM_1:102, SCMPDS_8:4; :: thesis: ( (Dstate s) . (intpos i) <= 0 & (Dstate s) . c = (p0 + 1) + (len h) )
thus (Dstate s) . (intpos i) <= 0 by A6, SCMPDS_8:4; :: thesis: (Dstate s) . c = (p0 + 1) + (len h)
thus (Dstate s) . c = (p0 + 1) + (len h) by A7, A35, SCMPDS_8:4; :: thesis: verum

end;

A37: ( H₁( Dstate (IExec ((while<0 (a,i,I)),s))) = 0 & S₁[ Dstate (IExec ((while<0 (a,i,I)),s))] ) from SCPINVAR:sch 1(A1, A10, A34, A13);
then consider g being FinSequence of INT such that
A38: g is_FinSequence_on s,p0 and
A39: len g = ((Dstate (IExec ((while<0 (a,i,I)),s))) . (intpos i)) + n and
A40: (Dstate (IExec ((while<0 (a,i,I)),s))) . b = Sum g and
A41: (Dstate (IExec ((while<0 (a,i,I)),s))) . (intpos i) <= 0 ;
(Dstate (IExec ((while<0 (a,i,I)),s))) . (intpos i) = (IExec ((while<0 (a,i,I)),s)) . (intpos (0 + i)) by SCMPDS_8:4
.= (IExec ((while<0 (a,i,I)),s)) . (DataLoc ((s . a),i)) by A5, SCMP_GCD:5 ;
then (Dstate (IExec ((while<0 (a,i,I)),s))) . (intpos i) >= 0 by A10, A37;
then A42: (Dstate (IExec ((while<0 (a,i,I)),s))) . (intpos i) = 0 by A41, XXREAL_0:1;

now

let i be Nat; :: thesis: ( i in dom f implies f . i = g . i )
reconsider a = i as Element of NAT by ORDINAL1:def 13;
assume i in dom f ; :: thesis: f . i = g . i
then A43: ( 1 <= i & i <= n ) by A3, FINSEQ_3:27;
hence f . i = s . (intpos (p0 + a)) by A2, A3, SCPISORT:def 1
.= g . i by A38, A39, A42, A43, SCPISORT:def 1 ;
:: thesis: verum

end;

then f = g by A3, A39, A42, FINSEQ_2:10;
hence (IExec ((while<0 (a,i,I)),s)) . b = Sum f by A40, SCMPDS_8:4; :: thesis: ( while<0 (a,i,I) is_closed_on s & while<0 (a,i,I) is_halting_on s )
A44: for t being State of SCMPDS st S₁[ Dstate t] & H₁( Dstate t) = 0 holds
t . (DataLoc ((s . a),i)) >= 0 by A10;
( ( H₁(s) = H₁(s) or S₁[s] ) & while<0 (a,i,I) is_closed_on s & while<0 (a,i,I) is_halting_on s ) from SCMPDS_8:sch 1(A1, A44, A34, A13);
hence ( while<0 (a,i,I) is_closed_on s & while<0 (a,i,I) is_halting_on s ) ; :: thesis: verum