let s be State of SCMPDS ; for I being shiftable No-StopCode 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) + 2),SCMPDS )
let I be shiftable No-StopCode 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) + 2),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) + 2),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) + 2),SCMPDS ) )
set b = DataLoc (s . a),k1;
set IF = if<=0 a,k1,I;
set IsIF = Initialized (stop (if<=0 a,k1,I));
set pI = stop I;
set IsI = Initialized (stop I);
set s2 = s +* (Initialized (stop I));
set s3 = s +* (Initialized (stop (if<=0 a,k1,I)));
set s4 = Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),1;
set i = a,k1 <=0_goto 2;
set j = goto ((card I) + 1);
set SAl = Start-At ((card I) + 2),SCMPDS ;
A1:
if<=0 a,k1,I = (a,k1 <=0_goto 2) ';' ((goto ((card I) + 1)) ';' I)
by SCMPDS_4:52;
A2: Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),(0 + 1) =
Following (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),0 )
by AMI_1:14
.=
Following (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I))))
by AMI_1:13
.=
Exec (a,k1 <=0_goto 2),(s +* (Initialized (stop (if<=0 a,k1,I))))
by A1, Th22
;
A3:
not DataLoc (s . a),k1 in dom (Initialized (stop (if<=0 a,k1,I)))
by SCMPDS_4:31;
not a in dom (Initialized (stop (if<=0 a,k1,I)))
by SCMPDS_4:31;
then A4: (s +* (Initialized (stop (if<=0 a,k1,I)))) . (DataLoc ((s +* (Initialized (stop (if<=0 a,k1,I)))) . a),k1) =
(s +* (Initialized (stop (if<=0 a,k1,I)))) . (DataLoc (s . a),k1)
by FUNCT_4:12
.=
s . (DataLoc (s . a),k1)
by A3, FUNCT_4:12
;
A5:
IC (s +* (Initialized (stop (if<=0 a,k1,I)))) = 0
by FUNCT_4:26, SCMPDS_5:18;
A6:
( Initialized (stop I) c= s +* (Initialized (stop I)) & Shift (stop I),2 c= Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),1 )
by Lm6, FUNCT_4:26;
A7:
DataPart (s +* (Initialized (stop I))) = DataPart (s +* (Initialized (stop (if<=0 a,k1,I))))
by SCMPDS_4:24, SCMPDS_4:36;
now let a be
Int_position ;
(s +* (Initialized (stop I))) . a = (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),1) . athus (s +* (Initialized (stop I))) . a =
(s +* (Initialized (stop (if<=0 a,k1,I)))) . a
by A7, SCMPDS_4:23
.=
(Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),1) . a
by A2, SCMPDS_2:68
;
verum end;
then A8:
DataPart (s +* (Initialized (stop I))) = DataPart (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),1)
by SCMPDS_4:23;
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) + 2),SCMPDS ) )
then A9: IC (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),1) =
ICplusConst (s +* (Initialized (stop (if<=0 a,k1,I)))),2
by A2, A4, SCMPDS_2:68
.=
0 + 2
by A5, Th23
;
A10:
dom (s | NAT ) = NAT
by Th1;
assume A11:
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) + 2),SCMPDS ) )
then A12:
I is_closed_on s +* (Initialized (stop I))
by Th38;
assume A13:
I is_halting_on s
; IExec (if<=0 a,k1,I),s = (IExec I,s) +* (Start-At ((card I) + 2),SCMPDS )
then A14:
ProgramPart (s +* (Initialized (stop I))) halts_on s +* (Initialized (stop I))
by Def3;
T:
ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I)))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),1)
by AMI_1:144;
x:
Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1) = Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),1),(LifeSpan (s +* (Initialized (stop I))))
by AMI_1:51;
A15: CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1))),(Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) =
CurInstr (ProgramPart (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),1),(LifeSpan (s +* (Initialized (stop I)))))),(Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),1),(LifeSpan (s +* (Initialized (stop I)))))
by x, T
.=
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))),(Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))
by A12, A6, A9, A8, Th45
.=
halt SCMPDS
by A14, AMI_1:def 46
;
then A16:
ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I)))) halts_on s +* (Initialized (stop (if<=0 a,k1,I)))
by AMI_1:146;
A17:
CurInstr (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))) = a,k1 <=0_goto 2
by A1, Th22;
now let l be
Element of
NAT ;
( l < (LifeSpan (s +* (Initialized (stop I)))) + 1 implies CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),b1)),(Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),b1) <> halt SCMPDS )assume A18:
l < (LifeSpan (s +* (Initialized (stop I)))) + 1
;
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),b1)),(Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),b1) <> halt SCMPDS u:
Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),
(s +* (Initialized (stop (if<=0 a,k1,I)))),
0 = s +* (Initialized (stop (if<=0 a,k1,I)))
by AMI_1:13;
per cases
( l = 0 or l <> 0 )
;
suppose
l = 0
;
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),b1)),(Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),b1) <> halt SCMPDS then
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),l)),
(Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),l) = CurInstr (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),
(s +* (Initialized (stop (if<=0 a,k1,I))))
by u;
hence
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),l)),
(Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),l) <> halt SCMPDS
by A17, Th30;
verum end; suppose
l <> 0
;
not CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),b1)),(Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),b1) = halt SCMPDS then consider n being
Nat such that A19:
l = n + 1
by NAT_1:6;
reconsider n =
n as
Element of
NAT by ORDINAL1:def 13;
A20:
n < LifeSpan (s +* (Initialized (stop I)))
by A18, A19, XREAL_1:8;
assume A21:
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),l)),
(Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),l) = halt SCMPDS
;
contradictionT:
ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I)))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),1)
by AMI_1:144;
x:
Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),
(s +* (Initialized (stop (if<=0 a,k1,I)))),
(n + 1) = Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),
(Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),1),
n
by AMI_1:51;
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),
(Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n) =
CurInstr (ProgramPart (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),1),n)),
(Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),1),n)
by A12, A6, A9, A8, Th45
.=
halt SCMPDS
by A19, A21, x, T
;
hence
contradiction
by A14, A20, AMI_1:def 46;
verum end; end;
then
for l being Element of NAT st CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),l)),(Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),l) = halt SCMPDS holds
(LifeSpan (s +* (Initialized (stop I)))) + 1 <= l
;
then A22:
LifeSpan (s +* (Initialized (stop (if<=0 a,k1,I)))) = (LifeSpan (s +* (Initialized (stop I)))) + 1
by A15, A16, AMI_1:def 46;
T:
ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I)))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),1)
by AMI_1:144;
A23: DataPart (Result (s +* (Initialized (stop I)))) =
DataPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))
by A14, AMI_1:122
.=
DataPart (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),1),(LifeSpan (s +* (Initialized (stop I)))))
by A12, A6, A9, A8, Th45, T
.=
DataPart (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1))
by AMI_1:51
.=
DataPart (Result (s +* (Initialized (stop (if<=0 a,k1,I)))))
by A16, A22, AMI_1:122
;
A24:
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) + 2),SCMPDS )) . b1 )A25:
IExec I,
s = (Result (s +* (Initialized (stop I)))) +* (s | NAT )
by SCMPDS_4:def 8;
A26:
IExec (if<=0 a,k1,I),
s = (Result (s +* (Initialized (stop (if<=0 a,k1,I))))) +* (s | NAT )
by SCMPDS_4:def 8;
A27:
dom (Start-At ((card I) + 2),SCMPDS ) = {(IC SCMPDS )}
by FUNCOP_1:19;
assume A28:
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) + 2),SCMPDS )) . b1per cases
( x is Int_position or x = IC SCMPDS or x is Element of NAT )
by A28, SCMPDS_4:20;
suppose A29:
x is
Int_position
;
(IExec (if<=0 a,k1,I),s) . b1 = ((IExec I,s) +* (Start-At ((card I) + 2),SCMPDS )) . b1then
x <> IC SCMPDS
by SCMPDS_2:52;
then A30:
not
x in dom (Start-At ((card I) + 2),SCMPDS )
by A27, TARSKI:def 1;
A31:
not
x in dom (s | NAT )
by A10, A29, SCMPDS_2:53;
hence (IExec (if<=0 a,k1,I),s) . x =
(Result (s +* (Initialized (stop (if<=0 a,k1,I))))) . x
by A26, FUNCT_4:12
.=
(Result (s +* (Initialized (stop I)))) . x
by A23, A29, SCMPDS_4:23
.=
(IExec I,s) . x
by A25, A31, FUNCT_4:12
.=
((IExec I,s) +* (Start-At ((card I) + 2),SCMPDS )) . x
by A30, FUNCT_4:12
;
verum end; suppose A32:
x = IC SCMPDS
;
(IExec (if<=0 a,k1,I),s) . b1 = ((IExec I,s) +* (Start-At ((card I) + 2),SCMPDS )) . b1A33:
not
x in dom (s | NAT )
by A10, A32, AMI_1:48;
then A34:
IC (Result (s +* (Initialized (stop I)))) =
IC (IExec I,s)
by A25, A32, FUNCT_4:12
.=
card I
by A11, A13, Th48
;
A35:
x in dom (Start-At ((card I) + 2),SCMPDS )
by A27, A32, TARSKI:def 1;
T:
ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I)))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),1)
by AMI_1:144;
thus (IExec (if<=0 a,k1,I),s) . x =
(Result (s +* (Initialized (stop (if<=0 a,k1,I))))) . x
by A26, A33, FUNCT_4:12
.=
(Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) . x
by A16, A22, AMI_1:122
.=
IC (Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(Comput (ProgramPart (s +* (Initialized (stop (if<=0 a,k1,I))))),(s +* (Initialized (stop (if<=0 a,k1,I)))),1),(LifeSpan (s +* (Initialized (stop I)))))
by A32, AMI_1:51
.=
(IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) + 2
by A12, A6, A9, A8, Th45, T
.=
(IC (Result (s +* (Initialized (stop I))))) + 2
by A14, AMI_1:122
.=
(Start-At ((card I) + 2),SCMPDS ) . (IC SCMPDS )
by A34, FUNCOP_1:87
.=
((IExec I,s) +* (Start-At ((card I) + 2),SCMPDS )) . x
by A32, A35, 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) + 2),SCMPDS ))
by PARTFUN1:def 4
;
hence
IExec (if<=0 a,k1,I),s = (IExec I,s) +* (Start-At ((card I) + 2),SCMPDS )
by A24, FUNCT_1:9; verum