let P be Instruction-Sequence of SCMPDS; for s being State of SCMPDS
for I being halt-free shiftable Program of
for a being Int_position
for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 & I is_closed_on s,P & I is_halting_on s,P holds
IExec ((if=0 (a,k1,I)),P,(Initialize s)) = (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS))
let s be State of SCMPDS; for I being halt-free shiftable Program of
for a being Int_position
for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 & I is_closed_on s,P & I is_halting_on s,P holds
IExec ((if=0 (a,k1,I)),P,(Initialize s)) = (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS))
let I be halt-free shiftable Program of ; for a being Int_position
for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 & I is_closed_on s,P & I is_halting_on s,P holds
IExec ((if=0 (a,k1,I)),P,(Initialize s)) = (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS))
let a be Int_position; for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 & I is_closed_on s,P & I is_halting_on s,P holds
IExec ((if=0 (a,k1,I)),P,(Initialize s)) = (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS))
let k1 be Integer; ( s . (DataLoc ((s . a),k1)) = 0 & I is_closed_on s,P & I is_halting_on s,P implies IExec ((if=0 (a,k1,I)),P,(Initialize s)) = (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS)) )
set b = DataLoc ((s . a),k1);
assume A1:
s . (DataLoc ((s . a),k1)) = 0
; ( not I is_closed_on s,P or not I is_halting_on s,P or IExec ((if=0 (a,k1,I)),P,(Initialize s)) = (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS)) )
set i = (a,k1) <>0_goto ((card I) + 1);
set IF = if=0 (a,k1,I);
set pI = stop I;
set pIF = stop (if=0 (a,k1,I));
set s2 = Initialize s;
set P2 = P +* (stop I);
set s3 = Initialize s;
set P3 = P +* (stop (if=0 (a,k1,I)));
set s4 = Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),1);
set P4 = P +* (stop (if=0 (a,k1,I)));
A2:
IC (Initialize s) = 0
by MEMSTR_0:47;
A3:
not DataLoc ((s . a),k1) in dom (Start-At (0,SCMPDS))
by SCMPDS_4:18;
A4: Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),(0 + 1)) =
Following ((P +* (stop (if=0 (a,k1,I)))),(Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),0)))
by EXTPRO_1:3
.=
Following ((P +* (stop (if=0 (a,k1,I)))),(Initialize s))
by EXTPRO_1:2
.=
Exec (((a,k1) <>0_goto ((card I) + 1)),(Initialize s))
by Th3
;
not a in dom (Start-At (0,SCMPDS))
by SCMPDS_4:18;
then (Initialize s) . (DataLoc (((Initialize s) . a),k1)) =
(Initialize s) . (DataLoc ((s . a),k1))
by FUNCT_4:11
.=
0
by A1, A3, FUNCT_4:11
;
then A5: IC (Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),1)) =
(IC (Initialize s)) + 1
by A4, SCMPDS_2:55
.=
0 + 1
by A2
;
for a being Int_position holds (Initialize s) . a = (Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),1)) . a
by A4, SCMPDS_2:55;
then A6:
DataPart (Initialize s) = DataPart (Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),1))
by SCMPDS_4:8;
assume A7:
I is_closed_on s,P
; ( not I is_halting_on s,P or IExec ((if=0 (a,k1,I)),P,(Initialize s)) = (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS)) )
then A8:
I is_closed_on Initialize s,P +* (stop I)
;
set SAl = Start-At (((card I) + 1),SCMPDS);
A9:
( Start-At (0,SCMPDS) c= Initialize s & Shift ((stop I),1) c= P +* (stop (if=0 (a,k1,I))) )
by Lm6, FUNCT_4:25;
A10:
stop I c= P +* (stop I)
by FUNCT_4:25;
assume A11:
I is_halting_on s,P
; IExec ((if=0 (a,k1,I)),P,(Initialize s)) = (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS))
then A12:
P +* (stop I) halts_on Initialize s
;
A13:
Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1)) = Comput ((P +* (stop (if=0 (a,k1,I)))),(Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),1)),(LifeSpan ((P +* (stop I)),(Initialize s))))
by EXTPRO_1:4;
A14: CurInstr ((P +* (stop (if=0 (a,k1,I)))),(Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1)))) =
CurInstr ((P +* (stop (if=0 (a,k1,I)))),(Comput ((P +* (stop (if=0 (a,k1,I)))),(Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),1)),(LifeSpan ((P +* (stop I)),(Initialize s))))))
by A13
.=
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))
by A8, A9, A5, A6, Th22, A10
.=
halt SCMPDS
by A12, EXTPRO_1:def 15
;
then A15:
P +* (stop (if=0 (a,k1,I))) halts_on Initialize s
by EXTPRO_1:29;
A16:
CurInstr ((P +* (stop (if=0 (a,k1,I)))),(Initialize s)) = (a,k1) <>0_goto ((card I) + 1)
by Th3;
now for l being Nat st l < (LifeSpan ((P +* (stop I)),(Initialize s))) + 1 holds
CurInstr ((P +* (stop (if=0 (a,k1,I)))),(Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),l))) <> halt SCMPDSlet l be
Nat;
( l < (LifeSpan ((P +* (stop I)),(Initialize s))) + 1 implies CurInstr ((P +* (stop (if=0 (a,k1,I)))),(Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),b1))) <> halt SCMPDS )assume A17:
l < (LifeSpan ((P +* (stop I)),(Initialize s))) + 1
;
CurInstr ((P +* (stop (if=0 (a,k1,I)))),(Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),b1))) <> halt SCMPDSA18:
Comput (
(P +* (stop (if=0 (a,k1,I)))),
(Initialize s),
0)
= Initialize s
by EXTPRO_1:2;
per cases
( l = 0 or l <> 0 )
;
suppose
l = 0
;
CurInstr ((P +* (stop (if=0 (a,k1,I)))),(Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),b1))) <> halt SCMPDSthen
CurInstr (
(P +* (stop (if=0 (a,k1,I)))),
(Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),l)))
= CurInstr (
(P +* (stop (if=0 (a,k1,I)))),
(Initialize s))
by A18;
hence
CurInstr (
(P +* (stop (if=0 (a,k1,I)))),
(Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),l)))
<> halt SCMPDS
by A16;
verum end; suppose
l <> 0
;
not CurInstr ((P +* (stop (if=0 (a,k1,I)))),(Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),b1))) = halt SCMPDSthen consider n being
Nat such that A19:
l = n + 1
by NAT_1:6;
reconsider n =
n as
Nat ;
A20:
n < LifeSpan (
(P +* (stop I)),
(Initialize s))
by A17, A19, XREAL_1:6;
assume A21:
CurInstr (
(P +* (stop (if=0 (a,k1,I)))),
(Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),l)))
= halt SCMPDS
;
contradictionA22:
Comput (
(P +* (stop (if=0 (a,k1,I)))),
(Initialize s),
(n + 1))
= Comput (
(P +* (stop (if=0 (a,k1,I)))),
(Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),1)),
n)
by EXTPRO_1:4;
CurInstr (
(P +* (stop I)),
(Comput ((P +* (stop I)),(Initialize s),n))) =
CurInstr (
(P +* (stop (if=0 (a,k1,I)))),
(Comput ((P +* (stop (if=0 (a,k1,I)))),(Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),1)),n)))
by A8, A9, A5, A6, Th22, A10
.=
halt SCMPDS
by A19, A21, A22
;
hence
contradiction
by A12, A20, EXTPRO_1:def 15;
verum end; end;
then
for l being Nat st CurInstr ((P +* (stop (if=0 (a,k1,I)))),(Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),l))) = halt SCMPDS holds
(LifeSpan ((P +* (stop I)),(Initialize s))) + 1 <= l
;
then A23:
LifeSpan ((P +* (stop (if=0 (a,k1,I)))),(Initialize s)) = (LifeSpan ((P +* (stop I)),(Initialize s))) + 1
by A14, A15, EXTPRO_1:def 15;
A24: DataPart (Result ((P +* (stop I)),(Initialize s))) =
DataPart (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))
by A12, EXTPRO_1:23
.=
DataPart (Comput ((P +* (stop (if=0 (a,k1,I)))),(Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),1)),(LifeSpan ((P +* (stop I)),(Initialize s)))))
by A8, A9, A5, A6, Th22, A10
.=
DataPart (Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1)))
by EXTPRO_1:4
.=
DataPart (Result ((P +* (stop (if=0 (a,k1,I)))),(Initialize s)))
by A15, A23, EXTPRO_1:23
;
A25:
now for x being object st x in dom (IExec ((if=0 (a,k1,I)),P,(Initialize s))) holds
(IExec ((if=0 (a,k1,I)),P,(Initialize s))) . x = ((IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS))) . xlet x be
object ;
( x in dom (IExec ((if=0 (a,k1,I)),P,(Initialize s))) implies (IExec ((if=0 (a,k1,I)),P,(Initialize s))) . b1 = ((IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS))) . b1 )A26:
dom (Start-At (((card I) + 1),SCMPDS)) = {(IC )}
by FUNCOP_1:13;
assume A27:
x in dom (IExec ((if=0 (a,k1,I)),P,(Initialize s)))
;
(IExec ((if=0 (a,k1,I)),P,(Initialize s))) . b1 = ((IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS))) . b1per cases
( x is Int_position or x = IC )
by A27, SCMPDS_4:6;
suppose A28:
x is
Int_position
;
(IExec ((if=0 (a,k1,I)),P,(Initialize s))) . b1 = ((IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS))) . b1then
x <> IC
by SCMPDS_2:43;
then A29:
not
x in dom (Start-At (((card I) + 1),SCMPDS))
by A26, TARSKI:def 1;
thus (IExec ((if=0 (a,k1,I)),P,(Initialize s))) . x =
(Result ((P +* (stop (if=0 (a,k1,I)))),(Initialize s))) . x
.=
(Result ((P +* (stop I)),(Initialize s))) . x
by A24, A28, SCMPDS_4:8
.=
(IExec (I,P,(Initialize s))) . x
.=
((IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS))) . x
by A29, FUNCT_4:11
;
verum end; suppose A30:
x = IC
;
(IExec ((if=0 (a,k1,I)),P,(Initialize s))) . b1 = ((IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS))) . b1A31:
IC (Result ((P +* (stop I)),(Initialize s))) =
IC (IExec (I,P,(Initialize s)))
.=
card I
by A7, A11, Th25
;
A32:
x in dom (Start-At (((card I) + 1),SCMPDS))
by A26, A30, TARSKI:def 1;
thus (IExec ((if=0 (a,k1,I)),P,(Initialize s))) . x =
(Result ((P +* (stop (if=0 (a,k1,I)))),(Initialize s))) . x
.=
(Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1))) . x
by A15, A23, EXTPRO_1:23
.=
IC (Comput ((P +* (stop (if=0 (a,k1,I)))),(Comput ((P +* (stop (if=0 (a,k1,I)))),(Initialize s),1)),(LifeSpan ((P +* (stop I)),(Initialize s)))))
by A30, EXTPRO_1:4
.=
(IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) + 1
by A8, A9, A5, A6, Th22, A10
.=
(IC (Result ((P +* (stop I)),(Initialize s)))) + 1
by A12, EXTPRO_1:23
.=
IC (Start-At (((card I) + 1),SCMPDS))
by A31, FUNCOP_1:72
.=
((IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS))) . x
by A30, A32, FUNCT_4:13
;
verum end; end;
dom (IExec ((if=0 (a,k1,I)),P,(Initialize s))) =
the carrier of SCMPDS
by PARTFUN1:def 2
.=
dom ((IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS)))
by PARTFUN1:def 2
;
hence
IExec ((if=0 (a,k1,I)),P,(Initialize s)) = (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS))
by A25, FUNCT_1:2; verum