let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for I being really-closed parahalting keeping_0 Program of
for J being really-closed 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; :: thesis: for I being really-closed parahalting keeping_0 Program of
for J being really-closed 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 really-closed parahalting keeping_0 Program of ; :: thesis: for J being really-closed parahalting Program of holds IExec ((I ";" J),P,s) = IncIC ((IExec (J,P,(IExec (I,P,s)))),(card I))
let J be really-closed parahalting Program of ; :: thesis: 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;
A3: I c= (P +* (I ";" J)) +* I by FUNCT_4:25;
A4: I ";" J c= P +* (I ";" J) by FUNCT_4:25;
A5: LifeSpan (((P +* (I ";" J)) +* I),(s +* (Initialize ((intloc 0) .--> 1)))) = LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) by Th8, A1, A3;
A6: Reloc (J,(card I)) c= P +* (I ";" J) by A2, Lm2, A4;
A7: I c= P +* I by FUNCT_4:25;
A8: Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
A9: (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 Th2, A7, A8, EXTPRO_1:23;
A10: ((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 ;
A11: (P +* I) +* (I ";" J) = P +* (I +* (I ";" J)) by FUNCT_4:14
.= P +* ((I ";" J) +* (I ";" J)) by SCMFSA6A:18 ;
A12: (P +* (I ";" J)) +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) by Th1, 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 A10, A12, Th10, A5, FUNCT_4:25
.= DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) by A11, A7, A8, Th10, Th2 ;
then A13: 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 ;
A14: J c= (P +* I) +* J by FUNCT_4:25;
A15: IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I by A2, A5, Lm2, A4;
A16: 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 A13, A2, A5, Lm2, A4;
then A17: 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 Th6, A14, A6, A15;
A18: 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 A15, Th6, A6, A14, A16;
A19: J c= (P +* I) +* J by FUNCT_4:25;
A20: 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;
A21: J c= (P +* I) +* J by FUNCT_4:25;
A22: J c= P +* J by FUNCT_4:25;
A23: 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 Th8, A22, A19, A9;
A24: 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, Th2, 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 A9, Th17 ;
then A25: 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 A17, EXTPRO_1:4
.= DataPart (IExec (J,P,(IExec (I,P,s)))) by A20, A23, Th2, A19, EXTPRO_1:23 ;
A26: 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 A24, A2, Th2, 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 A9, Th17
.= (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 A18, 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 A20, Th2, A19, EXTPRO_1:23
.= (IC (Result (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))))) + (card I) by A8, Th2, A7, EXTPRO_1:23
.= (IC (IExec (J,P,(IExec (I,P,s))))) + (card I) by A21, A22, Th8 ;

hereby :: thesis: verum

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

A28: now :: thesis: for x being object st x in dom (IExec ((I ";" J),P,s)) holds
(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

let x be object ; :: thesis: ( x in dom (IExec ((I ";" J),P,s)) implies (IExec ((I ";" J),P,s)) . b₁ = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . b₁ )
assume A29: x in dom (IExec ((I ";" J),P,s)) ; :: thesis: (IExec ((I ";" J),P,s)) . b₁ = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . b₁

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

suppose A30: x is Int-Location ; :: thesis: (IExec ((I ";" J),P,s)) . b₁ = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . b₁

then x <> IC by SCMFSA_2:56;
then A31: 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 A25, A30, SCMFSA_M:2;
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 A31, FUNCT_4:11; :: thesis: verum

end;

suppose A32: x is FinSeq-Location ; :: thesis: (IExec ((I ";" J),P,s)) . b₁ = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . b₁

then x <> IC by SCMFSA_2:57;
then A33: 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 A25, A32, SCMFSA_M:2;
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 A33, FUNCT_4:11; :: thesis: verum

end;

suppose A34: x = IC ; :: thesis: (IExec ((I ";" J),P,s)) . b₁ = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . b₁

then x in {(IC )} by TARSKI:def 1;
then A35: x in dom (Start-At (l,SCM+FSA)) ;
thus (IExec ((I ";" J),P,s)) . x = (Start-At (l,SCM+FSA)) . (IC ) by A26, A34, 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 A34, A35, FUNCT_4:13 ; :: thesis: verum

end;

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 A28, FUNCT_1:2; :: thesis: verum

end;