let s be State of SCM+FSA; for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds IExec ((I ';' J),P,s) = (IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds IExec ((I ';' J),P,s) = (IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))
set D = Int-Locations \/ FinSeq-Locations;
set A = NAT ;
let I be parahalting keeping_0 Program of SCM+FSA; for J being parahalting Program of SCM+FSA holds IExec ((I ';' J),P,s) = (IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))
let J be parahalting Program of SCM+FSA; IExec ((I ';' J),P,s) = (IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))
set ps = ProgramPart s;
set s1 = s +* (Initialize ((intloc 0) .--> 1));
set P1 = P +* I;
A1:
I c= P +* I
by FUNCT_4:26;
set s2 = s +* (Initialize ((intloc 0) .--> 1));
set P2 = P +* (I ';' J);
set s3 = (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1));
set P3 = (P +* I) +* J;
set m1 = LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))));
set m3 = LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))));
A2:
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:26;
B7:
Initialize ((intloc 0) .--> 1) c= (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:26;
L4:
Start-At (0,SCM+FSA) c= Initialize ((intloc 0) .--> 1)
by FUNCT_4:26;
then A7:
Start-At (0,SCM+FSA) c= (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))
by B7, XBOOLE_1:1;
A10:
dom (ProgramPart s) = NAT
by COMPOS_1:34;
L2:
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:26;
L3:
Start-At (0,SCM+FSA) c= Initialize ((intloc 0) .--> 1)
by FUNCT_4:26;
then A12:
Start-At (0,SCM+FSA) c= s +* (Initialize ((intloc 0) .--> 1))
by L2, XBOOLE_1:1;
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:26;
then A13:
Start-At (0,SCM+FSA) c= s +* (Initialize ((intloc 0) .--> 1))
by L3, XBOOLE_1:1;
A14:
I c= (P +* (I ';' J)) +* I
by FUNCT_4:26;
A15:
I ';' J c= P +* (I ';' J)
by FUNCT_4:26;
( NPP (s +* (Initialize ((intloc 0) .--> 1))) = NPP (s +* (Initialize ((intloc 0) .--> 1))) & NPP (s +* (Initialize ((intloc 0) .--> 1))) = NPP (s +* (Initialize ((intloc 0) .--> 1))) )
;
then A16:
LifeSpan (((P +* (I ';' J)) +* I),(s +* (Initialize ((intloc 0) .--> 1)))) = LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))
by A13, Th29, A1, A14;
A17:
Reloc (J,(card I)) c= P +* (I ';' J)
by A2, Lm5, A15;
A22:
I c= P +* I
by FUNCT_4:26;
B22:
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:26;
then A23:
P +* I halts_on s +* (Initialize ((intloc 0) .--> 1))
by Th19, A22;
A24:
(Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)) = (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))
by Th19, A22, B22, EXTPRO_1:23;
A25:
I c= (P +* (I ';' J)) +* I
by FUNCT_4:26;
A26: ((P +* (I ';' J)) +* I) +* (I ';' J) =
(P +* (I ';' J)) +* (I +* (I ';' J))
by FUNCT_4:15
.=
P +* ((I ';' J) +* (I +* (I ';' J)))
by FUNCT_4:15
.=
P +* ((I ';' J) +* (I ';' J))
by SCMFSA6A:57
;
A28: (P +* I) +* (I ';' J) =
P +* (I +* (I ';' J))
by FUNCT_4:15
.=
P +* ((I ';' J) +* (I ';' J))
by SCMFSA6A:57
;
A29:
Start-At (0,SCM+FSA) c= s +* (Initialize ((intloc 0) .--> 1))
by L2, L3, XBOOLE_1:1;
X2:
NPP (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = NPP (Comput (((P +* I) +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))
by A22, A13, A23, Th36;
(P +* (I ';' J)) +* I halts_on s +* (Initialize ((intloc 0) .--> 1))
by Th18, A12, FUNCT_4:26;
then X1:
NPP (Comput (((P +* (I ';' J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = NPP (Comput ((((P +* (I ';' J)) +* I) +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))
by Th36, A25, A29, A16;
DataPart (Comput (((P +* (I ';' J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) =
DataPart (Comput ((P +* ((I ';' J) +* (I ';' J))),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))
by A26, X1, COMPOS_1:138
.=
DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))
by A28, X2, COMPOS_1:138
;
then A30: DataPart ((Comput (((P +* (I ';' J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) =
(DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) +* (DataPart (Initialize ((intloc 0) .--> 1)))
by FUNCT_4:75
.=
DataPart ((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))
by FUNCT_4:75
;
A31:
J c= (P +* I) +* J
by FUNCT_4:26;
A32:
IC (Comput ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I
by A2, A16, Lm5, A15;
B32:
DataPart (Comput ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = DataPart ((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))
by A30, A2, A16, Lm5, A15;
then A33:
DataPart (Comput ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))))
by A7, Th27, A31, A17, A32;
A34:
IC (Comput ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) = (IC (Comput (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))))) + (card I)
by A32, A7, Th27, A17, A31, B32;
( Initialize ((intloc 0) .--> 1) c= (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)) & Initialize ((intloc 0) .--> 1) c= (IExec (I,P,s)) +* (Initialize ((intloc 0) .--> 1)) )
by FUNCT_4:26;
then A35:
( Start-At (0,SCM+FSA) c= (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)) & Start-At (0,SCM+FSA) c= (IExec (I,P,s)) +* (Initialize ((intloc 0) .--> 1)) )
by L4, XBOOLE_1:1;
Initialize ((intloc 0) .--> 1) c= (IExec (I,P,s)) +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:26;
then A36:
Start-At (0,SCM+FSA) c= (IExec (I,P,s)) +* (Initialize ((intloc 0) .--> 1))
by L4, XBOOLE_1:1;
A37:
J c= (P +* I) +* J
by FUNCT_4:26;
B38:
Initialize ((intloc 0) .--> 1) c= (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:26;
A39:
J c= (P +* I) +* J
by FUNCT_4:26;
A40:
J c= P +* J
by FUNCT_4:26;
dom (s | NAT) misses dom (Initialize ((intloc 0) .--> 1))
by RELAT_1:87, SCMFSA6A:87, XBOOLE_1:63;
then iii:
((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT)) +* (Initialize ((intloc 0) .--> 1)) = ((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))) +* (s | NAT)
by FUNCT_4:126;
then
NPP ((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))) = NPP (((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT)) +* (Initialize ((intloc 0) .--> 1)))
by COMPOS_1:236;
then
NPP (Result (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))))) = NPP (Result ((P +* J),((IExec (I,P,s)) +* (Initialize ((intloc 0) .--> 1)))))
by A39, A40, Th29, A35;
then A41:
IC (Result (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))))) = IC (Result ((P +* J),((IExec (I,P,s)) +* (Initialize ((intloc 0) .--> 1)))))
by COMPOS_1:230;
A42:
(IExec (I,P,s)) | NAT = ProgramPart s
by PBOOLE:157;
C7:
Start-At (0,SCM+FSA) c= (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))
by L4, B7, XBOOLE_1:1;
NPP ((IExec (I,P,s)) +* (Initialize ((intloc 0) .--> 1))) = NPP ((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))
by A24, iii, COMPOS_1:236;
then
NPP (Result ((P +* J),((IExec (I,P,s)) +* (Initialize ((intloc 0) .--> 1))))) = NPP (Result (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))
by A36, Th29, A40, A37, C7;
then xx:
(Result ((P +* J),((IExec (I,P,s)) +* (Initialize ((intloc 0) .--> 1))))) +* (ProgramPart s) = (Result (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))) +* (ProgramPart s)
by A10, COMPOS_1:238;
A43:
IExec (J,P,(IExec (I,P,s))) = (Comput (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) +* (ProgramPart s)
by B38, xx, A42, Th19, A37, EXTPRO_1:23;
B45:
I ';' J c= P +* (I ';' J)
by FUNCT_4:26;
then IExec ((I ';' J),P,s) =
(Comput ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (ProgramPart s)
by A2, Th19, EXTPRO_1:23
.=
(Comput ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))))) +* (ProgramPart s)
by A24, Th43
;
then A46: DataPart (IExec ((I ';' J),P,s)) =
DataPart (Comput ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))))
by COMPOS_1:82
.=
DataPart (Comput (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))))
by A33, EXTPRO_1:5
.=
DataPart (IExec (J,P,(IExec (I,P,s))))
by A43, COMPOS_1:82
;
A47: IC (IExec ((I ';' J),P,s)) =
IC (Result ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1)))))
by Th30
.=
IC (Comput ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1)))))))
by B45, A2, Th19, EXTPRO_1:23
.=
IC (Comput ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))))
by A24, Th43
.=
(IC (Comput (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))))) + (card I)
by A34, EXTPRO_1:5
.=
(IC (Result (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))) + (card I)
by B38, Th19, A37, EXTPRO_1:23
.=
(IC (Result (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))))) + (card I)
by A23, EXTPRO_1:23
.=
(IC (IExec (J,P,(IExec (I,P,s))))) + (card I)
by A41, Th30
;
hereby verum
reconsider l =
(IC (IExec (J,P,(IExec (I,P,s))))) + (card I) as
Element of
NAT ;
A48:
dom (Start-At (l,SCM+FSA)) = {(IC )}
by FUNCOP_1:19;
A49:
now let x be
set ;
( x in dom (IExec ((I ';' J),P,s)) implies (IExec ((I ';' J),P,s)) . b1 = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . b1 )assume A50:
x in dom (IExec ((I ';' J),P,s))
;
(IExec ((I ';' J),P,s)) . b1 = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . b1per cases
( x is Int-Location or x is FinSeq-Location or x = IC or x is Element of NAT )
by A50, SCMFSA6A:35;
suppose A51:
x is
Int-Location
;
(IExec ((I ';' J),P,s)) . b1 = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . b1then
x <> IC
by SCMFSA_2:81;
then A52:
not
x in dom (Start-At (l,SCM+FSA))
by A48, TARSKI:def 1;
(IExec ((I ';' J),P,s)) . x = (IExec (J,P,(IExec (I,P,s)))) . x
by A46, A51, SCMFSA6A:38;
hence
(IExec ((I ';' J),P,s)) . x = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . x
by A52, FUNCT_4:12;
verum end; suppose A53:
x is
FinSeq-Location
;
(IExec ((I ';' J),P,s)) . b1 = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . b1then
x <> IC
by SCMFSA_2:82;
then A54:
not
x in dom (Start-At (l,SCM+FSA))
by A48, TARSKI:def 1;
(IExec ((I ';' J),P,s)) . x = (IExec (J,P,(IExec (I,P,s)))) . x
by A46, A53, SCMFSA6A:38;
hence
(IExec ((I ';' J),P,s)) . x = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . x
by A54, FUNCT_4:12;
verum end; suppose A55:
x = IC
;
(IExec ((I ';' J),P,s)) . b1 = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . b1then
x in {(IC )}
by TARSKI:def 1;
then A56:
x in dom (Start-At (l,SCM+FSA))
by FUNCOP_1:19;
thus (IExec ((I ';' J),P,s)) . x =
(Start-At (l,SCM+FSA)) . (IC )
by A47, A55, FUNCOP_1:87
.=
((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . x
by A55, A56, FUNCT_4:14
;
verum end; suppose A57:
x is
Element of
NAT
;
(IExec ((I ';' J),P,s)) . b1 = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . b1then
x <> IC
by COMPOS_1:3;
then A58:
not
x in dom (Start-At (l,SCM+FSA))
by A48, TARSKI:def 1;
(IExec ((I ';' J),P,s)) | NAT =
s | NAT
by PBOOLE:157
.=
(IExec (J,P,(IExec (I,P,s)))) | NAT
by A42, PBOOLE:157
;
then
(IExec ((I ';' J),P,s)) . x = (IExec (J,P,(IExec (I,P,s)))) . x
by A57, COMPOS_1:127;
hence
(IExec ((I ';' J),P,s)) . x = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . x
by A58, FUNCT_4:12;
verum end; end; dom (IExec ((I ';' J),P,s)) =
the
carrier of
SCM+FSA
by PARTFUN1:def 4
.=
dom ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA)))
by PARTFUN1:def 4
;
hence
IExec (
(I ';' J),
P,
s)
= (IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))
by A49, FUNCT_1:9;
verum
end;