let s be State of SCM+FSA ; :: thesis: for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds IExec (I ';' J),s = (IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))
set SA0 = Start-At (insloc 0 );
let I be parahalting keeping_0 Program of SCM+FSA ; :: thesis: for J being parahalting Program of SCM+FSA holds IExec (I ';' J),s = (IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))
let J be parahalting Program of SCM+FSA ; :: thesis: IExec (I ';' J),s = (IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))
set ps = s | NAT ;
set s1 = s +* (Initialized I);
set s2 = s +* (Initialized (I ';' J));
set s3 = (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J);
set m1 = LifeSpan (s +* (Initialized I));
set m3 = LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J));
set A = NAT ;
set D = Int-Locations \/ FinSeq-Locations ;
A1: Initialized I c= s +* (Initialized I) by FUNCT_4:26;
A2: s +* (Initialized I) is halting by Th19, FUNCT_4:26;
A3: I +* (Start-At (insloc 0 )) c= s +* (Initialized I) by Th8, FUNCT_4:26;
A4: Initialized (I ';' J) c= s +* (Initialized (I ';' J)) by FUNCT_4:26;
( Start-At (insloc 0 ) c= Initialized (I ';' J) & Initialized (I ';' J) c= s +* (Initialized (I ';' J)) ) by FUNCT_4:26;
then A5: Start-At (insloc 0 ) c= s +* (Initialized (I ';' J)) by XBOOLE_1:1;
I +* (Start-At (insloc 0 )) c= (s +* (Initialized (I ';' J))) +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:26;
then I +* (Start-At (insloc 0 )) c= ((s +* (Initialized (I ';' J))) +* I) +* (Start-At (insloc 0 )) by FUNCT_4:15;
then I +* (Start-At (insloc 0 )) c= ((s +* (Initialized (I ';' J))) +* (Start-At (insloc 0 ))) +* I by Th14;
then I +* (Start-At (insloc 0 )) c= (s +* (Initialized (I ';' J))) +* I by A5, FUNCT_4:79;
then A6: (s +* (Initialized (I ';' J))) +* I is halting by Th18;
A7: Initialized J c= (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J) by FUNCT_4:26;
A8: dom (s | NAT ) = (dom s) /\ NAT by RELAT_1:90
.= (((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT ) /\ NAT by AMI_1:79, SCMFSA_2:8
.= NAT by XBOOLE_1:21 ;
A9: (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J),((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (s | NAT )) +* (Initialized J) equal_outside dom (s | NAT ) by FUNCT_7:31, FUNCT_7:106;
then A10: ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (s | NAT )) +* (Initialized J),(Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J) equal_outside dom (s | NAT ) by FUNCT_7:28;
Result ((IExec I,s) +* (Initialized J)), Result ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)) equal_outside NAT
proof
A11: J +* (Start-At (insloc 0 )) c= (IExec I,s) +* (Initialized J) by Th8, FUNCT_4:26;
A12: J +* (Start-At (insloc 0 )) c= (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J) by Th8, FUNCT_4:26;
IExec I,s = (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (s | NAT ) by A1, Th19, AMI_1:122;
hence Result ((IExec I,s) +* (Initialized J)), Result ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)) equal_outside NAT by A8, A10, A11, A12, Th29; :: thesis: verum
end;
then A13: (Result ((IExec I,s) +* (Initialized J))) +* (s | NAT ) = (Result ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J))) +* (s | NAT ) by A8, FUNCT_7:108;
A14: (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J) = (Result (s +* (Initialized I))) +* (Initialized J) by A1, Th19, AMI_1:122;
A15: IExec (I ';' J),s = (Computation (s +* (Initialized (I ';' J))),(LifeSpan (s +* (Initialized (I ';' J))))) +* (s | NAT ) by A4, Th19, AMI_1:122
.= (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J))))) +* (s | NAT ) by A14, Th43 ;
A16: (IExec I,s) | NAT = s | NAT by CARD_3:99;
then A17: IExec J,(IExec I,s) = (Computation ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)))) +* (s | NAT ) by A7, A13, Th19, AMI_1:122;
Initialized I c= (s +* (Initialized (I ';' J))) +* I by FUNCT_4:26, SCMFSA6A:52;
then A18: I +* (Start-At (insloc 0 )) c= (s +* (Initialized (I ';' J))) +* I by Th8;
A19: s +* (Initialized I),s +* (Initialized (I ';' J)) equal_outside NAT by SCMFSA6A:53;
s +* (Initialized (I ';' J)),(s +* (Initialized (I ';' J))) +* I equal_outside NAT by AMI_1:120;
then s +* (Initialized I),(s +* (Initialized (I ';' J))) +* I equal_outside NAT by A19, FUNCT_7:29;
then A20: LifeSpan ((s +* (Initialized (I ';' J))) +* I) = LifeSpan (s +* (Initialized I)) by A3, A18, Th29;
then A21: ( IC (Computation (s +* (Initialized (I ';' J))),((LifeSpan (s +* (Initialized I))) + 1)) = insloc (card I) & DataPart (Computation (s +* (Initialized (I ';' J))),((LifeSpan (s +* (Initialized I))) + 1)) = DataPart ((Computation ((s +* (Initialized (I ';' J))) +* I),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)) & ProgramPart (Relocated J,(card I)) c= Computation (s +* (Initialized (I ';' J))),((LifeSpan (s +* (Initialized I))) + 1) & (Computation (s +* (Initialized (I ';' J))),((LifeSpan (s +* (Initialized I))) + 1)) . (intloc 0 ) = 1 ) by A4, Lm4;
A22: ( DataPart (Computation (Computation (s +* (Initialized (I ';' J))),((LifeSpan (s +* (Initialized I))) + 1)),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)))) = DataPart (Computation ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)))) & IC (Computation (Computation (s +* (Initialized (I ';' J))),((LifeSpan (s +* (Initialized I))) + 1)),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)))) = (IC (Computation ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J))))) + (card I) )
proof
A23: J +* (Start-At (insloc 0 )) c= (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J) by Th8, FUNCT_4:26;
A24: (s +* (Initialized I)) +* (I ';' J) = s +* ((Initialized I) +* (I ';' J)) by FUNCT_4:15
.= s +* (Initialized (I ';' J)) by SCMFSA6A:58 ;
DataPart (Computation ((s +* (Initialized (I ';' J))) +* I),(LifeSpan (s +* (Initialized I)))) = DataPart (Computation (((s +* (Initialized (I ';' J))) +* I) +* (I ';' J)),(LifeSpan (s +* (Initialized I)))) by A6, A18, A20, Th36, SCMFSA6A:39
.= DataPart (Computation ((s +* (Initialized (I ';' J))) +* (I +* (I ';' J))),(LifeSpan (s +* (Initialized I)))) by FUNCT_4:15
.= DataPart (Computation ((s +* (Initialized (I ';' J))) +* (I ';' J)),(LifeSpan (s +* (Initialized I)))) by SCMFSA6A:57
.= DataPart (Computation (s +* ((Initialized (I ';' J)) +* (I ';' J))),(LifeSpan (s +* (Initialized I)))) by FUNCT_4:15
.= DataPart (Computation (s +* (Initialized (I ';' J))),(LifeSpan (s +* (Initialized I)))) by LATTICE2:8, SCMFSA6A:26
.= DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) by A2, A3, A24, Th36, SCMFSA6A:39 ;
then DataPart ((Computation ((s +* (Initialized (I ';' J))) +* I),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)) = (DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))) +* (DataPart (Initialized J)) by FUNCT_4:75
.= DataPart ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)) by FUNCT_4:75 ;
hence ( DataPart (Computation (Computation (s +* (Initialized (I ';' J))),((LifeSpan (s +* (Initialized I))) + 1)),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)))) = DataPart (Computation ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)))) & IC (Computation (Computation (s +* (Initialized (I ';' J))),((LifeSpan (s +* (Initialized I))) + 1)),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)))) = (IC (Computation ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J))))) + (card I) ) by A21, A23, Th27; :: thesis: verum
end;
A25: DataPart (IExec (I ';' J),s) = DataPart (IExec J,(IExec I,s))
proof
A26: dom (s | NAT ) misses Int-Locations \/ FinSeq-Locations by A8, SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
hence DataPart (IExec (I ';' J),s) = DataPart (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J))))) by A15, FUNCT_4:76, SCMFSA_2:127
.= DataPart (Computation ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)))) by A22, AMI_1:51
.= DataPart (IExec J,(IExec I,s)) by A17, A26, FUNCT_4:76, SCMFSA_2:127 ;
:: thesis: verum
end;
A27: Result (s +* (Initialized I)) = Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))) by A1, Th19, AMI_1:122;
A28: J +* (Start-At (insloc 0 )) c= (Result (s +* (Initialized I))) +* (Initialized J) by Th8, FUNCT_4:26;
J +* (Start-At (insloc 0 )) c= (IExec I,s) +* (Initialized J) by Th8, FUNCT_4:26;
then A29: IC (Result ((Result (s +* (Initialized I))) +* (Initialized J))) = IC (Result ((IExec I,s) +* (Initialized J))) by A8, A9, A27, A28, Th29, AMI_1:121;
A30: IC (IExec (I ';' J),s) = IC (Result (s +* (Initialized (I ';' J)))) by Th30
.= IC (Computation (s +* (Initialized (I ';' J))),(LifeSpan (s +* (Initialized (I ';' J))))) by A4, Th19, AMI_1:122
.= IC (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J))))) by A14, Th43
.= (IC (Computation ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J))))) + (card I) by A22, AMI_1:51
.= (IC (Result ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)))) + (card I) by A7, Th19, AMI_1:122
.= (IC (Result ((Result (s +* (Initialized I))) +* (Initialized J)))) + (card I) by A1, Th19, AMI_1:122
.= (IC (IExec J,(IExec I,s))) + (card I) by A29, Th30 ;
hereby :: thesis: verum
A31: dom (IExec (I ';' J),s) = the carrier of SCM+FSA by AMI_1:79
.= dom ((IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))) by AMI_1:79 ;
reconsider l = (IC (IExec J,(IExec I,s))) + (card I) as Instruction-Location of SCM+FSA ;
A32: dom (Start-At l) = {(IC SCM+FSA )} by FUNCOP_1:19;
now
let x be set ; :: thesis: ( x in dom (IExec (I ';' J),s) implies (IExec (I ';' J),s) . b1 = ((IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))) . b1 )
assume A33: x in dom (IExec (I ';' J),s) ; :: thesis: (IExec (I ';' J),s) . b1 = ((IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))) . b1
per cases ( x is Int-Location or x is FinSeq-Location or x = IC SCM+FSA or x is Instruction-Location of SCM+FSA ) by A33, SCMFSA6A:35;
suppose A34: x is Int-Location ; :: thesis: (IExec (I ';' J),s) . b1 = ((IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))) . b1
then A35: (IExec (I ';' J),s) . x = (IExec J,(IExec I,s)) . x by A25, SCMFSA6A:38;
x <> IC SCM+FSA by A34, SCMFSA_2:81;
then not x in dom (Start-At l) by A32, TARSKI:def 1;
hence (IExec (I ';' J),s) . x = ((IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))) . x by A35, FUNCT_4:12; :: thesis: verum
end;
suppose A36: x is FinSeq-Location ; :: thesis: (IExec (I ';' J),s) . b1 = ((IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))) . b1
then A37: (IExec (I ';' J),s) . x = (IExec J,(IExec I,s)) . x by A25, SCMFSA6A:38;
x <> IC SCM+FSA by A36, SCMFSA_2:82;
then not x in dom (Start-At l) by A32, TARSKI:def 1;
hence (IExec (I ';' J),s) . x = ((IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))) . x by A37, FUNCT_4:12; :: thesis: verum
end;
suppose A38: x = IC SCM+FSA ; :: thesis: (IExec (I ';' J),s) . b1 = ((IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))) . b1
then x in {(IC SCM+FSA )} by TARSKI:def 1;
then A39: x in dom (Start-At l) by FUNCOP_1:19;
thus (IExec (I ';' J),s) . x = (Start-At l) . (IC SCM+FSA ) by A30, A38, FUNCOP_1:87
.= ((IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))) . x by A38, A39, FUNCT_4:14 ; :: thesis: verum
end;
suppose A40: x is Instruction-Location of SCM+FSA ; :: thesis: (IExec (I ';' J),s) . b1 = ((IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))) . b1
(IExec (I ';' J),s) | NAT = s | NAT by CARD_3:99
.= (IExec J,(IExec I,s)) | NAT by A16, CARD_3:99 ;
then A41: (IExec (I ';' J),s) . x = (IExec J,(IExec I,s)) . x by A40, SCMFSA6A:36;
x <> IC SCM+FSA by A40, AMI_1:48;
then not x in dom (Start-At l) by A32, TARSKI:def 1;
hence (IExec (I ';' J),s) . x = ((IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))) . x by A41, FUNCT_4:12; :: thesis: verum
end;
end;
end;
hence IExec (I ';' J),s = (IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I))) by A31, FUNCT_1:9; :: thesis: verum
end;