let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA
for I being InitHalting keepInt0_1 Program of SCM+FSA
for J being 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 InitHalting keepInt0_1 Program of SCM+FSA
for J being 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 InitHalting keepInt0_1 Program of SCM+FSA; :: thesis: for J being InitHalting Program of SCM+FSA holds IExec ((I ';' J),p,s) = IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))
let J be 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;
A9: Initialize ((intloc 0) .--> 1) c= Initialized s by FUNCT_4:25;
I c= p +* I by FUNCT_4:25;
then A10: p +* I halts_on Initialized s by Def2, A9;
A11: Initialize ((intloc 0) .--> 1) c= Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))) by FUNCT_4:25;
A14: ( 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;
A17: J c= p +* J by FUNCT_4:25;
A18: ( 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;
A19: ( J c= p +* J & J c= (p +* I) +* J ) by FUNCT_4:25;
A20: Initialize ((intloc 0) .--> 1) c= Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))) by FUNCT_4:25;
A21: Initialize ((intloc 0) .--> 1) c= Initialized s by FUNCT_4:25;
A22: I c= p +* I by FUNCT_4:25;
p +* I halts_on Initialized s by A21, Def2, A22;
then A23: Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))) = Initialized (Result ((p +* I),(Initialized s))) by EXTPRO_1:23;
A24: IC (Result (((p +* I) +* J),(Initialized (Result ((p +* I),(Initialized s)))))) = IC (Result ((p +* J),(Initialized (IExec (I,p,s))))) by A14, Th15, A17, A4;
A25: Initialize ((intloc 0) .--> 1) c= Initialized s by FUNCT_4:25;
A26: I c= (p +* (I ';' J)) +* I by FUNCT_4:25;
A27: LifeSpan (((p +* (I ';' J)) +* I),(Initialized s)) = LifeSpan ((p +* I),(Initialized s)) by A25, Th15, A22, A26;
Reloc (J,(card I)) c= I ';' J by FUNCT_4:25;
then A29: Reloc (J,(card I)) c= p +* (I ';' J) by A2, XBOOLE_1:1;
A34: Initialize ((intloc 0) .--> 1) c= Initialized s by FUNCT_4:25;
A35: ((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) by FUNCT_4:93
.= 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 Def2, A34;
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 A25, A27, Th18, A26
.= DataPart (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))) by A21, A10, Th18, A1, A35 ;
then A37: 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 ;
A38: ( 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, A27, Th25, A6;
then A39: 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 A11, A37, Th12, A4, A29;
A40: 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 A38, A11, A37, Th12, A4, A29;
A41: Initialize ((intloc 0) .--> 1) c= Initialized s by FUNCT_4:25;
I ';' J c= p +* (I ';' J) by FUNCT_4:25;
then A42: p +* (I ';' J) halts_on Initialized s by Def2, A41;
A43: 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 A42, 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 A23, Th28 ;
B43: p +* I halts_on Initialized s by A21, Def2, 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 B43, EXTPRO_1:23 ;
then A44: 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 A18, Th15, A19;
A45: (p +* I) +* J halts_on Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))) by Def2, A3, A4;
A46: 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 A44, A45, EXTPRO_1:23 ;
A48: DataPart (IExec ((I ';' J),p,s)) = DataPart (IExec (J,p,(IExec (I,p,s)))) by A46, A39, A43, EXTPRO_1:4;
F2: (p +* I) +* J halts_on Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))) by A20, Def2, A4;
F1: p +* (I ';' J) halts_on Initialized s by A5, Def2, A2;
p +* I halts_on Initialized s by A21, Def2, A1;
then A49: Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))) = Initialized (Result ((p +* I),(Initialized s))) by EXTPRO_1:23;
A50: 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 F1, 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 A23, Th28
.= (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 A40, EXTPRO_1:4
.= (IC (Result (((p +* I) +* J),(Initialized (Comput ((p +* I),(Initialized s),(LifeSpan ((p +* I),(Initialized s))))))))) + (card I) by F2, EXTPRO_1:23
.= (IC (IExec (J,p,(IExec (I,p,s))))) + (card I) by A24, A49, SCMFSA6B:def 1 ;
hereby :: thesis: verum
reconsider l = (IC (IExec (J,p,(IExec (I,p,s))))) + (card I) as Element of NAT ;
A51: dom (Start-At (l,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
A52: now
let x be set ; :: 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 A53: 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 A53, SCMFSA6A:5;
suppose A54: 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 A55: not x in dom (Start-At (l,SCM+FSA)) by A51, TARSKI:def 1;
(IExec ((I ';' J),p,s)) . x = (IExec (J,p,(IExec (I,p,s)))) . x by A48, A54, SCMFSA6A:7;
hence (IExec ((I ';' J),p,s)) . x = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . x by A55, FUNCT_4:11; :: thesis: verum
end;
suppose A56: 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 A57: not x in dom (Start-At (l,SCM+FSA)) by A51, TARSKI:def 1;
(IExec ((I ';' J),p,s)) . x = (IExec (J,p,(IExec (I,p,s)))) . x by A48, A56, SCMFSA6A:7;
hence (IExec ((I ';' J),p,s)) . x = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . x by A57, FUNCT_4:11; :: thesis: verum
end;
suppose A58: 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 A59: 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 A50, A58, FUNCOP_1:72
.= (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . x by A58, A59, 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 A52, FUNCT_1:2; :: thesis: verum
end;