let s be State of SCM+FSA; for P being Instruction-Sequence of SCM+FSA
for I being parahalting keeping_0 Program of
for J being parahalting Program of holds IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(IExec (I,P,s)))),(card I))
let P be Instruction-Sequence of SCM+FSA; for I being parahalting keeping_0 Program of
for J being parahalting Program of holds IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(IExec (I,P,s)))),(card I))
set D = Int-Locations \/ FinSeq-Locations;
set A = NAT ;
let I be parahalting keeping_0 Program of ; for J being parahalting Program of holds IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(IExec (I,P,s)))),(card I))
let J be parahalting Program of ; IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(IExec (I,P,s)))),(card I))
set s1 = s +* (Initialize ((intloc 0) .--> 1));
set P1 = P +* I;
A1:
I c= P +* I
by FUNCT_4:25;
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:25;
A14:
I c= (P +* (I ';' J)) +* I
by FUNCT_4:25;
A15:
I ';' J c= P +* (I ';' J)
by FUNCT_4:25;
A16:
LifeSpan (((P +* (I ';' J)) +* I),(s +* (Initialize ((intloc 0) .--> 1)))) = LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))
by Th29, A1, A14;
A17:
Reloc (J,(card I)) c= P +* (I ';' J)
by A2, Lm5, A15;
A22:
I c= P +* I
by FUNCT_4:25;
B22:
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:25;
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;
A26: ((P +* (I ';' J)) +* I) +* (I ';' J) =
(P +* (I ';' J)) +* (I +* (I ';' J))
by FUNCT_4:14
.=
P +* ((I ';' J) +* (I +* (I ';' J)))
by FUNCT_4:14
.=
P +* ((I ';' J) +* (I ';' J))
by SCMFSA6A:18
;
A28: (P +* I) +* (I ';' J) =
P +* (I +* (I ';' J))
by FUNCT_4:14
.=
P +* ((I ';' J) +* (I ';' J))
by SCMFSA6A:18
;
Y1:
(P +* (I ';' J)) +* I halts_on s +* (Initialize ((intloc 0) .--> 1))
by Th18, FUNCT_4:25;
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, Y1, Th36, A16, FUNCT_4:25
.=
DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))
by A28, A22, B22, Th36, Th19
;
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:71
.=
DataPart ((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))
by FUNCT_4:71
;
A31:
J c= (P +* I) +* J
by FUNCT_4:25;
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 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, Th27, A17, A31, B32;
A37:
J c= (P +* I) +* J
by FUNCT_4:25;
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:25;
A39:
J c= (P +* I) +* J
by FUNCT_4:25;
A40:
J c= P +* J
by FUNCT_4:25;
xx:
Result ((P +* J),((IExec (I,P,s)) +* (Initialize ((intloc 0) .--> 1)))) = 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 Th29, A40, A37, A24;
B45:
I ';' J c= P +* (I ';' J)
by FUNCT_4:25;
then IExec ((I ';' J),P,s) =
Comput ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))))))
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)))))))
by A24, Th43
;
then A46: DataPart (IExec ((I ';' J),P,s)) =
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:4
.=
DataPart (IExec (J,P,(IExec (I,P,s))))
by B38, xx, Th19, A37, EXTPRO_1:23
;
A47: IC (IExec ((I ';' J),P,s)) =
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:4
.=
(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 B22, Th19, A22, EXTPRO_1:23
.=
(IC (IExec (J,P,(IExec (I,P,s))))) + (card I)
by A39, A40, Th29
;
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:13;
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 )
by A50, SCMFSA6A:5;
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:56;
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:7;
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:11;
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:57;
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:7;
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:11;
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:13;
thus (IExec ((I ';' J),P,s)) . x =
(Start-At (l,SCM+FSA)) . (IC )
by A47, A55, FUNCOP_1:72
.=
((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:13
;
verum end; end; dom (IExec ((I ';' J),P,s)) =
the
carrier of
SCM+FSA
by PARTFUN1:def 2
.=
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 2
;
hence
IExec (
(I ';' J),
P,
s)
= IncIC (
(IExec (J,P,(IExec (I,P,s)))),
(card I))
by A49, FUNCT_1:2;
verum
end;