let s be State of SCMPDS; for I being halt-free shiftable Program of SCMPDS
for a being Int_position
for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 & I is_closed_on s & I is_halting_on s holds
IExec ((if>0 (a,k1,I)),s) = (IExec (I,s)) +* (Start-At (((card I) + 1),SCMPDS))
let I be halt-free shiftable Program of SCMPDS; for a being Int_position
for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 & I is_closed_on s & I is_halting_on s holds
IExec ((if>0 (a,k1,I)),s) = (IExec (I,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 & I is_halting_on s holds
IExec ((if>0 (a,k1,I)),s) = (IExec (I,s)) +* (Start-At (((card I) + 1),SCMPDS))
let k1 be Integer; ( s . (DataLoc ((s . a),k1)) > 0 & I is_closed_on s & I is_halting_on s implies IExec ((if>0 (a,k1,I)),s) = (IExec (I,s)) +* (Start-At (((card I) + 1),SCMPDS)) )
set b = DataLoc ((s . a),k1);
set IF = if>0 (a,k1,I);
set pI = stop I;
set pIF = stop (if>0 (a,k1,I));
set s2 = (Initialize s) +* (stop I);
set s3 = (Initialize s) +* (stop (if>0 (a,k1,I)));
set s4 = Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1);
set i = (a,k1) <=0_goto ((card I) + 1);
set SAl = Start-At (((card I) + 1),SCMPDS);
I1:
s +* (Initialize (stop I)) = (Initialize s) +* (stop I)
by COMPOS_1:125;
I2:
s +* (Initialize (stop (if>0 (a,k1,I)))) = (Initialize s) +* (stop (if>0 (a,k1,I)))
by COMPOS_1:125;
A1:
IC ((Initialize s) +* (stop (if>0 (a,k1,I)))) = 0
by I2, FUNCT_4:26, SCMPDS_5:18;
A2:
not DataLoc ((s . a),k1) in dom (Initialize (stop (if>0 (a,k1,I))))
by SCMPDS_4:31;
not a in dom (Initialize (stop (if>0 (a,k1,I))))
by SCMPDS_4:31;
then A3: ((Initialize s) +* (stop (if>0 (a,k1,I)))) . (DataLoc ((((Initialize s) +* (stop (if>0 (a,k1,I)))) . a),k1)) =
((Initialize s) +* (stop (if>0 (a,k1,I)))) . (DataLoc ((s . a),k1))
by I2, FUNCT_4:12
.=
s . (DataLoc ((s . a),k1))
by A2, I2, FUNCT_4:12
;
A4: Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),(0 + 1)) =
Following ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),0)))
by EXTPRO_1:4
.=
Following ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))))
by EXTPRO_1:3
.=
Exec (((a,k1) <=0_goto ((card I) + 1)),((Initialize s) +* (stop (if>0 (a,k1,I)))))
by Th22, I2
;
assume
s . (DataLoc ((s . a),k1)) > 0
; ( not I is_closed_on s or not I is_halting_on s or IExec ((if>0 (a,k1,I)),s) = (IExec (I,s)) +* (Start-At (((card I) + 1),SCMPDS)) )
then A5: IC (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1)) =
succ (IC ((Initialize s) +* (stop (if>0 (a,k1,I)))))
by A4, A3, SCMPDS_2:68
.=
0 + 1
by A1
;
A6:
DataPart ((Initialize s) +* (stop I)) = DataPart ((Initialize s) +* (stop (if>0 (a,k1,I))))
by COMPOS_1:138, FUNCT_7:134;
now let a be
Int_position ;
((Initialize s) +* (stop I)) . a = (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1)) . athus ((Initialize s) +* (stop I)) . a =
((Initialize s) +* (stop (if>0 (a,k1,I)))) . a
by A6, SCMPDS_4:23
.=
(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1)) . a
by A4, SCMPDS_2:68
;
verum end;
then A7:
DataPart ((Initialize s) +* (stop I)) = DataPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1))
by SCMPDS_4:23;
assume A8:
I is_closed_on s
; ( not I is_halting_on s or IExec ((if>0 (a,k1,I)),s) = (IExec (I,s)) +* (Start-At (((card I) + 1),SCMPDS)) )
then A9:
I is_closed_on (Initialize s) +* (stop I)
by Th38;
A10:
dom (ProgramPart s) = NAT
by COMPOS_1:34;
A11:
( Initialize (stop I) c= (Initialize s) +* (stop I) & Shift ((stop I),1) c= Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1) )
by Lm5, I1, FUNCT_4:26;
assume A12:
I is_halting_on s
; IExec ((if>0 (a,k1,I)),s) = (IExec (I,s)) +* (Start-At (((card I) + 1),SCMPDS))
then A13:
ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I)
by Def3;
T:
ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I)))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1))
by AMI_1:123;
x:
Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1)) = Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))
by EXTPRO_1:5;
TX4:
ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1)) = ProgramPart (Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))
by AMI_1:123;
TX2:
ProgramPart ((Initialize s) +* (stop I)) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))
by AMI_1:123;
A14: CurInstr ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1)))) =
CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1))),(Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))))
by x, T
.=
CurInstr ((ProgramPart ((Initialize s) +* (stop I))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))))
by A9, A11, A5, A7, Th45, TX2, TX4
.=
halt SCMPDS
by A13, EXTPRO_1:def 14
;
then A15:
ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I)))) halts_on (Initialize s) +* (stop (if>0 (a,k1,I)))
by EXTPRO_1:30;
A16:
CurInstr ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I))))) = (a,k1) <=0_goto ((card I) + 1)
by Th22, I2;
now let l be
Element of
NAT ;
( l < (LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1 implies CurInstr ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),b1))) <> halt SCMPDS )assume A17:
l < (LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1
;
CurInstr ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),b1))) <> halt SCMPDSu:
Comput (
(ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),
((Initialize s) +* (stop (if>0 (a,k1,I)))),
0)
= (Initialize s) +* (stop (if>0 (a,k1,I)))
by EXTPRO_1:3;
per cases
( l = 0 or l <> 0 )
;
suppose
l = 0
;
CurInstr ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),b1))) <> halt SCMPDSthen
CurInstr (
(ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),
(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),l)))
= CurInstr (
(ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),
((Initialize s) +* (stop (if>0 (a,k1,I)))))
by u;
hence
CurInstr (
(ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),
(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),l)))
<> halt SCMPDS
by A16, Th30;
verum end; suppose
l <> 0
;
not CurInstr ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),b1))) = halt SCMPDSthen consider n being
Nat such that A18:
l = n + 1
by NAT_1:6;
reconsider n =
n as
Element of
NAT by ORDINAL1:def 13;
A19:
n < LifeSpan (
(ProgramPart ((Initialize s) +* (stop I))),
((Initialize s) +* (stop I)))
by A17, A18, XREAL_1:8;
assume A20:
CurInstr (
(ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),
(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),l)))
= halt SCMPDS
;
contradictionT:
ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I)))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1))
by AMI_1:123;
x:
Comput (
(ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),
((Initialize s) +* (stop (if>0 (a,k1,I)))),
(n + 1))
= Comput (
(ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),
(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1)),
n)
by EXTPRO_1:5;
TX2:
ProgramPart ((Initialize s) +* (stop I)) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))
by AMI_1:123;
TX4:
ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1)) = ProgramPart (Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1)),n))
by AMI_1:123;
CurInstr (
(ProgramPart ((Initialize s) +* (stop I))),
(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) =
CurInstr (
(ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1))),
(Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1)),n)))
by A9, A11, A5, A7, TX2, TX4, Th45
.=
halt SCMPDS
by A18, A20, x, T
;
hence
contradiction
by A13, A19, EXTPRO_1:def 14;
verum end; end;
then
for l being Element of NAT st CurInstr ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),l))) = halt SCMPDS holds
(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1 <= l
;
then A21:
LifeSpan ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I))))) = (LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1
by A14, A15, EXTPRO_1:def 14;
T:
ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I)))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1))
by AMI_1:123;
A22: DataPart (Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) =
DataPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))
by A13, EXTPRO_1:23
.=
DataPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))
by A9, A11, A5, A7, Th45, T
.=
DataPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1)))
by EXTPRO_1:5
.=
DataPart (Result ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I))))))
by A15, A21, EXTPRO_1:23
;
A23:
now let x be
set ;
( x in dom (IExec ((if>0 (a,k1,I)),s)) implies (IExec ((if>0 (a,k1,I)),s)) . b1 = ((IExec (I,s)) +* (Start-At (((card I) + 1),SCMPDS))) . b1 )A26:
dom (Start-At (((card I) + 1),SCMPDS)) = {(IC SCMPDS)}
by FUNCOP_1:19;
assume A27:
x in dom (IExec ((if>0 (a,k1,I)),s))
;
(IExec ((if>0 (a,k1,I)),s)) . b1 = ((IExec (I,s)) +* (Start-At (((card I) + 1),SCMPDS))) . b1per cases
( x is Int_position or x = IC SCMPDS or x is Element of NAT )
by A27, SCMPDS_4:20;
suppose A28:
x is
Int_position
;
(IExec ((if>0 (a,k1,I)),s)) . b1 = ((IExec (I,s)) +* (Start-At (((card I) + 1),SCMPDS))) . b1then
x <> IC SCMPDS
by SCMPDS_2:52;
then A29:
not
x in dom (Start-At (((card I) + 1),SCMPDS))
by A26, TARSKI:def 1;
A30:
not
x in dom (s | NAT)
by A10, A28, SCMPDS_2:53;
hence (IExec ((if>0 (a,k1,I)),s)) . x =
(Result ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))))) . x
by FUNCT_4:12
.=
(Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) . x
by A22, A28, SCMPDS_4:23
.=
(IExec (I,s)) . x
by A30, FUNCT_4:12
.=
((IExec (I,s)) +* (Start-At (((card I) + 1),SCMPDS))) . x
by A29, FUNCT_4:12
;
verum end; suppose A31:
x = IC SCMPDS
;
(IExec ((if>0 (a,k1,I)),s)) . b1 = ((IExec (I,s)) +* (Start-At (((card I) + 1),SCMPDS))) . b1A32:
not
x in dom (s | NAT)
by A10, A31, COMPOS_1:3;
then A33:
IC (Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) =
IC (IExec (I,s))
by A31, FUNCT_4:12
.=
card I
by A8, A12, Th48
;
A34:
x in dom (Start-At (((card I) + 1),SCMPDS))
by A26, A31, TARSKI:def 1;
T:
ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I)))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1))
by AMI_1:123;
thus (IExec ((if>0 (a,k1,I)),s)) . x =
(Result ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))))) . x
by A32, FUNCT_4:12
.=
(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1))) . x
by A15, A21, EXTPRO_1:23
.=
IC (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I))))),((Initialize s) +* (stop (if>0 (a,k1,I)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))
by A31, EXTPRO_1:5
.=
(IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) + 1
by A9, A11, A5, A7, Th45, T
.=
(IC (Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) + 1
by A13, EXTPRO_1:23
.=
(Start-At (((card I) + 1),SCMPDS)) . (IC SCMPDS)
by A33, FUNCOP_1:87
.=
((IExec (I,s)) +* (Start-At (((card I) + 1),SCMPDS))) . x
by A31, A34, FUNCT_4:14
;
verum end; end;
dom (IExec ((if>0 (a,k1,I)),s)) =
the carrier of SCMPDS
by PARTFUN1:def 4
.=
dom ((IExec (I,s)) +* (Start-At (((card I) + 1),SCMPDS)))
by PARTFUN1:def 4
;
hence
IExec ((if>0 (a,k1,I)),s) = (IExec (I,s)) +* (Start-At (((card I) + 1),SCMPDS))
by A23, FUNCT_1:9; verum