let P be Instruction-Sequence of SCMPDS; for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of
for a, x1, x2, x3, x4 being Int_position
for i, c, md being Integer st s . x4 = ((s . x3) - c) + (s . x1) & md <= (s . x3) - c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x4 = ((t . x3) - c) + (t . x1) & md <= (t . x3) - c & t . x2 = s . x2 & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & (IExec (I,Q,t)) . x4 = (((IExec (I,Q,t)) . x3) - c) + ((IExec (I,Q,t)) . x1) & md <= ((IExec (I,Q,t)) . x3) - c & (IExec (I,Q,t)) . x2 = t . x2 ) ) holds
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ) )
let s be 0 -started State of SCMPDS; for I being halt-free shiftable Program of
for a, x1, x2, x3, x4 being Int_position
for i, c, md being Integer st s . x4 = ((s . x3) - c) + (s . x1) & md <= (s . x3) - c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x4 = ((t . x3) - c) + (t . x1) & md <= (t . x3) - c & t . x2 = s . x2 & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & (IExec (I,Q,t)) . x4 = (((IExec (I,Q,t)) . x3) - c) + ((IExec (I,Q,t)) . x1) & md <= ((IExec (I,Q,t)) . x3) - c & (IExec (I,Q,t)) . x2 = t . x2 ) ) holds
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ) )
let I be halt-free shiftable Program of ; for a, x1, x2, x3, x4 being Int_position
for i, c, md being Integer st s . x4 = ((s . x3) - c) + (s . x1) & md <= (s . x3) - c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x4 = ((t . x3) - c) + (t . x1) & md <= (t . x3) - c & t . x2 = s . x2 & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & (IExec (I,Q,t)) . x4 = (((IExec (I,Q,t)) . x3) - c) + ((IExec (I,Q,t)) . x1) & md <= ((IExec (I,Q,t)) . x3) - c & (IExec (I,Q,t)) . x2 = t . x2 ) ) holds
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ) )
let a, x1, x2, x3, x4 be Int_position; for i, c, md being Integer st s . x4 = ((s . x3) - c) + (s . x1) & md <= (s . x3) - c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x4 = ((t . x3) - c) + (t . x1) & md <= (t . x3) - c & t . x2 = s . x2 & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & (IExec (I,Q,t)) . x4 = (((IExec (I,Q,t)) . x3) - c) + ((IExec (I,Q,t)) . x1) & md <= ((IExec (I,Q,t)) . x3) - c & (IExec (I,Q,t)) . x2 = t . x2 ) ) holds
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ) )
let i, c, md be Integer; ( s . x4 = ((s . x3) - c) + (s . x1) & md <= (s . x3) - c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x4 = ((t . x3) - c) + (t . x1) & md <= (t . x3) - c & t . x2 = s . x2 & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & (IExec (I,Q,t)) . x4 = (((IExec (I,Q,t)) . x3) - c) + ((IExec (I,Q,t)) . x1) & md <= ((IExec (I,Q,t)) . x3) - c & (IExec (I,Q,t)) . x2 = t . x2 ) ) implies ( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ) ) )
set b = DataLoc ((s . a),i);
defpred S1[ set ] means ex t being State of SCMPDS st
( t = $1 & t . x4 = ((t . x3) - c) + (t . x1) & md <= (t . x3) - c & t . x2 = s . x2 );
assume that
A1:
s . x4 = ((s . x3) - c) + (s . x1)
and
A2:
md <= (s . x3) - c
; ( ex t being 0 -started State of SCMPDS ex Q being Instruction-Sequence of SCMPDS st
( t . x4 = ((t . x3) - c) + (t . x1) & md <= (t . x3) - c & t . x2 = s . x2 & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 & not ( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & (IExec (I,Q,t)) . x4 = (((IExec (I,Q,t)) . x3) - c) + ((IExec (I,Q,t)) . x1) & md <= ((IExec (I,Q,t)) . x3) - c & (IExec (I,Q,t)) . x2 = t . x2 ) ) or ( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ) ) )
consider f being Function of (product (the_Values_of SCMPDS)),NAT such that
A3:
for s being State of SCMPDS holds
( ( s . (DataLoc ((s . a),i)) <= 0 implies f . s = 0 ) & ( s . (DataLoc ((s . a),i)) > 0 implies f . s = s . (DataLoc ((s . a),i)) ) )
by SCMPDS_8:5;
deffunc H1( State of SCMPDS) -> Element of NAT = f . $1;
A4:
for t being 0 -started State of SCMPDS st S1[t] & H1(t) = 0 holds
t . (DataLoc ((s . a),i)) <= 0
by A3;
assume A5:
for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x4 = ((t . x3) - c) + (t . x1) & md <= (t . x3) - c & t . x2 = s . x2 & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & (IExec (I,Q,t)) . x4 = (((IExec (I,Q,t)) . x3) - c) + ((IExec (I,Q,t)) . x1) & md <= ((IExec (I,Q,t)) . x3) - c & (IExec (I,Q,t)) . x2 = t . x2 )
; ( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ) )
A6:
now for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st S1[t] & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & H1( Initialize (IExec (I,Q,t))) < H1(t) & S1[ Initialize (IExec (I,Q,t))] )let t be
0 -started State of
SCMPDS;
for Q being Instruction-Sequence of SCMPDS st S1[t] & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & H1( Initialize (IExec (I,Q,t))) < H1(t) & S1[ Initialize (IExec (I,Q,t))] )let Q be
Instruction-Sequence of
SCMPDS;
( S1[t] & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 implies ( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & H1( Initialize (IExec (I,Q,t))) < H1(t) & S1[ Initialize (IExec (I,Q,t))] ) )assume that A7:
S1[
t]
and A8:
t . a = s . a
and A9:
t . (DataLoc ((s . a),i)) > 0
;
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & H1( Initialize (IExec (I,Q,t))) < H1(t) & S1[ Initialize (IExec (I,Q,t))] )set It =
IExec (
I,
Q,
t);
set t2 =
Initialize (IExec (I,Q,t));
consider v being
State of
SCMPDS such that A10:
v = t
and A11:
v . x4 = ((v . x3) - c) + (v . x1)
and A12:
md <= (v . x3) - c
and A13:
v . x2 = s . x2
by A7;
A14:
t . x2 = s . x2
by A10, A13;
A15:
t . x4 = ((t . x3) - c) + (t . x1)
by A10, A11;
A16:
md <= (t . x3) - c
by A10, A12;
thus
(
(IExec (I,Q,t)) . a = t . a &
I is_closed_on t,
Q &
I is_halting_on t,
Q )
by A5, A8, A9, A15, A13, A10, A12;
( H1( Initialize (IExec (I,Q,t))) < H1(t) & S1[ Initialize (IExec (I,Q,t))] )thus
H1(
Initialize (IExec (I,Q,t)))
< H1(
t)
S1[ Initialize (IExec (I,Q,t))]proof
A17:
H1(
t)
= t . (DataLoc ((s . a),i))
by A3, A9;
assume A18:
H1(
Initialize (IExec (I,Q,t)))
>= H1(
t)
;
contradiction
then
(Initialize (IExec (I,Q,t))) . (DataLoc ((s . a),i)) > 0
by A3, A9, A17;
then H1(
Initialize (IExec (I,Q,t))) =
(Initialize (IExec (I,Q,t))) . (DataLoc ((s . a),i))
by A3
.=
(IExec (I,Q,t)) . (DataLoc ((s . a),i))
by SCMPDS_5:15
;
hence
contradiction
by A5, A8, A9, A15, A16, A10, A13, A18, A17;
verum
end; thus
S1[
Initialize (IExec (I,Q,t))]
verumproof
take v =
Initialize (IExec (I,Q,t));
( v = Initialize (IExec (I,Q,t)) & v . x4 = ((v . x3) - c) + (v . x1) & md <= (v . x3) - c & v . x2 = s . x2 )
thus
v = Initialize (IExec (I,Q,t))
;
( v . x4 = ((v . x3) - c) + (v . x1) & md <= (v . x3) - c & v . x2 = s . x2 )
(IExec (I,Q,t)) . x4 = (((IExec (I,Q,t)) . x3) - c) + ((IExec (I,Q,t)) . x1)
by A5, A8, A9, A15, A16, A14;
then
v . x4 = (((IExec (I,Q,t)) . x3) - c) + ((IExec (I,Q,t)) . x1)
by SCMPDS_5:15;
then
v . x4 = ((v . x3) - c) + ((IExec (I,Q,t)) . x1)
by SCMPDS_5:15;
hence
v . x4 = ((v . x3) - c) + (v . x1)
by SCMPDS_5:15;
( md <= (v . x3) - c & v . x2 = s . x2 )
md <= ((IExec (I,Q,t)) . x3) - c
by A5, A8, A9, A15, A16, A14;
hence
md <= (v . x3) - c
by SCMPDS_5:15;
v . x2 = s . x2
(IExec (I,Q,t)) . x2 = t . x2
by A5, A8, A9, A15, A16, A10, A13;
hence
v . x2 = s . x2
by A10, A13, SCMPDS_5:15;
verum
end; end;
A19:
S1[s]
by A1, A2;
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P )
from SCMPDS_8:sch 3(A4, A19, A6);
hence
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P )
; ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) )
assume A20:
s . (DataLoc ((s . a),i)) > 0
; IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s))))
IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s))))
from SCMPDS_8:sch 4(A20, A4, A19, A6);
hence
IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s))))
; verum