:: On the Composition of non-parahalting Macro Instructions
:: by Piotr Rudnicki
::
:: Received June 3, 1998
:: Copyright (c) 1998-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies AMI_1, SCMFSA_2, SCMFSA7B, SCMFSA6A, SF_MASTR, GRAPHSP, AMI_3,
SCMFSA6B, AOFA_I00, SCMFSA8C, CARD_1, AMISTD_2, RELAT_1, TARSKI,
XXREAL_0, ARYTM_3, FSM_1, XBOOLE_0, FUNCT_4, NUMBERS, SCMFSA6C, CIRCUIT2,
FUNCT_1, MSUALG_1, SUBSET_1, NAT_1, STRUCT_0, FINSET_1, EXTPRO_1,
SFMASTR1, PARTFUN1, RELOC, FUNCOP_1, COMPOS_1, AMISTD_1, FRECHET;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, FINSET_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4,
FUNCOP_1, PBOOLE, VALUED_1, FUNCT_7, AMI_2, STRUCT_0, MEMSTR_0, COMPOS_0,
COMPOS_1, EXTPRO_1, AMISTD_1, AMISTD_2, SCMFSA_1, SCMFSA_2, SCMFSA6A,
SCMFSA6B, SF_MASTR, SCMFSA6C, SCMFSA7B, SCMFSA8C, XXREAL_0, SEQ_4,
SCMFSA_M;
constructors DOMAIN_1, SETWISEO, SEQ_4, PRE_FF, SCM_1, SCMFSA6A, SF_MASTR,
SCMFSA6B, SCMFSA6C, SCMFSA8A, SCMFSA8B, SCMFSA8C, RELSET_1, PRE_POLY,
AMISTD_2, SCMFSA7B, SCMFSA_1, PBOOLE, AMISTD_1, COMPLEX1, INT_2, NAT_D,
XXREAL_1, MEMSTR_0, SCMFSA_M, FUNCT_7, SCMFSA_X;
registrations ORDINAL1, FINSET_1, XREAL_0, NAT_1, INT_1, SCMFSA_2, SF_MASTR,
SCMFSA6C, SCMFSA8A, SCMFSA8C, SCMFSA_9, SCMFSA10, AMISTD_2, COMPOS_1,
EXTPRO_1, FUNCT_4, FUNCOP_1, STRUCT_0, MEMSTR_0, AMI_3, COMPOS_0,
SCMFSA_M, SCMFSA6A;
requirements NUMERALS, SUBSET, BOOLE, REAL;
definitions EXTPRO_1, SCMFSA7B;
equalities EXTPRO_1, SCMFSA_2, FUNCOP_1, SCMFSA6A, MEMSTR_0, SCMFSA_M,
SCMFSA8C;
expansions SCMFSA7B, SCMFSA_M;
theorems TARSKI, NAT_1, RELAT_1, FUNCT_1, GRFUNC_1, FUNCT_4, SCMFSA_2,
MEMSTR_0, SCMFSA6A, SCMFSA6B, SF_MASTR, SCMFSA6C, SCMFSA7B, SCMFSA8A,
SCMFSA8B, SCMFSA8C, XBOOLE_0, XBOOLE_1, XREAL_1, ORDINAL1, FUNCOP_1,
PBOOLE, PARTFUN1, COMPOS_1, EXTPRO_1, AMI_2, COMPOS_0, SCMFSA_M,
AMISTD_1, AFINSQ_1;
schemes NAT_1;
begin :: Good instructions and good macro instructions
reserve p,P,P1,P2 for Instruction-Sequence of SCM+FSA;
definition
let i be Instruction of SCM+FSA;
attr i is good means
:Def1:
Macro i is good;
end;
registration
let a be read-write Int-Location, b be Int-Location;
cluster a := b -> good;
coherence
by SCMFSA7B:6,SCMFSA8C:70;
cluster AddTo(a, b) -> good;
coherence
by SCMFSA7B:7,SCMFSA8C:70;
cluster SubFrom(a, b) -> good;
coherence
by SCMFSA7B:8,SCMFSA8C:70;
cluster MultBy(a, b) -> good;
coherence
by SCMFSA7B:9,SCMFSA8C:70;
end;
registration
cluster good sequential for Instruction of SCM+FSA;
existence
proof
set a = the read-write Int-Location;
take a:=a;
thus thesis;
end;
end;
registration
let a, b be read-write Int-Location;
cluster Divide(a, b) -> good;
coherence
by SCMFSA7B:10,SCMFSA8C:70;
end;
registration
let l be Element of NAT;
cluster goto l -> good;
coherence
by SCMFSA7B:11,SCMFSA8C:70;
end;
registration
let a be Int-Location, l be Element of NAT;
cluster a =0_goto l -> good;
coherence
by SCMFSA7B:12,SCMFSA8C:70;
cluster a >0_goto l -> good;
coherence
by SCMFSA7B:13,SCMFSA8C:70;
end;
registration
let a be Int-Location, f be FinSeq-Location, b be read-write Int-Location;
cluster b := (f,a) -> good;
coherence
by SCMFSA7B:14,SCMFSA8C:70;
end;
registration
let f be FinSeq-Location, b be read-write Int-Location;
cluster b :=len f -> good;
coherence
by SCMFSA7B:16,SCMFSA8C:70;
end;
registration
let f be FinSeq-Location, a be Int-Location;
cluster f :=<0,...,0> a -> good;
coherence
by SCMFSA7B:17,SCMFSA8C:70;
let b be Int-Location;
cluster (f,a) := b -> good;
coherence
by SCMFSA7B:15,SCMFSA8C:70;
end;
registration
let i be good Instruction of SCM+FSA;
cluster Macro i -> good;
coherence by Def1;
end;
registration
let i, j be good Instruction of SCM+FSA;
cluster i ";" j -> good;
coherence;
end;
registration
let i be good Instruction of SCM+FSA, I be good Program of SCM+FSA;
cluster i ";" I -> good;
coherence;
cluster I ";" i -> good;
coherence;
end;
registration
let a, b be read-write Int-Location;
cluster swap(a, b) -> good;
coherence
proof
swap(a, b) = FirstNotUsed Macro (a := b) := a ";" (a := b) ";" (b :=
FirstNotUsed Macro (a := b)) by SCMFSA6C:def 3;
hence thesis;
end;
end;
registration
let I be good MacroInstruction of SCM+FSA, a be read-write Int-Location;
cluster Times(a, I) -> good;
coherence;
end;
theorem
for a being Int-Location, I being Program of SCM+FSA st not a in
UsedILoc I holds I does not destroy a
proof
let aa be Int-Location, I be Program of SCM+FSA such that
A1: not aa in UsedILoc I;
let i be Instruction of SCM+FSA;
assume i in rng I;
then UsedIntLoc i c= UsedILoc I by SF_MASTR:19;
then
A2: not aa in UsedIntLoc i by A1;
InsCode i <= 12 by SCMFSA_2:16;
then InsCode i = 0 or ... or InsCode i = 12;
then per cases;
suppose
InsCode i = 0;
then i = halt SCM+FSA by SCMFSA_2:95;
hence thesis;
end;
suppose
InsCode i = 1;
then consider a, b be Int-Location such that
A3: i = a:=b by SCMFSA_2:30;
UsedIntLoc i = {a, b} by A3,SF_MASTR:14;
then a in UsedIntLoc i by TARSKI:def 2;
hence thesis by A2,A3,SCMFSA7B:6;
end;
suppose
InsCode i = 2;
then consider a, b be Int-Location such that
A4: i = AddTo(a,b) by SCMFSA_2:31;
UsedIntLoc i = {a, b} by A4,SF_MASTR:14;
then a in UsedIntLoc i by TARSKI:def 2;
hence thesis by A2,A4,SCMFSA7B:7;
end;
suppose
InsCode i = 3;
then consider a, b be Int-Location such that
A5: i = SubFrom(a, b) by SCMFSA_2:32;
UsedIntLoc i = {a, b} by A5,SF_MASTR:14;
then a in UsedIntLoc i by TARSKI:def 2;
hence thesis by A2,A5,SCMFSA7B:8;
end;
suppose
InsCode i = 4;
then consider a, b be Int-Location such that
A6: i = MultBy(a, b) by SCMFSA_2:33;
UsedIntLoc i = {a, b} by A6,SF_MASTR:14;
then a in UsedIntLoc i by TARSKI:def 2;
hence thesis by A2,A6,SCMFSA7B:9;
end;
suppose
InsCode i = 5;
then consider a, b be Int-Location such that
A7: i = Divide(a, b) by SCMFSA_2:34;
A8: UsedIntLoc i = {a, b} by A7,SF_MASTR:14;
then
A9: b in UsedIntLoc i by TARSKI:def 2;
a in UsedIntLoc i by A8,TARSKI:def 2;
hence thesis by A2,A7,A9,SCMFSA7B:10;
end;
suppose
InsCode i = 6;
then ex l be Nat st i = goto l by SCMFSA_2:35;
hence thesis;
end;
suppose
InsCode i = 7;
then
ex l be Nat, a being Int-Location st i =
a=0_goto l by SCMFSA_2:36;
hence thesis;
end;
suppose
InsCode i = 8;
then
ex l be Nat, a being Int-Location st i =
a>0_goto l by SCMFSA_2:37;
hence thesis;
end;
suppose
InsCode i = 9;
then consider a, b be Int-Location, f be FinSeq-Location such that
A10: i = b:=(f,a) by SCMFSA_2:38;
UsedIntLoc i = {a, b} by A10,SF_MASTR:17;
then b in UsedIntLoc i by TARSKI:def 2;
hence thesis by A2,A10,SCMFSA7B:14;
end;
suppose
InsCode i = 10;
then ex a, b be Int-Location, f be FinSeq-Location st i = (f,a) :=b by
SCMFSA_2:39;
hence thesis by SCMFSA7B:15;
end;
suppose
InsCode i = 11;
then consider a be Int-Location, f be FinSeq-Location such that
A11: i = a:=len f by SCMFSA_2:40;
UsedIntLoc i = {a} by A11,SF_MASTR:18;
then a in UsedIntLoc i by TARSKI:def 1;
hence thesis by A2,A11,SCMFSA7B:16;
end;
suppose
InsCode i = 12;
then
ex a be Int-Location, f be FinSeq-Location st i = f :=<0,...,0>a by
SCMFSA_2:41;
hence thesis by SCMFSA7B:17;
end;
end;
begin :: Composition of non parahalting macro instructions
reserve s, S for State of SCM+FSA,
I, J for Program of SCM+FSA,
Ig for good Program of SCM+FSA,
i for good sequential Instruction of SCM+FSA,
j for sequential Instruction of SCM+FSA,
a, b for Int-Location,
f for FinSeq-Location;
set D = Data-Locations SCM+FSA;
set SAt = Start-At(0,SCM+FSA);
::$CT
theorem Th2: :: SCMFSA6B:27
for I,J being really-closed Program of SCM+FSA holds
I is_halting_on Initialized S,P & J is_halting_on IExec(I,P,S),P
implies
I ";" J is_halting_on Initialized S,P
proof let I,J be really-closed Program of SCM+FSA;
assume that
A1: I is_halting_on Initialized S,P and
A2: J is_halting_on IExec(I,P,S),P;
set s = Initialize Initialized S,
p = P +* (I ";" J);
A3: I ";" J c= p by FUNCT_4:25;
Directed I c= I ";" J by SCMFSA6A:16;
then Directed I c= p by A3,XBOOLE_1:1;
then
A4: p +* Directed I = p by FUNCT_4:98;
A5: DataPart Initialized S = DataPart s by MEMSTR_0:79;
then
A6: I is_halting_on s,p by A1,SCMFSA8B:5;
then
A7: p+*I halts_on Initialize s;
set s1 = Initialize s,
p1 = p +* I;
A8: (Initialized S).intloc 0 = 1 by SCMFSA_M:9;
then s.intloc 0 = 1 by A5,SCMFSA_M:2;
then
A9: s1 = Initialized s by SCMFSA_M:18;
set JAt = Start-At(0,SCM+FSA);
set s3 = Initialize Comput(p1,s1,LifeSpan(p1,s1)),
p3 = p1 +* J;
A10: J c= p3 by FUNCT_4:25;
set m3 = LifeSpan(p3,s3);
DataPart IExec(I,P,S) = DataPart IExec(I,P,Initialized S)
by SCMFSA8C:3
.= DataPart IExec(I,p,s) by A1,A5,A8,SCMFSA8C:20
.= DataPart(Result(p+*I,Initialized s)) by SCMFSA6B:def 1
.= DataPart Result(p+*I,Initialized s)
.= DataPart Comput(p1,s1,LifeSpan(p1,s1)) by A9,A7,EXTPRO_1:23;
then
J is_halting_on Comput(p1,s1,LifeSpan(p1,s1)),p1 by A2,SCMFSA8B:5;
then
A11: p3 halts_on s3;
A12: Reloc(J,card I) c= I ";" J by SCMFSA6A:38;
set m1 = LifeSpan(p1,s1);
set s4 = Comput(p,s,m1+1),
p4 = p;
A13: Reloc(J,card I) c= p by A3,A12,XBOOLE_1:1;
reconsider m = m1 + 1 + m3 as Element of NAT by ORDINAL1:def 12;
reconsider kk = DataPart JAt as Function;
A14: DataPart s3 = (DataPart Comput(p1,s1,m1)) +* kk by FUNCT_4:71;
take m;
IC Comput(p,s,m) in NAT;
hence IC Comput(p,s,m) in dom p by PARTFUN1:def 2;
A15: IC s4 = card I by A6,A4,SCMFSA8A:22;
A16: Comput(p,s,m1+1+m3)
= Comput(p,Comput(p,s,m1+1),m3) by EXTPRO_1:4;
DataPart JAt = {} by MEMSTR_0:20;
then DataPart Comput(p1,s1,m1) = DataPart s3 by A14,FUNCT_4:98,XBOOLE_1:2;
then DataPart s4 = DataPart s3 by A6,A4,SCMFSA8A:22;
then
IncAddr(CurInstr(p3,Comput(p3,s3,m3)),card I)
= CurInstr(p,Comput(p,s4,m3)) by A15,A13,A10,SCMFSA8C:16;
then
IncAddr(CurInstr(p3,Comput(p3,s3,m3)),card I)
= CurInstr(p,Comput(p,s,m1+1+m3))
by A16;
then CurInstr(p,Comput(p,s,m))
= IncAddr (halt SCM+FSA,card I) by A11,EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_0:4;
hence thesis;
end;
theorem Th3: :: SCMFSA6B:27
for I being really-closed Program of SCM+FSA
for s being 0-started State of SCM+FSA
st I c= p & p halts_on s
for m being Nat st m <= LifeSpan(p,s) holds
Comput(p, s,m) = Comput(p+*(I ";" J),s,m)
proof let I be really-closed Program of SCM+FSA;
let s be 0-started State of SCM+FSA;
assume that
A1: I c= p and
A2: p halts_on s;
defpred X[Nat] means
$1 <= LifeSpan(p,s) implies
Comput(p, s,$1) = Comput(p+*(I ";" J),s,$1);
A3: for m being Nat st X[m] holds X[m+1]
proof
dom(I ";" J) = dom I \/ dom Reloc(J, card I) by SCMFSA6A:39;
then
A4: dom I c= dom(I ";" J) by XBOOLE_1:7;
set sIJ = s,
pIJ = p+*(I ";" J);
A5: I ";" J c= pIJ by FUNCT_4:25;
let m be Nat;
assume
A6: m <= LifeSpan(p,s) implies
Comput(p, s,m) = Comput(p+*(I ";"J),s,m);
A7: Comput(pIJ,sIJ,m+1) = Following(pIJ,Comput(pIJ,sIJ,m)) by EXTPRO_1:3;
A8: Comput(p,s,m+1) = Following(p,Comput(p,s,m)) by EXTPRO_1:3;
A9: p/.IC Comput(p,s,m) = p.IC Comput(p,s,m) by PBOOLE:143;
assume
A10: m+1 <= LifeSpan(p,s);
then
A11: IC(Comput(p,s,m)) = IC(Comput(pIJ,sIJ,m)) by A6,NAT_1:13;
IC s = 0 by MEMSTR_0:def 11;
then IC s in dom I by AFINSQ_1:65;
then
A12: IC Comput(p,s,m) in dom I by A1,AMISTD_1:21;
A13: CurInstr(p,Comput(p,s,m))
= I.IC(Comput(p,s,m)) by A12,A9,A1,GRFUNC_1:2;
A14: (pIJ)/.IC Comput(pIJ,sIJ,m)
= pIJ.IC Comput(pIJ,sIJ,m) by PBOOLE:143;
m < LifeSpan(p,s) by A10,NAT_1:13;
then I.IC(Comput(p,s,m)) <> halt SCM+FSA by A2,A13,EXTPRO_1:def 15;
then CurInstr(p,Comput(p,s,m))
= (I ";" J).IC(Comput(p,s,m)) by A12,A13,SCMFSA6A:15
.= CurInstr(pIJ,Comput(pIJ,sIJ,m))
by A11,A12,A4,A14,A5,GRFUNC_1:2;
hence thesis by A6,A10,A8,A7,NAT_1:13;
end;
A15: X[0];
thus for n being Nat holds X[n] from NAT_1:sch 2(A15,A3);
end;
Lm1: for I being good really-closed Program of SCM+FSA,
J being really-closed Program of SCM+FSA, s being
State of SCM+FSA st s.intloc 0 = 1 & I is_halting_on s,p &
J is_halting_on IExec(I,p,s),p &
Initialize((intloc 0).-->1) c= s & I ";" J c= p
holds IC Comput(p, s,LifeSpan(p+*I,s) + 1) = card I &
DataPart Comput(p, s,LifeSpan(p+*I,s) + 1)
= DataPart Initialized Comput(p+*I,s,(LifeSpan(p +* I,s))) &
Reloc(J,card I) c= p &
Comput(p, s,LifeSpan(p+*I,s) + 1).intloc 0 = 1 &
p halts_on s &
LifeSpan(p,s) = LifeSpan(p+*I,s) + 1 + LifeSpan(p+*I+*J,
Initialized Result(p+*I,s)) &
(J is good implies (Result(p,s)).intloc 0 = 1)
proof
let I be good really-closed Program of SCM+FSA,
J be really-closed Program of SCM+FSA, s be State of
SCM+FSA such that
A1: s.intloc 0 = 1 and
A2: I is_halting_on s,p and
A3: J is_halting_on IExec(I,p,s),p;
set s1 = s,
p1 = p +* I;
set m1 = LifeSpan(p1,s1);
set s4 = Comput(p,s,m1+1),
p4 = p;
assume
A4: Initialize((intloc 0).-->1) c= s;
then Start-At(0,SCM+FSA) c= s by MEMSTR_0:50;
then
A5: SAt c= s;
A6: s = s +* SAt by A5,FUNCT_4:98
.= Initialize s;
then
A7: p+*I halts_on s by A2;
assume
A8: I ";" J c= p;
Directed I c= I ";" J by SCMFSA6A:16;
then Directed I c= p by A8,XBOOLE_1:1;
then
A9: p +* Directed I = p by FUNCT_4:98;
Start-At(0,SCM+FSA) c= s by A4,MEMSTR_0:50;
then Start-At(0,SCM+FSA) c= s;
then s = Initialize s by FUNCT_4:98;
hence
A10: IC s4 = card I by A2,A9,SCMFSA8A:22;
set JAt = Start-At(0,SCM+FSA);
set InJ = Initialize((intloc 0).-->1);
set s3 = Initialized Comput(p1,s1,m1),
p3 = p1 +* J;
A11: J c= p3 by FUNCT_4:25;
reconsider kk = DataPart JAt as Function;
A12: DataPart JAt = {} by MEMSTR_0:20;
Comput(p1,s1,m1).intloc 0 = s.intloc 0 by A6,SCMFSA8C:68;
then
A13: s3 = Initialize Comput(p1,s1,m1) by A1,SCMFSA_M:18;
then DataPart s3 = DataPart Comput(p1,s1,m1) +* kk by FUNCT_4:71;
then DataPart Comput(p1,s1,m1) = DataPart s3 by A12,FUNCT_4:98,XBOOLE_1:2;
hence
A14: DataPart s4 = DataPart s3 by A2,A6,A9,SCMFSA8A:22;
A15: Reloc(J,card I) c= I ";" J by SCMFSA6A:38;
A16: intloc 0 in dom InJ by SCMFSA_M:10;
A17: s1 = s+*Initialize((intloc 0).-->1) by A4,FUNCT_4:98;
DataPart IExec(I,p,s)
= DataPart(Result(p+*I,Initialized s)) by SCMFSA6B:def 1
.= DataPart Comput(p1,s1,LifeSpan(p1,s1)) by A7,A17,EXTPRO_1:23;
then
J is_halting_on Comput(p1,s1,LifeSpan(p1,s1)),p1 by A3,SCMFSA8B:5;
then
A18: p3 halts_on s3 by A13;
I ";" J c= p by A8;
then Reloc(J,card I) c= p by A15,XBOOLE_1:1;
then Reloc(J,card I) c= p;
hence Reloc(J,card I) c= p;
A19: Reloc(J,card I) c= p by A8,A15,XBOOLE_1:1;
intloc 0 in Int-Locations by AMI_2:def 16;
then
A20: intloc 0 in D by SCMFSA_2:100,XBOOLE_0:def 3;
hence s4.intloc 0 = (DataPart s3).intloc 0 by A14,FUNCT_1:49
.= s3.intloc 0 by A20,FUNCT_1:49
.= 1 by A16,FUNCT_4:13,SCMFSA_M:12;
set m3 = LifeSpan(p3,s3);
reconsider m = m1 + 1 + m3 as Element of NAT by ORDINAL1:def 12;
A21: Comput(p,s,m1+1+m3)
= Comput(p,Comput(p,s,m1+1),m3) by EXTPRO_1:4;
IncAddr(CurInstr(p3,Comput(p3,s3,m3)),card I)
= CurInstr(p,Comput(p,s4,m3))
by A10,A14,A19,A11,SCMFSA8C:16;
then
IncAddr(CurInstr(p3,Comput(p3,s3,m3)),card I)
= CurInstr(p,Comput(p,s,m1+1+m3))
by A21;
then
A22: CurInstr(p,Comput(p,s,m))
= IncAddr (halt SCM+FSA,card I) by A18,EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_0:4;
hence
A23: p halts_on s by EXTPRO_1:29;
A24: now
let k be Element of NAT;
assume m1 + 1 + k < m;
then
A25: k < m3 by XREAL_1:6;
A26: Comput(p,s,m1+1+k) = Comput(p,Comput(p,s,m1+1),k) by EXTPRO_1:4;
assume
A27: CurInstr(p,Comput(p,s,m1+1+k)) = halt SCM+FSA;
A28: InsCode halt SCM+FSA = 0 by COMPOS_1:70;
IncAddr(CurInstr(p3,Comput(p3,s3,k)),card I)
= halt SCM+FSA by A27,A26,A10,A14,A19,A11,SCMFSA8C:16;
then InsCode CurInstr(p3,Comput(p3,s3,k))
= 0 by A28,COMPOS_0:def 9;
then CurInstr(p3,Comput(p3,s3,k)) = halt SCM+FSA by SCMFSA_2:95;
hence contradiction by A18,A25,EXTPRO_1:def 15;
end;
now
let k be Nat;
assume
A29: k < m;
per cases;
suppose
k <= m1;
hence CurInstr(p,Comput(p,s,k)) <>
halt SCM+FSA by A2,A6,A9,SCMFSA8A:21;
end;
suppose
m1 < k;
then m1 + 1 <= k by NAT_1:13;
then consider kk being Nat such that
A30: m1 + 1 + kk = k by NAT_1:10;
reconsider kk as Element of NAT by ORDINAL1:def 12;
m1 + 1 + kk = k by A30;
hence CurInstr(p,Comput(p,s,k)) <>
halt SCM+FSA by A24,A29;
end;
end;
then
for k being Nat st CurInstr(p,Comput(p,s,k))
= halt SCM+FSA
holds m <= k;
then
A31: LifeSpan(p,s) = m by A22,A23,EXTPRO_1:def 15;
Comput(p+*I,s,m1)
= Result(p+*I,s) by A7,EXTPRO_1:23;
hence LifeSpan(p,s)
= LifeSpan(p+*I,s) + 1 + LifeSpan(p+*I+*J,Initialized Result(p+*I,s))
by A31;
Start-At(0,SCM+FSA) c= s3 by FUNCT_4:25,MEMSTR_0:50;
then
A32: Initialize s3 = s3 by FUNCT_4:98;
A33: InJ c= s3 by FUNCT_4:25;
hereby
A34: DataPart Comput(p3, s3,m3) = DataPart Comput(p, s4,m3)
by A10,A14,A19,A11,SCMFSA8C:16;
assume
A35: J is good;
thus (Result(p,s)).intloc 0
= Comput(p, s,m).intloc 0 by A23,A31,EXTPRO_1:23
.= Comput(p, s4,m3).intloc 0 by EXTPRO_1:4
.= Comput(p3, s3,m3).intloc 0 by A34,SCMFSA_M:2
.= s3.intloc 0 by A32,A35,SCMFSA8C:68
.= 1 by A16,A33,GRFUNC_1:2,SCMFSA_M:12;
end;
end;
theorem Th4:
for Ig being good really-closed Program of SCM+FSA
for J being really-closed Program of SCM+FSA holds
Ig is_halting_on Initialized s,p & J is_halting_on IExec(Ig,p,s),p
implies LifeSpan(p +* (Ig ";" J),Initialized s)
= LifeSpan(p +* Ig,Initialized s) + 1 +
LifeSpan(p +* Ig +* J,Initialized Result(p +* Ig,Initialized s))
proof
let Ig be good really-closed Program of SCM+FSA;
let J be really-closed Program of SCM+FSA;
set I = Ig;
assume that
A1: I is_halting_on Initialized s,p and
A2: J is_halting_on IExec(I,p,s),p;
set Is = Initialized s;
A3: (Initialized s).intloc 0 = 1 by SCMFSA_M:9;
set s1 = Initialized s, p1 = p +* I;
set m1 = LifeSpan(p1,s1);
set s3 = Initialized Comput(p1,s1,m1), p3 = p1 +* J;
s1 = Initialized Is;
then
A4: s1 = Initialize Is by A3,SCMFSA_M:18;
then
A5: p1 halts_on s1 by A1;
then
A6: s3 = Initialized Result(p1,s1) by EXTPRO_1:23;
set s2 = Initialized s,
p2 = p +* (I ";" J);
A7: I ";" J c= p2 by FUNCT_4:25;
A8: DataPart Is = DataPart s2;
A9: s2.intloc 0 = 1 by A3;
set JAt = Start-At(0,SCM+FSA);
Comput(p1,s1,m1).intloc 0 = 1 by A3,A4,SCMFSA8C:68;
then
A10: Initialized Comput(p1,s1,m1) = Initialize Comput(p1,s1,m1) by SCMFSA_M:18;
then JAt c= s3 by FUNCT_4:25;
then
A11: s3 = Initialize s3 by FUNCT_4:98;
DataPart IExec(I,p,s) = DataPart(Result(p+*I,Initialized s))
by SCMFSA6B:def 1
.= DataPart Result(p+*I,Initialized s)
.= DataPart Comput(p1,s1,LifeSpan(p1,s1)) by A5,EXTPRO_1:23;
then DataPart IExec(I,p,s) = DataPart s3 by A10,MEMSTR_0:79;
then
A12: J is_halting_on s3,p3 by A2,SCMFSA8B:5;
Initialize s2 = s2 by MEMSTR_0:44;
then Result(p2+*I,s2) = Result(p1,s1)
by A1,A8,SCMFSA8C:72;
then Initialized Result(p2+*I,s2) = s3 by A6;
then
A13: DataPart Initialized Result(p2+*I,s2) = DataPart s3;
A14: DataPart IExec(I,p,s) = DataPart IExec(I,p,Is) by SCMFSA8C:3
.= DataPart IExec(I,p2,s2) by A1,A3,A8,SCMFSA8C:20;
A15: Initialize((intloc 0).-->1) c= Initialized s by FUNCT_4:25;
A16: J is_halting_on IExec(I,p2,s2),p2 by A2,A14,SCMFSA8B:5;
I is_halting_on s2,p2 by A1,A8,SCMFSA8B:5;
then
A17: LifeSpan(p2,s2) = LifeSpan(p2+*I,s2) + 1
+ LifeSpan(p2+*I+*J,Initialized Result(p2+*I,s2))
by A9,A16,A15,Lm1,A7;
Start-At(0,SCM+FSA) c= Initialized Result(p2+*I,s2)
by FUNCT_4:25,MEMSTR_0:50;
then
A18: Initialized Result(p2+*I,s2)
= Initialize Initialized Result(p2 +* I,s2) by FUNCT_4:98;
A19: LifeSpan(p2+*I,s2) = m1 by A1,A4,A8,SCMFSA8C:72;
LifeSpan(p2+*I+*J,Initialized Result(p2+*I,s2)) = LifeSpan(p3,s3)
by A12,A11,A18,A13,SCMFSA8C:72;
hence thesis by A6,A17,A19;
end;
theorem Th5: :: Main theorem
for Ig being good really-closed Program of SCM+FSA
for J being really-closed Program of SCM+FSA holds
Ig is_halting_on Initialized s,p & J is_halting_on IExec(Ig,p,s),p
implies IExec(Ig ";" J,p,s) = IExec(J,p,IExec(Ig,p,s))+*
Start-At(IC IExec(J,p,IExec(Ig,p,s))+card Ig,SCM+FSA)
proof
let Ig be good really-closed Program of SCM+FSA;
let J be really-closed Program of SCM+FSA;
set I = Ig;
assume that
A1: I is_halting_on Initialized s,p and
A2: J is_halting_on IExec(I,p,s),p;
set Is = Initialized s, Ip = p;
A3: (Initialized s).intloc 0 = 1 by SCMFSA_M:9;
set s1 = Initialized s, p1 = p +* I;
A4: I c= p1 by FUNCT_4:25;
set m1 = LifeSpan(p1,s1);
s1 = Initialized Is;
then
A5: s1 = Initialize Is by A3,SCMFSA_M:18;
set s3 = Initialized Comput(p1,s1,m1), p3 = p1 +* J;
A6: J c= p3 by FUNCT_4:25;
A7: p1 halts_on s1 by A1,A5;
then
A8: s3 = Initialized Result(p1,s1) by EXTPRO_1:23;
set s2 = Initialized s,
p2 = p +* (I ";" J);
A9: I ";" J c= p2 by FUNCT_4:25;
s2 = Initialized Is;
then
A10: s2 = Initialize Is by A3,SCMFSA_M:18;
A11: DataPart Is = DataPart s2;
A12: s2.intloc 0 = 1 by A3;
A13: DataPart IExec(I,p,s) = DataPart IExec(I,p,Is) by SCMFSA8C:3
.= DataPart IExec(I,p2,s2) by A1,A3,A11,SCMFSA8C:20;
s2 = Initialize s2 by MEMSTR_0:44;
then
A14: LifeSpan(p2+*I,s2) = m1 by A1,A11,SCMFSA8C:72;
set JAt = Start-At(0,SCM+FSA);
Comput(p1,s1,m1).intloc 0 = 1 by A3,A5,SCMFSA8C:68;
then
A15: s3 = Initialize Comput(p1,s1,m1) by SCMFSA_M:18;
set m3 = LifeSpan(p3,s3);
I ";" J is_halting_on Is,Ip by A1,A2,Th2;
then
A16: p2 halts_on s2 by A10;
A17: IExec(I ";" J,p,s) = Result(p+*(I ";" J),Initialized s) by SCMFSA6B:def 1
.= Comput(p2,s2,LifeSpan(p2,s2)) by A16,EXTPRO_1:23
.= Comput(p2,s2,m1+1+m3) by A1,A2,A8,Th4;
A18: DataPart IExec(I,p,s) = DataPart Result(p+*I,Initialized s)
by SCMFSA6B:def 1
.= DataPart(Result(p+*I,s+*Initialize((intloc 0).-->1)))
.= DataPart Comput(p1,s1,LifeSpan(p1,s1)) by A7,EXTPRO_1:23;
then
J is_halting_on Comput(p1,s1,LifeSpan(p1,s1)),p1 by A2,SCMFSA8B:5;
then
A19: p3 halts_on s3 by A15;
set IEJIs = IExec(J,p,IExec(I,p,s));
set IAt = Start-At(0,SCM+FSA);
A20: Initialize((intloc 0).-->1) c= s2 by FUNCT_4:25;
IExec(I,p,s).intloc 0 = 1 by A1,SCMFSA8C:67;
then
A21: Initialized IExec(I,p,s) = Initialize IExec(I,p,s) by SCMFSA_M:18;
then Result(p1+*J,Result(p1, s1) +*
Initialize((intloc 0).-->1)) = Result(p+*J,IExec(I,p,s) +*
Initialize((intloc 0).-->1)) by A2,A15,A18,A8,SCMFSA8C:72;
then
A22: IC Result(p1+*J,Initialized Result(p1, s1))
= IC Result(p+*J,Initialized IExec(I,p,s));
A23: Result(p+*J,Initialized IExec(I,p,s)) = Result(p3,s3)
by A2,A15,A18,A21,SCMFSA8C:72;
A24: IEJIs = Result(p+*J,Initialized IExec(I,p,s)) by SCMFSA6B:def 1
.= Comput(p3,s3,m3) by A19,A23,EXTPRO_1:23;
A25: I is_halting_on s2,p2 by A1,A11,SCMFSA8B:5;
reconsider l = IC IEJIs + card I as Element of NAT;
reconsider s2t = s +* ((intloc 0) .--> 1) as State of SCM+FSA;
A27: I +* (I ";" J) = I ";" J by SCMFSA6A:18;
A28: p2 +* I +* (I ";" J) = p2 +* (I +* (I ";" J)) by FUNCT_4:14;
A29: I c= p2 +* I by FUNCT_4:25;
A30: p1+*(I ";" J) = p2 by A27,FUNCT_4:14;
A31: Comput(p1,s1,m1) = Comput(p2, s2,m1) by A7,Th3,A4,A30;
s2 = Initialize s2 by MEMSTR_0:44;
then p2+*I halts_on s2 by A25;
then Comput(p2+*I, s2,m1) = Comput(p2+*I+*(I ";" J),s2,m1)
by A14,Th3,A29;
then DataPart Comput(p2+*I, s2,m1)
= DataPart Comput(p2+*I+*(I ";" J),s2,m1)
.= DataPart Comput(p2+*I+*(I ";" J), s2,m1)
.= DataPart Comput(p2+*(I ";" J), s2,m1) by A27,A28
.= DataPart Comput(p2, s2,m1)
.= DataPart Comput(p1,s1,m1)
by A31;
then
A32: DataPart(Comput(p2+*I, s2,m1) +* Initialize((intloc 0).-->1)) =
DataPart
Comput(p1,s1,m1) +* DataPart (Initialize((intloc 0).-->1)) by FUNCT_4:71
.= DataPart (Comput(p1,s1,m1) +* Initialize((intloc 0).-->1))
by FUNCT_4:71;
A33: J is_halting_on IExec(I,p2,s2),p2 by A2,A13,SCMFSA8B:5;
then
A34: DataPart Comput(p2,s2,m1+1) = DataPart Initialized Comput(p2+*I, s2,m1)
by A20,A25,A14,A12,Lm1,A9;
Reloc(J, card I) c= I ";" J by SCMFSA6A:38;
then
A35: Reloc(J, card I) c= p2 by A9,XBOOLE_1:1;
A36: IC Comput(p2,s2,m1+1) = card I by A20,A25,A14,A12,A33,Lm1,A9;
then
A37: DataPart Comput(p2, Comput(p2,s2,m1+1),m3)
= DataPart Comput(p3,s3, m3) by A32,A34,A6,A35,SCMFSA8C:16;
A38: DataPart IExec(I ";" J,p,s) = DataPart Comput(p2,s2,m1+1+m3)
by A17
.= DataPart Comput(p3,s3,m3) by A37,EXTPRO_1:4
.= DataPart IEJIs by A24;
A39: IC Comput(p2, Comput(p2,s2,m1+1),m3) = IC Comput(p3,s3,m3) + card
I by A32,A36,A34,A6,A35,SCMFSA8C:16;
A40: s3 = Initialized Result(p1, s1) by A7,EXTPRO_1:23;
A41: IC IExec(I ";" J,p,s)
= IC Result(p+*(I ";" J),Initialized s) by SCMFSA6B:def 1
.= IC Comput(p2,s2,LifeSpan(p2,s2)) by A16,EXTPRO_1:23
.= IC Comput(p2,s2,m1+1+m3) by A1,A2,A8,Th4
.= IC Comput(p3,s3,m3) + card I by A39,EXTPRO_1:4
.= IC Result(p3,s3) + card I by A19,EXTPRO_1:23
.= IC IEJIs + card I by A22,A40,SCMFSA6B:def 1;
A42: now
let x be object;
assume
A43: x in dom IExec(I ";" J,p,s);
per cases by A43,SCMFSA_M:1;
suppose
A44: x is Int-Location;
then x <> IC SCM+FSA 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 = IEJIs.x by A38,A44,SCMFSA_M:2;
hence IExec(I ";" J,p,s).x =
(IEJIs +* Start-At (IC IEJIs + card I,SCM+FSA)).x by A45,FUNCT_4:11;
end;
suppose
A46: x is FinSeq-Location;
then x <> IC SCM+FSA 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 = IEJIs.x by A38,A46,SCMFSA_M:2;
hence IExec(I ";" J,p,s).x =
(IEJIs +* Start-At (IC IEJIs + card I,SCM+FSA)).x by A47,FUNCT_4:11;
end;
suppose
A48: x = IC SCM+FSA;
then x in {IC SCM+FSA} 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 SCM+FSA
by A41,A48,FUNCOP_1:72
.= (IEJIs +* Start-At (IC IEJIs + card I,SCM+FSA)).x
by A48,A49,FUNCT_4:13;
end;
end;
dom IExec(I ";" J,p,s) = the carrier of SCM+FSA by PARTFUN1:def 2
.= dom (IEJIs +* Start-At (IC IEJIs + card I,SCM+FSA)) by PARTFUN1:def 2;
hence thesis by A42,FUNCT_1:2;
end;
theorem Th6:
for Ig being good really-closed Program of SCM+FSA
for J being really-closed Program of SCM+FSA holds
(Ig is parahalting or Ig is_halting_on Initialized s,p) &
(J is parahalting or J is_halting_on IExec(Ig,p,s),p)
implies IExec(Ig ";" J,p,s).a = IExec(J,p,IExec(Ig,p,s)).a
proof
let Ig be good really-closed Program of SCM+FSA;
let J be really-closed Program of SCM+FSA;
set I = Ig;
assume that
A1: I is parahalting or I is_halting_on Initialized s,p
and
A2: J is parahalting or J is_halting_on IExec(I,p,s),p;
A3: J is_halting_on IExec(I,p,s),p by A2,SCMFSA7B:19;
A4: not a in dom Start-At (IC IExec(J,p,IExec(I,p,s)) + card I,SCM+FSA)
by SCMFSA_2:102;
I is_halting_on Initialized s,p by A1,SCMFSA7B:19;
then
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 A3,Th5;
hence thesis by A4,FUNCT_4:11;
end;
theorem Th7:
for Ig being good really-closed Program of SCM+FSA
for J being really-closed Program of SCM+FSA holds
(Ig is parahalting or Ig is_halting_on Initialized s,p) &
(J is parahalting or J is_halting_on IExec(Ig,p,s),p)
implies IExec(Ig ";" J,p,s).f = IExec(J,p,IExec(Ig,p,s)).f
proof
let Ig be good really-closed Program of SCM+FSA;
let J be really-closed Program of SCM+FSA;
set I = Ig;
assume that
A1: I is parahalting or I is_halting_on Initialized s,p
and
A2: J is parahalting or J is_halting_on IExec(I,p,s),p;
A3: J is_halting_on IExec(I,p,s),p by A2,SCMFSA7B:19;
A4: not f in dom Start-At (IC IExec(J,p,IExec(I,p,s)) + card I,SCM+FSA)
by SCMFSA_2:103;
I is_halting_on Initialized s,p by A1,SCMFSA7B:19;
then
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 A3,Th5;
hence thesis by A4,FUNCT_4:11;
end;
theorem
for Ig being good really-closed Program of SCM+FSA
for J being really-closed Program of SCM+FSA holds
(Ig is parahalting or Ig is_halting_on Initialized s,p) &
(J is parahalting or J is_halting_on IExec(Ig,p,s),p)
implies DataPart IExec(Ig ";" J,p,s) = DataPart IExec(J,p,IExec(Ig,p,s))
proof
let Ig be good really-closed Program of SCM+FSA;
let J be really-closed Program of SCM+FSA;
set I = Ig;
assume that
A1: I is parahalting or I is_halting_on Initialized s,p
and
A2: J is parahalting or J is_halting_on IExec(I,p,s),p;
A3: for f holds IExec(I ";" J,p,s).f = IExec(J,p,IExec(I,p,s)).f by A1,A2,Th7;
for a holds IExec(I ";" J,p,s).a = IExec(J,p,IExec(I,p,s)).a by A1,A2,Th6;
hence thesis by A3,SCMFSA_M:2;
end;
theorem Th9:
for Ig being good really-closed Program of SCM+FSA holds
Ig is parahalting or Ig is_halting_on Initialized s,p implies
DataPart Initialized IExec(Ig,p,s)= DataPart IExec(Ig,p,s)
proof let Ig be good really-closed Program of SCM+FSA;
set I = Ig;
set IE = IExec(I,p,s);
assume that
A1: I is parahalting or I is_halting_on Initialized s,p;
A2: I is_halting_on Initialized s,p by A1,SCMFSA7B:19;
now
A3: dom ( Initialized IE) = the carrier of SCM+FSA by PARTFUN1:def 2;
A4: dom ( Initialized IE) = D \/ {IC SCM+FSA} by MEMSTR_0:13
.= D \/ ({IC SCM+FSA});
A5: dom IE = the carrier of SCM+FSA by PARTFUN1:def 2;
hence dom DataPart Initialized IE = dom IE /\ D by A3,RELAT_1:61;
then
A6: dom DataPart Initialized IE = D by A3,A5,A4,XBOOLE_1:21;
let x be object;
assume
A7: x in dom DataPart Initialized IE;
per cases by A7,A6,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in Int-Locations;
then reconsider x9 = x as Int-Location by AMI_2:def 16;
hereby
per cases;
suppose
A8: x9 is read-write;
thus (DataPart Initialized IE).x =
( Initialized IE).x by A7,A6,FUNCT_1:49
.= IE.x by A8,SCMFSA_M:37;
end;
suppose
x9 is read-only;
then
A9: x9 = intloc 0;
thus (DataPart Initialized IE).x =
( Initialized IE).x9 by A7,A6,FUNCT_1:49
.= 1 by A9,SCMFSA_M:9
.= IE.x by A2,A9,SCMFSA8C:67;
end;
end;
end;
suppose
x in FinSeq-Locations;
then reconsider x9 = x as FinSeq-Location by SCMFSA_2:def 5;
thus (DataPart Initialized IE).x = ( Initialized IE).x9
by A7,A6,FUNCT_1:49
.= IE.x by SCMFSA_M:37;
end;
end;
hence thesis by FUNCT_1:46;
end;
theorem Th10:
for Ig being good really-closed Program of SCM+FSA holds
Ig is parahalting or Ig is_halting_on Initialized s,p
implies IExec(Ig ";" j,p,s).a = Exec(j, IExec(Ig,p,s)).a
proof let Ig be good really-closed Program of SCM+FSA;
set I = Ig;
set Mj = Macro j;
a in Int-Locations by AMI_2:def 16;
then
A1: a in D by SCMFSA_2:100,XBOOLE_0:def 3;
assume that
A2: I is parahalting or I is_halting_on Initialized s,p;
A3: DataPart Initialized IExec(I,p,s)
= DataPart IExec(I,p,s) by A2,Th9;
thus IExec(I ";" j,p,s).a = IExec(Mj,p,IExec(I,p,s)).a by A2,Th6
.= ( IExec(Mj,p,IExec(I,p,s))).a
.= ( Exec(j, Initialized IExec(I,p,s))).a by SCMFSA6C:5
.= Exec(j, Initialized IExec(I,p,s)).a
.= (DataPart Exec(j, Initialized IExec(I,p,s))).a by A1,FUNCT_1:49
.= (DataPart Exec(j, IExec(I,p,s))).a by A3,SCMFSA6C:4
.= Exec(j, IExec(I,p,s)).a by A1,FUNCT_1:49;
end;
theorem Th11:
for Ig being good really-closed Program of SCM+FSA holds
Ig is parahalting or Ig is_halting_on Initialized s,p
implies IExec(Ig ";" j,p,s).f = Exec(j, IExec(Ig,p,s)).f
proof let Ig be good really-closed Program of SCM+FSA;
set I = Ig;
set Mj = Macro j;
f in FinSeq-Locations by SCMFSA_2:def 5;
then
A1: f in D by SCMFSA_2:100,XBOOLE_0:def 3;
assume that
A2: I is parahalting or I is_halting_on Initialized s,p;
A3: DataPart Initialized IExec(I,p,s) = DataPart IExec(I,p,s) by A2,Th9;
thus IExec(I ";" j,p,s).f = IExec(Mj,p,IExec(I,p,s)).f by A2,Th7
.= ( IExec(Mj,p,IExec(I,p,s))).f
.= ( Exec(j, Initialized IExec(I,p,s))).f by SCMFSA6C:5
.= Exec(j, Initialized IExec(I,p,s)).f
.= (DataPart Exec(j, Initialized IExec(I,p,s))).f by A1,FUNCT_1:49
.= (DataPart Exec(j, IExec(I,p,s))).f by A3,SCMFSA6C:4
.= Exec(j, IExec(I,p,s)).f by A1,FUNCT_1:49;
end;
theorem
for Ig being good really-closed Program of SCM+FSA holds
Ig is parahalting or Ig is_halting_on Initialized s,p
implies DataPart IExec(Ig ";" j,p,s) = DataPart Exec(j, IExec(Ig,p,s))
proof let Ig be good really-closed Program of SCM+FSA;
set I = Ig;
assume
A1: I is parahalting or I is_halting_on Initialized s,p;
then
A2: for f holds IExec(I ";" j,p,s).f = Exec(j, IExec(I,p,s)).f by Th11;
for a holds IExec(I ";" j,p,s).a = Exec(j, IExec(I,p,s)).a by A1,Th10;
hence thesis by A2,SCMFSA_M:2;
end;
theorem Th13:
for J being really-closed Program of SCM+FSA holds
J is parahalting or J is_halting_on Exec(i, Initialized s),p
implies IExec(i ";" J,p,s).a = IExec(J,p,Exec(i,Initialized s)).a
proof let J be really-closed Program of SCM+FSA;
set Mi = Macro i;
A1: IExec(Mi,p,s) = Exec(i,Initialized s) by SCMFSA6C:5;
assume J is parahalting or J is_halting_on Exec(i, Initialized s),p;
then
A2: J is_halting_on Exec(i, Initialized s),p
by SCMFSA7B:19;
J is_halting_on IExec(Mi,p,s),p by A2,A1;
hence IExec(i ";" J,p,s).a
= IExec(J,p,IExec(Mi,p,s)).a by Th6
.= ( IExec(J,p,IExec(Mi,p,s))).a
.= ( IExec(J,p,Exec(i,Initialized s))).a by A1
.= IExec(J,p,Exec(i,Initialized s)).a;
end;
theorem Th14:
for J being really-closed Program of SCM+FSA holds
J is parahalting or J is_halting_on Exec(i, Initialized s),p
implies IExec(i ";" J,p,s).f = IExec(J,p,Exec(i,Initialized s)).f
proof let J be really-closed Program of SCM+FSA;
set Mi = Macro i;
A1: IExec(Mi,p,s) = Exec(i,Initialized s) by SCMFSA6C:5;
assume J is parahalting or J is_halting_on Exec(i, Initialized s),p;
then
A2: J is_halting_on Exec(i, Initialized s),p
by SCMFSA7B:19;
J is_halting_on IExec(Mi,p,s),p by A2,A1;
hence IExec(i ";" J,p,s).f = IExec(J,p,IExec(Mi,p,s)).f by Th7
.= ( IExec(J,p,IExec(Mi,p,s))).f
.= ( IExec(J,p,Exec(i,Initialized s))).f by A1
.= IExec(J,p,Exec(i,Initialized s)).f;
end;
theorem
for J being really-closed Program of SCM+FSA holds
J is parahalting or J is_halting_on Exec(i, Initialized s),p
implies
DataPart IExec(i ";" J,p,s) = DataPart IExec(J,p,Exec(i,Initialized s))
proof let J be really-closed Program of SCM+FSA;
assume
A1: J is parahalting or J is_halting_on Exec(i, Initialized s),p;
then
A2: for f holds IExec(i ";" J,p,s).f = IExec(J,p,Exec(i,Initialized s)).f
by Th14;
for a holds IExec(i ";" J,p,s).a
= IExec(J,p,Exec(i,Initialized s)).a by A1,Th13;
hence thesis by A2,SCMFSA_M:2;
end;
begin :: Memory allocation
reserve L for finite Subset of Int-Locations,
m, n for Nat;
definition
::$CD 2
let n be Element of NAT, p be preProgram of SCM+FSA;
func n-thNotUsed p -> Int-Location equals
n-thRWNotIn UsedILoc p;
correctness;
end;
notation
let n be Element of NAT, p be preProgram of SCM+FSA;
synonym n-stNotUsed p for n-thNotUsed p;
synonym n-ndNotUsed p for n-thNotUsed p;
synonym n-rdNotUsed p for n-thNotUsed p;
end;
registration
let n be Element of NAT, p be preProgram of SCM+FSA;
cluster n-thNotUsed p -> read-write;
coherence;
end;