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 ;
hereby :: thesis: verum
reconsider l = (IC (IExec (J,p,(IExec (I,p,s))))) + (card I) as Element of NAT ;
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
let x be object ; :: thesis: ( 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)) ; :: thesis: (IExec ((I ";" J),p,s)) . b1 = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . b1
per cases ( x is Int-Location or x is FinSeq-Location or x = IC ) by A43, SCMFSA_M:1;
suppose A44: x is Int-Location ; :: thesis: (IExec ((I ";" J),p,s)) . b1 = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . b1
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;
suppose A46: x is FinSeq-Location ; :: thesis: (IExec ((I ";" J),p,s)) . b1 = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . b1
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;
suppose A48: x = IC ; :: thesis: (IExec ((I ";" J),p,s)) . b1 = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . b1
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;
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; :: thesis: verum
end;