let s be State of SCM+FSA; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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 ;

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; :: thesis: 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; :: thesis: 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; :: thesis: 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 :: thesis: verum

reconsider l = (IC (IExec (J,p,(IExec (I,p,s))))) + (card I) as Element of NAT ;

.= 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; :: thesis: verum

end;A42: now :: thesis: 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))) . x

dom (IExec ((I ";" J),p,s)) =
the carrier of SCM+FSA
by PARTFUN1:def 2
(IExec ((I ";" J),p,s)) . x = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . x

let x be object ; :: thesis: ( x in dom (IExec ((I ";" J),p,s)) implies (IExec ((I ";" J),p,s)) . b_{1} = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . b_{1} )

assume A43: x in dom (IExec ((I ";" J),p,s)) ; :: thesis: (IExec ((I ";" J),p,s)) . b_{1} = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . b_{1}

end;assume A43: x in dom (IExec ((I ";" J),p,s)) ; :: thesis: (IExec ((I ";" J),p,s)) . b

per cases
( x is Int-Location or x is FinSeq-Location or x = IC )
by A43, SCMFSA_M:1;

end;

suppose A44:
x is Int-Location
; :: thesis: (IExec ((I ";" J),p,s)) . b_{1} = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . b_{1}

then
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; :: thesis: verum

end;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; :: thesis: verum

suppose A46:
x is FinSeq-Location
; :: thesis: (IExec ((I ";" J),p,s)) . b_{1} = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . b_{1}

then
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; :: thesis: verum

end;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; :: thesis: verum

suppose A48:
x = IC
; :: thesis: (IExec ((I ";" J),p,s)) . b_{1} = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . b_{1}

then
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 ; :: thesis: verum

end;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 ; :: thesis: verum

.= 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; :: thesis: verum