let s be State of SCM+FSA; for p being Instruction-Sequence of SCM+FSA
for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA
for J being really-closed InitHalting Program of SCM+FSA 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 really-closed InitHalting keepInt0_1 Program of SCM+FSA
for J being really-closed InitHalting Program of SCM+FSA holds IExec ((I ";" J),p,s) = IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))
set D = Data-Locations ;
set A = NAT ;
let I be really-closed InitHalting keepInt0_1 Program of SCM+FSA; for J being really-closed InitHalting Program of SCM+FSA holds IExec ((I ";" J),p,s) = IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))
let J be really-closed InitHalting Program of SCM+FSA; IExec ((I ";" J),p,s) = IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))
set s1 = Initialized s;
set p1 = p +* I;
A1:
I c= p +* I
by FUNCT_4:25;
set p2 = p +* (I ";" J);
A2:
I ";" J c= p +* (I ";" J)
by FUNCT_4:25;
set s3 = Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s)))));
set p3 = (p +* I) +* J;
A3:
Initialize ((intloc 0) .--> 1) c= Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s)))))
by FUNCT_4:25;
A4:
J c= (p +* I) +* J
by FUNCT_4:25;
set m1 = LifeSpan ((p +* I),(Initialized s));
set m3 = LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s)))))));
A5:
Initialize ((intloc 0) .--> 1) c= Initialized s
by FUNCT_4:25;
A6:
I ";" J c= p +* (I ";" J)
by FUNCT_4:25;
A7:
Initialize ((intloc 0) .--> 1) c= Initialized s
by FUNCT_4:25;
I c= p +* I
by FUNCT_4:25;
then A8:
p +* I halts_on Initialized s
by Def1, A7;
A9:
Initialize ((intloc 0) .--> 1) c= Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s)))))
by FUNCT_4:25;
A10:
( IExec (I,p,s) = Result ((p +* I),(Initialized s)) & Initialize ((intloc 0) .--> 1) c= (Result ((p +* I),(Initialized s))) +* (Initialize ((intloc 0) .--> 1)) )
by FUNCT_4:25, SCMFSA6B:def 1;
A11:
J c= p +* J
by FUNCT_4:25;
A12:
( Initialize ((intloc 0) .--> 1) c= Initialized (IExec (I,p,s)) & Initialize ((intloc 0) .--> 1) c= Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))) )
by FUNCT_4:25;
A13:
( J c= p +* J & J c= (p +* I) +* J )
by FUNCT_4:25;
A14:
Initialize ((intloc 0) .--> 1) c= Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s)))))
by FUNCT_4:25;
A15:
Initialize ((intloc 0) .--> 1) c= Initialized s
by FUNCT_4:25;
A16:
I c= p +* I
by FUNCT_4:25;
p +* I halts_on Initialized s
by A15, Def1, A16;
then A17:
Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))) = Initialized (Result ((p +* I),(Initialized s)))
by EXTPRO_1:23;
A18:
IC (Result (((p +* I) +* J),(Initialized (Result ((p +* I),(Initialized s)))))) = IC (Result ((p +* J),(Initialized (IExec (I,p,s)))))
by A10, Th6, A11, A4;
A19:
Initialize ((intloc 0) .--> 1) c= Initialized s
by FUNCT_4:25;
A20:
I c= (p +* (I ";" J)) +* I
by FUNCT_4:25;
A21:
LifeSpan (((p +* (I ";" J)) +* I),(Initialized s)) = LifeSpan ((p +* I),(Initialized s))
by A19, Th6, A16, A20;
Reloc (J,(card I)) c= I ";" J
by SCMFSA6A:38;
then A22:
Reloc (J,(card I)) c= p +* (I ";" J)
by A2, XBOOLE_1:1;
A23:
Initialize ((intloc 0) .--> 1) c= Initialized s
by FUNCT_4:25;
A24: ((p +* (I ";" J)) +* I) +* (I ";" J) =
(p +* (I ";" J)) +* (I +* (I ";" J))
by FUNCT_4:14
.=
(p +* (I ";" J)) +* (I ";" J)
by SCMFSA6A:18
.=
p +* (I ";" J)
.=
p +* (I +* (I ";" J))
by SCMFSA6A:18
.=
(p +* I) +* (I ";" J)
by FUNCT_4:14
;
I c= (p +* (I ";" J)) +* I
by FUNCT_4:25;
then
(p +* (I ";" J)) +* I halts_on Initialized s
by Def1, A23;
then DataPart (Comput (((p +* (I ";" J)) +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))) =
DataPart (Comput ((((p +* (I ";" J)) +* I) +* (I ";" J)),(Initialized s),(LifeSpan ((p +* I),(Initialized s)))))
by A19, A21, Th8, A20
.=
DataPart (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s)))))
by A15, A8, Th8, A1, A24
;
then A25: DataPart ((Comput (((p +* (I ";" J)) +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))) +* (Initialize ((intloc 0) .--> 1))) =
(DataPart (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s)))))) +* (DataPart (Initialize ((intloc 0) .--> 1)))
by FUNCT_4:71
.=
DataPart ((Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))) +* (Initialize ((intloc 0) .--> 1)))
by FUNCT_4:71
;
A26:
( IC (Comput ((p +* (I ";" J)),(Initialized s),((LifeSpan ((p +* I),(Initialized s))) + 1))) = card I & DataPart (Comput ((p +* (I ";" J)),(Initialized s),((LifeSpan ((p +* I),(Initialized s))) + 1))) = DataPart ((Comput (((p +* (I ";" J)) +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))) +* (Initialize ((intloc 0) .--> 1))) )
by A5, A21, Th13, A6;
then A27:
DataPart (Comput ((p +* (I ";" J)),(Comput ((p +* (I ";" J)),(Initialized s),((LifeSpan ((p +* I),(Initialized s))) + 1))),(LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s)))))))))) = DataPart (Comput (((p +* I) +* J),(Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s)))))),(LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))))))))
by A9, A25, Th4, A4, A22;
A28:
IC (Comput ((p +* (I ";" J)),(Comput ((p +* (I ";" J)),(Initialized s),((LifeSpan ((p +* I),(Initialized s))) + 1))),(LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s)))))))))) = (IC (Comput (((p +* I) +* J),(Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s)))))),(LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))))))))) + (card I)
by A26, A9, A25, Th4, A4, A22;
A29:
Initialize ((intloc 0) .--> 1) c= Initialized s
by FUNCT_4:25;
I ";" J c= p +* (I ";" J)
by FUNCT_4:25;
then A30:
p +* (I ";" J) halts_on Initialized s
by Def1, A29;
A31: IExec ((I ";" J),p,s) =
Result ((p +* (I ";" J)),(Initialized s))
by SCMFSA6B:def 1
.=
Comput ((p +* (I ";" J)),(Initialized s),(LifeSpan ((p +* (I ";" J)),(Initialized s))))
by A30, EXTPRO_1:23
.=
Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(Initialized s))) + 1) + (LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))))))))
by A17, Th16
;
A32:
p +* I halts_on Initialized s
by A15, Def1, A1;
IExec (I,p,s) =
Result ((p +* I),(Initialized s))
by SCMFSA6B:def 1
.=
Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))
by A32, EXTPRO_1:23
;
then A33:
Result ((p +* J),((IExec (I,p,s)) +* (Initialize ((intloc 0) .--> 1)))) = Result (((p +* I) +* J),(Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s)))))))
by A12, Th6, A13;
A34:
(p +* I) +* J halts_on Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s)))))
by Def1, A3, A4;
A35: IExec (J,p,(IExec (I,p,s))) =
Result ((p +* J),(Initialized (IExec (I,p,s))))
by SCMFSA6B:def 1
.=
Comput (((p +* I) +* J),(Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s)))))),(LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s)))))))))
by A33, A34, EXTPRO_1:23
;
A36:
DataPart (IExec ((I ";" J),p,s)) = DataPart (IExec (J,p,(IExec (I,p,s))))
by A35, A27, A31, EXTPRO_1:4;
A37:
(p +* I) +* J halts_on Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s)))))
by A14, Def1, A4;
A38:
p +* (I ";" J) halts_on Initialized s
by A5, Def1, A2;
p +* I halts_on Initialized s
by A15, Def1, A1;
then A39:
Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))) = Initialized (Result ((p +* I),(Initialized s)))
by EXTPRO_1:23;
A40: IC (IExec ((I ";" J),p,s)) =
IC (Result ((p +* (I ";" J)),(Initialized s)))
by SCMFSA6B:def 1
.=
IC (Comput ((p +* (I ";" J)),(Initialized s),(LifeSpan ((p +* (I ";" J)),(Initialized s)))))
by A38, EXTPRO_1:23
.=
IC (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(Initialized s))) + 1) + (LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s)))))))))))
by A17, Th16
.=
(IC (Comput (((p +* I) +* J),(Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s)))))),(LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))))))))) + (card I)
by A28, EXTPRO_1:4
.=
(IC (Result (((p +* I) +* J),(Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))))))) + (card I)
by A37, EXTPRO_1:23
.=
(IC (IExec (J,p,(IExec (I,p,s))))) + (card I)
by A18, A39, SCMFSA6B:def 1
;
hereby verum
reconsider l =
(IC (IExec (J,p,(IExec (I,p,s))))) + (card I) as
Element of
NAT ;
A42:
now for x being object st x in dom (IExec ((I ";" J),p,s)) holds
(IExec ((I ";" J),p,s)) . x = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . xlet x be
object ;
( x in dom (IExec ((I ";" J),p,s)) implies (IExec ((I ";" J),p,s)) . b1 = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . b1 )assume A43:
x in dom (IExec ((I ";" J),p,s))
;
(IExec ((I ";" J),p,s)) . b1 = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . b1per cases
( x is Int-Location or x is FinSeq-Location or x = IC )
by A43, SCMFSA_M:1;
suppose A44:
x is
Int-Location
;
(IExec ((I ";" J),p,s)) . b1 = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . b1then
x <> IC
by SCMFSA_2:56;
then A45:
not
x in dom (Start-At (l,SCM+FSA))
by TARSKI:def 1;
(IExec ((I ";" J),p,s)) . x = (IExec (J,p,(IExec (I,p,s)))) . x
by A36, A44, SCMFSA_M:2;
hence
(IExec ((I ";" J),p,s)) . x = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . x
by A45, FUNCT_4:11;
verum end; suppose A46:
x is
FinSeq-Location
;
(IExec ((I ";" J),p,s)) . b1 = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . b1then
x <> IC
by SCMFSA_2:57;
then A47:
not
x in dom (Start-At (l,SCM+FSA))
by TARSKI:def 1;
(IExec ((I ";" J),p,s)) . x = (IExec (J,p,(IExec (I,p,s)))) . x
by A36, A46, SCMFSA_M:2;
hence
(IExec ((I ";" J),p,s)) . x = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . x
by A47, FUNCT_4:11;
verum end; suppose A48:
x = IC
;
(IExec ((I ";" J),p,s)) . b1 = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . b1then
x in {(IC )}
by TARSKI:def 1;
then A49:
x in dom (Start-At (l,SCM+FSA))
;
thus (IExec ((I ";" J),p,s)) . x =
(Start-At (l,SCM+FSA)) . (IC )
by A40, A48, FUNCOP_1:72
.=
(IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . x
by A48, A49, FUNCT_4:13
;
verum end; end; end; dom (IExec ((I ";" J),p,s)) =
the
carrier of
SCM+FSA
by PARTFUN1:def 2
.=
dom (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I)))
by PARTFUN1:def 2
;
hence
IExec (
(I ";" J),
p,
s)
= IncIC (
(IExec (J,p,(IExec (I,p,s)))),
(card I))
by A42, FUNCT_1:2;
verum
end;