let s be State of SCM+FSA; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds IExec ((I ';' J),P,s) = (IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds IExec ((I ';' J),P,s) = (IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))
set D = Int-Locations \/ FinSeq-Locations;
set A = NAT ;
let I be parahalting keeping_0 Program of SCM+FSA; :: thesis: for J being parahalting Program of SCM+FSA holds IExec ((I ';' J),P,s) = (IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))
let J be parahalting Program of SCM+FSA; :: thesis: IExec ((I ';' J),P,s) = (IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))
set ps = ProgramPart s;
set s1 = s +* (Initialized I);
set P1 = P +* I;
A1: I c= P +* I by FUNCT_4:26;
set s2 = s +* (Initialized (I ';' J));
set P2 = P +* (I ';' J);
set s3 = (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J);
set P3 = (P +* I) +* J;
set m1 = LifeSpan ((P +* I),(s +* (Initialized I)));
set m3 = LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J)));
A2: Initialized (I ';' J) c= s +* (Initialized (I ';' J)) by FUNCT_4:26;
Initialize I c= (s +* (Initialized (I ';' J))) +* (Initialize I) by FUNCT_4:26;
then Initialize I c= Initialize ((s +* (Initialized (I ';' J))) +* I) by FUNCT_4:15;
then A3: Initialize I c= (Initialize (s +* (Initialized (I ';' J)))) +* I by COMPOS_1:83;
A4: (s +* (Initialized I)) +* (I ';' J) = s +* ((Initialized I) +* (I ';' J)) by FUNCT_4:15
.= s +* (Initialized (I ';' J)) by SCMFSA6A:58 ;
A5: I c= P +* I by FUNCT_4:26;
Initialized I c= s +* (Initialized I) by FUNCT_4:26;
then A6: P +* I halts_on s +* (Initialized I) by Th19, A5;
A7: Initialize J c= (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J) by Th8, FUNCT_4:26;
A8: (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (ProgramPart s)) +* (Initialized J) equal_outside dom (ProgramPart s) by FUNCT_7:31, FUNCT_7:106;
then A9: ((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (ProgramPart s)) +* (Initialized J),(Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J) equal_outside dom (ProgramPart s) by FUNCT_7:28;
A10: dom (ProgramPart s) = NAT by COMPOS_1:34;
then A11: dom (ProgramPart s) misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
Initialized I c= (s +* (Initialized (I ';' J))) +* I by FUNCT_4:26, SCMFSA6A:52;
then A12: Initialize I c= (s +* (Initialized (I ';' J))) +* I by Th8;
A13: Initialize I c= s +* (Initialized I) by Th8, FUNCT_4:26;
A14: I c= (P +* (I ';' J)) +* I by FUNCT_4:26;
A15: I ';' J c= P +* (I ';' J) by FUNCT_4:26;
( s +* (Initialized I),s +* (Initialized (I ';' J)) equal_outside NAT & s +* (Initialized (I ';' J)),(s +* (Initialized (I ';' J))) +* I equal_outside NAT ) by FUNCT_7:132, SCMFSA6A:53;
then s +* (Initialized I),(s +* (Initialized (I ';' J))) +* I equal_outside NAT by FUNCT_7:29;
then A16: LifeSpan (((P +* (I ';' J)) +* I),((s +* (Initialized (I ';' J))) +* I)) = LifeSpan ((P +* I),(s +* (Initialized I))) by A13, A12, Th29, A1, A14;
A17: Reloc (J,(card I)) c= P +* (I ';' J) by A2, Lm5, A15;
A18: I +* (I ';' J) = I ';' J by SCMFSA6A:57;
A19: ((s +* (Initialized (I ';' J))) +* I) +* (I ';' J) = (s +* (Initialized (I ';' J))) +* (I +* (I ';' J)) by FUNCT_4:15;
A20: (s +* (Initialized (I ';' J))) +* (I ';' J) = s +* ((Initialized (I ';' J)) +* (I ';' J)) by FUNCT_4:15;
I ';' J c= Initialized (I ';' J) by SCMFSA6A:26;
then A21: (Initialized (I ';' J)) +* (I ';' J) = Initialized (I ';' J) by LATTICE2:8;
A22: I c= P +* I by FUNCT_4:26;
Initialized I c= s +* (Initialized I) by FUNCT_4:26;
then A23: P +* I halts_on s +* (Initialized I) by Th19, A22;
then A24: (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J) = (Result ((P +* I),(s +* (Initialized I)))) +* (Initialized J) by EXTPRO_1:23;
A25: I c= (P +* (I ';' J)) +* I by FUNCT_4:26;
A26: ((P +* (I ';' J)) +* I) +* (I ';' J) = (P +* (I ';' J)) +* (I +* (I ';' J)) by FUNCT_4:15
.= P +* ((I ';' J) +* (I +* (I ';' J))) by FUNCT_4:15
.= P +* ((I ';' J) +* (I ';' J)) by SCMFSA6A:57 ;
A27: I c= P +* I by FUNCT_4:26;
A28: (P +* I) +* (I ';' J) = P +* (I +* (I ';' J)) by FUNCT_4:15
.= P +* ((I ';' J) +* (I ';' J)) by SCMFSA6A:57 ;
Initialized (I ';' J) = Initialize ((I ';' J) +* ((intloc 0) .--> 1)) by FUNCT_4:15;
then ( Start-At (0,SCM+FSA) c= Initialized (I ';' J) & Initialized (I ';' J) c= s +* (Initialized (I ';' J)) ) by FUNCT_4:26;
then Start-At (0,SCM+FSA) c= s +* (Initialized (I ';' J)) by XBOOLE_1:1;
then A29: Initialize I c= (s +* (Initialized (I ';' J))) +* I by A3, FUNCT_4:79;
(P +* (I ';' J)) +* I halts_on (s +* (Initialized (I ';' J))) +* I by Th18, A29, FUNCT_4:26;
then DataPart (Comput (((P +* (I ';' J)) +* I),((s +* (Initialized (I ';' J))) +* I),(LifeSpan ((P +* I),(s +* (Initialized I)))))) = DataPart (Comput ((P +* ((I ';' J) +* (I ';' J))),(s +* ((Initialized (I ';' J)) +* (I ';' J))),(LifeSpan ((P +* I),(s +* (Initialized I)))))) by A18, A20, A19, COMPOS_1:138, A26, Th36, A25, A29, A16
.= DataPart (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) by A6, A13, A4, Th36, COMPOS_1:138, A21, A27, A28 ;
then A30: DataPart ((Comput (((P +* (I ';' J)) +* I),((s +* (Initialized (I ';' J))) +* I),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J)) = (DataPart (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I))))))) +* (DataPart (Initialized J)) by FUNCT_4:75
.= DataPart ((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J)) by FUNCT_4:75 ;
A31: J c= (P +* I) +* J by FUNCT_4:26;
A32: ( IC (Comput ((P +* (I ';' J)),(s +* (Initialized (I ';' J))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1))) = card I & DataPart (Comput ((P +* (I ';' J)),(s +* (Initialized (I ';' J))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1))) = DataPart ((Comput (((P +* (I ';' J)) +* I),((s +* (Initialized (I ';' J))) +* I),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J)) ) by A2, A16, Lm5, A15;
then A33: DataPart (Comput ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(s +* (Initialized (I ';' J))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J)))))) = DataPart (Comput (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J)),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J)))))) by A7, A30, Th27, A31, A17;
A34: IC (Comput ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(s +* (Initialized (I ';' J))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J)))))) = (IC (Comput (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J)),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J))))))) + (card I) by A32, A7, A30, Th27, A17, A31;
A35: ( Initialize J c= (Result ((P +* I),(s +* (Initialized I)))) +* (Initialized J) & Initialize J c= (IExec (I,P,s)) +* (Initialized J) ) by Th8, FUNCT_4:26;
A36: ( Initialize J c= (IExec (I,P,s)) +* (Initialized J) & Initialize J c= (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J) ) by Th8, FUNCT_4:26;
A37: J c= (P +* I) +* J by FUNCT_4:26;
Initialized J c= (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J) by FUNCT_4:26;
then A38: (P +* I) +* J halts_on (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J) by Th19, A37;
A39: J c= (P +* I) +* J by FUNCT_4:26;
A40: J c= P +* J by FUNCT_4:26;
Result ((P +* I),(s +* (Initialized I))) = Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I))))) by A23, EXTPRO_1:23;
then A41: IC (Result (((P +* I) +* J),((Result ((P +* I),(s +* (Initialized I)))) +* (Initialized J)))) = IC (Result ((P +* J),((IExec (I,P,s)) +* (Initialized J)))) by A10, A8, A35, Th29, COMPOS_1:24, A39, A40;
A42: (IExec (I,P,s)) | NAT = ProgramPart s by PBOOLE:157;
IExec (I,P,s) = (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (ProgramPart s) by A23, EXTPRO_1:23;
then Result ((P +* J),((IExec (I,P,s)) +* (Initialized J))), Result (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J))) equal_outside NAT by A10, A9, A36, Th29, A40, A37;
then (Result ((P +* J),((IExec (I,P,s)) +* (Initialized J)))) +* (ProgramPart s) = (Result (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J)))) +* (ProgramPart s) by A10, FUNCT_7:108;
then A43: IExec (J,P,(IExec (I,P,s))) = (Comput (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J)),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J)))))) +* (ProgramPart s) by A42, A38, EXTPRO_1:23;
A44: Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I))))) = Result ((P +* I),(s +* (Initialized I))) by A23, EXTPRO_1:23;
I ';' J c= P +* (I ';' J) by FUNCT_4:26;
then A45: P +* (I ';' J) halts_on s +* (Initialized (I ';' J)) by A2, Th19;
then IExec ((I ';' J),P,s) = (Comput ((P +* (I ';' J)),(s +* (Initialized (I ';' J))),(LifeSpan ((P +* (I ';' J)),(s +* (Initialized (I ';' J))))))) +* (ProgramPart s) by EXTPRO_1:23
.= (Comput ((P +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1) + (LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J))))))) +* (ProgramPart s) by A24, Th43 ;
then A46: DataPart (IExec ((I ';' J),P,s)) = DataPart (Comput ((P +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1) + (LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J))))))) by A11, FUNCT_4:76, SCMFSA_2:127
.= DataPart (Comput (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J)),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J)))))) by A33, EXTPRO_1:5
.= DataPart (IExec (J,P,(IExec (I,P,s)))) by A43, A11, FUNCT_4:76, SCMFSA_2:127 ;
A47: IC (IExec ((I ';' J),P,s)) = IC (Result ((P +* (I ';' J)),(s +* (Initialized (I ';' J))))) by Th30
.= IC (Comput ((P +* (I ';' J)),(s +* (Initialized (I ';' J))),(LifeSpan ((P +* (I ';' J)),(s +* (Initialized (I ';' J))))))) by A45, EXTPRO_1:23
.= IC (Comput ((P +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1) + (LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J))))))) by A24, Th43
.= (IC (Comput (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J)),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J))))))) + (card I) by A34, EXTPRO_1:5
.= (IC (Result (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized J))))) + (card I) by A38, EXTPRO_1:23
.= (IC (Result (((P +* I) +* J),((Result ((P +* I),(s +* (Initialized I)))) +* (Initialized J))))) + (card I) by A44
.= (IC (IExec (J,P,(IExec (I,P,s))))) + (card I) by A41, Th30 ;
hereby :: thesis: verum
reconsider l = (IC (IExec (J,P,(IExec (I,P,s))))) + (card I) as Element of NAT ;
A48: dom (Start-At (l,SCM+FSA)) = {(IC )} by FUNCOP_1:19;
A49: now
let x be set ; :: thesis: ( x in dom (IExec ((I ';' J),P,s)) implies (IExec ((I ';' J),P,s)) . b1 = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . b1 )
assume A50: x in dom (IExec ((I ';' J),P,s)) ; :: thesis: (IExec ((I ';' J),P,s)) . b1 = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . b1
per cases ( x is Int-Location or x is FinSeq-Location or x = IC or x is Element of NAT ) by A50, SCMFSA6A:35;
suppose A51: x is Int-Location ; :: thesis: (IExec ((I ';' J),P,s)) . b1 = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . b1
then x <> IC by SCMFSA_2:81;
then A52: not x in dom (Start-At (l,SCM+FSA)) by A48, TARSKI:def 1;
(IExec ((I ';' J),P,s)) . x = (IExec (J,P,(IExec (I,P,s)))) . x by A46, A51, SCMFSA6A:38;
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 A52, FUNCT_4:12; :: thesis: verum
end;
suppose A53: x is FinSeq-Location ; :: thesis: (IExec ((I ';' J),P,s)) . b1 = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . b1
then x <> IC by SCMFSA_2:82;
then A54: not x in dom (Start-At (l,SCM+FSA)) by A48, TARSKI:def 1;
(IExec ((I ';' J),P,s)) . x = (IExec (J,P,(IExec (I,P,s)))) . x by A46, A53, SCMFSA6A:38;
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 A54, FUNCT_4:12; :: thesis: verum
end;
suppose A55: x = IC ; :: thesis: (IExec ((I ';' J),P,s)) . b1 = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . b1
then x in {(IC )} by TARSKI:def 1;
then A56: x in dom (Start-At (l,SCM+FSA)) by FUNCOP_1:19;
thus (IExec ((I ';' J),P,s)) . x = (Start-At (l,SCM+FSA)) . (IC ) by A47, A55, FUNCOP_1:87
.= ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . x by A55, A56, FUNCT_4:14 ; :: thesis: verum
end;
suppose A57: x is Element of NAT ; :: thesis: (IExec ((I ';' J),P,s)) . b1 = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . b1
then x <> IC by COMPOS_1:3;
then A58: not x in dom (Start-At (l,SCM+FSA)) by A48, TARSKI:def 1;
(IExec ((I ';' J),P,s)) | NAT = ProgramPart s by PBOOLE:157
.= (IExec (J,P,(IExec (I,P,s)))) | NAT by A42, PBOOLE:157 ;
then (IExec ((I ';' J),P,s)) . x = (IExec (J,P,(IExec (I,P,s)))) . x by A57, SCMFSA6A:36;
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 A58, FUNCT_4:12; :: thesis: verum
end;
end;
end;
dom (IExec ((I ';' J),P,s)) = the carrier of SCM+FSA by PARTFUN1:def 4
.= 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 4 ;
hence IExec ((I ';' J),P,s) = (IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA)) by A49, FUNCT_1:9; :: thesis: verum
end;