:: On the compositions of macro instructions, Part III
:: by Noriko Asamoto , Yatsuka Nakamura , Piotr Rudnicki and Andrzej Trybulec
::
:: Received July 22, 1996
:: Copyright (c) 1996-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, FSM_1, CARD_1, SCMFSA6B, FUNCT_1, RELAT_1,
ARYTM_3, FUNCT_4, SCMFSA6A, TARSKI, XBOOLE_0, CIRCUIT2, NUMBERS, GRAPHSP,
AMI_3, XXREAL_0, SF_MASTR, FUNCOP_1, STRUCT_0, ARYTM_1, INT_1, COMPLEX1,
PARTFUN1, FINSEQ_1, FINSEQ_2, AOFA_I00, EXTPRO_1, SCMFSA6C, COMPOS_1,
NAT_1, AMISTD_1, FRECHET, TURING_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ENUMSET1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, NAT_1, INT_1, COMPLEX1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1,
FINSEQ_2, FUNCOP_1, FUNCT_4, PBOOLE, STRUCT_0, MEMSTR_0, COMPOS_0,
COMPOS_1, COMPOS_2, EXTPRO_1, AMISTD_1, FUNCT_7, SCMFSA_M, SCMFSA_2,
SCMFSA10, SCMFSA6A, SF_MASTR, SCMFSA6B, XXREAL_0;
constructors DOMAIN_1, SETWISEO, XXREAL_0, INT_2, SCMFSA6A, SF_MASTR,
SCMFSA6B, RELSET_1, PRE_POLY, AMISTD_1, AMISTD_2, PBOOLE, FUNCT_4,
MEMSTR_0, SCMFSA_1, SCMFSA_M, FUNCT_7, SCMFSA10, COMPOS_2;
registrations FUNCT_1, FUNCOP_1, XREAL_0, INT_1, SCMFSA_2, SF_MASTR, SCMFSA6B,
ORDINAL1, RELSET_1, COMPOS_1, STRUCT_0, EXTPRO_1, FUNCT_4, MEMSTR_0,
AMI_3, COMPOS_0, SCMFSA_M, SCMFSA6A, SCMFSA10, AMISTD_2;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions SCMFSA6B, AMISTD_1;
equalities FUNCOP_1, EXTPRO_1, SCMFSA6B, SCMFSA6A, MEMSTR_0, SCMFSA_2,
SCMFSA_M, COMPOS_2;
expansions EXTPRO_1, SCMFSA_M;
theorems RELAT_1, FUNCT_4, FUNCT_1, ZFMISC_1, FUNCOP_1, TARSKI, NAT_1,
SCMFSA_2, ENUMSET1, GRFUNC_1, SCMFSA6A, SF_MASTR, SCMFSA6B, XBOOLE_0,
XBOOLE_1, PARTFUN1, COMPOS_1, EXTPRO_1, AMISTD_2, PBOOLE, STRUCT_0,
MEMSTR_0, AMISTD_1, AMI_2, SCMFSA_M, AFINSQ_1;
begin :: Consequences of the main theorem from SCMFSA6B
reserve x for set,
i for Instruction of SCM+FSA,
a,b for Int-Location,
f for FinSeq-Location,
l, l1 for Nat,
s,s1,s2 for State of SCM+FSA,
P,P1,P2 for Instruction-Sequence of SCM+FSA;
set SA0 = Start-At(0,SCM+FSA);
theorem
for I being keeping_0 parahalting really-closed Program of SCM+FSA,
J being parahalting really-closed Program of SCM+FSA
holds IExec(I ";" J,P,s).a = IExec(J,P,IExec(I,P,s)).a
proof
let I be keeping_0 parahalting really-closed Program of SCM+FSA,
J be parahalting really-closed Program of SCM+FSA;
A1: not a in dom Start-At (IC IExec(J,P,IExec(I,P,s)) + card I,SCM+FSA)
by SCMFSA_2:102;
IExec(I ";" J,P,s) = IncIC(IExec(J,P,IExec(I,P,s)),card I) by SCMFSA6B:20;
hence thesis by A1,FUNCT_4:11;
end;
theorem
for I being keeping_0 parahalting really-closed Program of SCM+FSA,
J being parahalting really-closed Program of SCM+FSA
holds IExec(I ";" J,P,s).f = IExec(J,P,IExec(I,P,s)).f
proof
let I be keeping_0 parahalting really-closed Program of SCM+FSA,
J be parahalting really-closed Program of SCM+FSA;
A1: not f in dom Start-At (IC IExec(J,P,IExec(I,P,s)) + card I,SCM+FSA)
by SCMFSA_2:103;
IExec(I ";" J,P,s) = IncIC(IExec(J,P,IExec(I,P,s)),card I) by SCMFSA6B:20;
hence thesis by A1,FUNCT_4:11;
end;
begin :: Properties of simple macro instructions
::$CD
definition
let i be Instruction of SCM+FSA;
:: attr i is parahalting means
:: :Def1:
:: Macro i is parahalting;
attr i is keeping_0 means
:Def1:
Macro i is keeping_0;
end;
Lm1: Macro halt SCM+FSA is keeping_0
proof
set Mi = Macro halt SCM+FSA;
let s be 0-started State of SCM+FSA;
A1: Start-At(0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA;
assume
A2: Mi c= P;
let k be Nat;
A3: (P)/.IC s = P.IC s by PBOOLE:143;
A4: 0 in dom Mi by COMPOS_1:60;
CurInstr(P,Comput(P,s,0))
= P.0 by A1,A3,MEMSTR_0:39
.= Mi.0 by A2,A4,GRFUNC_1:2
.= halt SCM+FSA by COMPOS_1:58;
hence (Comput(P,s,k)).intloc 0 = s.intloc 0 by EXTPRO_1:5,NAT_1:2;
end;
registration
cluster halt SCM+FSA -> keeping_0;
coherence by Lm1;
end;
registration
let i be sequential Instruction of SCM+FSA;
cluster Macro i -> parahalting;
coherence
proof let s being 0-started State of SCM+FSA;
let P being Instruction-Sequence of SCM+FSA such that
A1: Macro i c= P;
dom P = NAT by PARTFUN1:def 2;
then
A2: 0 in dom P;
A3: 0 in dom Macro i & 1 in dom Macro i by COMPOS_1:57;
A4: IC s = 0 by MEMSTR_0:def 11;
A5: P.0 = (Macro i).0 by A1,GRFUNC_1:2,A3
.= i by COMPOS_1:58;
Comput(P,s,0+1) = Following(P,Comput(P,s,0)) by EXTPRO_1:3
.= Exec(i,s) by A5,A2,A4,PARTFUN1:def 6;
then
A6: IC Comput(P,s,1) = 0+1 by AMISTD_1:def 8,A4;
then (Macro i).IC Comput(P,s,1) = halt SCM+FSA by COMPOS_1:59;
then P.IC Comput(P,s,1) = halt SCM+FSA by A3,A1,GRFUNC_1:2,A6;
hence P halts_on s by EXTPRO_1:30;
end;
end;
registration
let a, b be Int-Location;
let f be FinSeq-Location;
cluster (f,a) := b -> keeping_0;
coherence
proof
thus (f,a) := b is keeping_0
proof
set Ma = Macro ((f,a):=b);
let s be 0-started State of SCM+FSA;
A1: Start-At(0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA;
assume
A2: Ma c= P;
let k be Nat;
A3: IC SCM+FSA in dom SA0 by TARSKI:def 1;
A4: IC s = SA0.IC SCM+FSA by A3,A1,GRFUNC_1:2
.= 0 by FUNCOP_1:72;
0 in dom Ma by COMPOS_1:60;
then
A5: Ma. 0 = P.0 by A2,GRFUNC_1:2;
A6: (P)/.IC s
= P.IC s by PBOOLE:143;
A7: Comput(P,s,0+1) = Following(P,Comput(P,s,0)) by EXTPRO_1:3
.= Exec((f,a):=b, s) by A4,A5,A6,COMPOS_1:58;
1 in dom Ma by COMPOS_1:60;
then Ma. 1 = P.1 by A2,GRFUNC_1:2;
then
A8: P.1 = halt SCM+FSA by COMPOS_1:59;
IC Exec((f,a):=b, s) = 0+1 by A4,SCMFSA_2:73;
then
A9: CurInstr(P,Comput(P,s,1)) = halt SCM+FSA by A8,A7,PBOOLE:143;
per cases by NAT_1:14;
suppose
k = 0;
hence thesis;
end;
suppose
A10: 1 <= k;
Comput(P,s,1).intloc 0 = s.intloc 0 by A7,SCMFSA_2:73;
hence thesis by A9,A10,EXTPRO_1:5;
end;
end;
end;
end;
registration
let a be Int-Location, f be FinSeq-Location;
cluster f :=<0,...,0> a -> keeping_0;
coherence
proof
thus (f:=<0,...,0>a) is keeping_0
proof
set Ma = Macro (f:=<0,...,0>a);
let s be 0-started State of SCM+FSA;
A1: Start-At(0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA;
assume
A2: Ma c= P;
let k be Nat;
A3: IC SCM+FSA in dom SA0 by TARSKI:def 1;
A4: IC s = SA0.IC SCM+FSA by A3,A1,GRFUNC_1:2
.= 0 by FUNCOP_1:72;
0 in dom Ma by COMPOS_1:60;
then
A5: Ma. 0 = P.0 by A2,GRFUNC_1:2;
A6: (P)/.IC s
= P.IC s by PBOOLE:143;
A7: Comput(P,s,0+1) = Following(P,Comput(P,s,0)) by EXTPRO_1:3
.= Exec(f:=<0,...,0>a, s) by A4,A5,A6,COMPOS_1:58;
1 in dom Ma by COMPOS_1:60;
then Ma. 1 = P.1 by A2,GRFUNC_1:2;
then
A8: P.1 = halt SCM+FSA by COMPOS_1:59;
IC Exec(f:=<0,...,0>a, s) = 0+1 by A4,SCMFSA_2:75;
then
A9: CurInstr(P,Comput(P,s,1)) = halt SCM+FSA by A8,A7,PBOOLE:143;
per cases by NAT_1:14;
suppose
k = 0;
hence thesis;
end;
suppose
A10: 1 <= k;
Comput(P,s,1).intloc 0 = s.intloc 0 by A7,SCMFSA_2:75;
hence thesis by A9,A10,EXTPRO_1:5;
end;
end;
end;
end;
registration
let a be read-write Int-Location, b be Int-Location;
cluster a := b -> keeping_0;
coherence
proof
set Ma = Macro (a:=b);
let s be 0-started State of SCM+FSA;
A1: Start-At(0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA;
assume
A2: Ma c= P;
let k be Nat;
A3: IC SCM+FSA in dom SA0 by TARSKI:def 1;
A4: IC s = SA0.IC SCM+FSA by A3,A1,GRFUNC_1:2
.= 0 by FUNCOP_1:72;
0 in dom Ma by COMPOS_1:60;
then
A5: Ma. 0 = P.0 by A2,GRFUNC_1:2;
A6: (P)/.IC s
= P.IC s by PBOOLE:143;
A7: Comput(P,s,0+1) = Following(P,Comput(P,s,0)) by EXTPRO_1:3
.= Exec(a:=b, s) by A4,A5,A6,COMPOS_1:58;
1 in dom Ma by COMPOS_1:60;
then Ma. 1 = P.1 by A2,GRFUNC_1:2;
then
A8: P.1 = halt SCM+FSA by COMPOS_1:59;
IC Exec(a:=b, s) = 0+1 by A4,SCMFSA_2:63;
then
A9: CurInstr(P,Comput(P,s,1))
= halt SCM+FSA by A8,A7,PBOOLE:143;
per cases by NAT_1:14;
suppose
k = 0;
hence thesis;
end;
suppose
A10: 1 <= k;
Comput(P,s,1).intloc 0 = s.intloc 0 by A7,SCMFSA_2:63;
hence thesis by A9,A10,EXTPRO_1:5;
end;
end;
cluster AddTo(a, b) -> keeping_0;
coherence
proof
set Ma = Macro (AddTo(a,b));
let s be 0-started State of SCM+FSA;
A11: Start-At(0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA;
assume
A12: Ma c= P;
let k be Nat;
A13: IC SCM+FSA in dom SA0 by TARSKI:def 1;
A14: IC s = SA0.IC SCM+FSA by A13,A11,GRFUNC_1:2
.= 0 by FUNCOP_1:72;
0 in dom Ma by COMPOS_1:60;
then
A15: Ma. 0 = P.0 by A12,GRFUNC_1:2;
A16: (P)/.IC s
= P.IC s by PBOOLE:143;
A17: Comput(P,s,0+1) = Following(P,Comput(P,s,0)) by EXTPRO_1:3
.= Exec(AddTo(a,b), s) by A14,A15,A16,COMPOS_1:58;
1 in dom Ma by COMPOS_1:60;
then Ma. 1 = P.1 by A12,GRFUNC_1:2;
then
A18: P.1 = halt SCM+FSA by COMPOS_1:59;
IC Exec(AddTo(a,b), s) = 0+1 by A14,SCMFSA_2:64;
then
A19: CurInstr(P,Comput(P,s,1)) = halt SCM+FSA by A18,A17,PBOOLE:143;
per cases by NAT_1:14;
suppose
k = 0;
hence thesis;
end;
suppose
A20: 1 <= k;
Comput(P,s,1).intloc 0 = s.intloc 0 by A17,SCMFSA_2:64;
hence thesis by A19,A20,EXTPRO_1:5;
end;
end;
cluster SubFrom(a, b) -> keeping_0;
coherence
proof
set Ma = Macro (SubFrom(a,b));
let s be 0-started State of SCM+FSA;
A21: Start-At(0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA;
assume
A22: Ma c= P;
let k be Nat;
A23: IC SCM+FSA in dom SA0 by TARSKI:def 1;
A24: IC s = SA0.IC SCM+FSA by A23,A21,GRFUNC_1:2
.= 0 by FUNCOP_1:72;
0 in dom Ma by COMPOS_1:60;
then
A25: Ma. 0 = P.0 by A22,GRFUNC_1:2;
A26: (P)/.IC s
= P.IC s by PBOOLE:143;
A27: Comput(P,s,0+1) = Following(P,Comput(P,s,0)) by EXTPRO_1:3
.= Exec(SubFrom(a,b), s) by A24,A25,A26,COMPOS_1:58;
1 in dom Ma by COMPOS_1:60;
then Ma. 1 = P.1 by A22,GRFUNC_1:2;
then
A28: P.1 = halt SCM+FSA by COMPOS_1:59;
IC Exec(SubFrom(a,b), s) = 0+1 by A24,SCMFSA_2:65;
then
A29: CurInstr(P,Comput(P,s,1)) = halt SCM+FSA by A28,A27,PBOOLE:143;
per cases by NAT_1:14;
suppose
k = 0;
hence thesis;
end;
suppose
A30: 1 <= k;
Comput(P,s,1).intloc 0 = s.intloc 0 by A27,SCMFSA_2:65;
hence thesis by A29,A30,EXTPRO_1:5;
end;
end;
cluster MultBy(a, b) -> keeping_0;
coherence
proof
set Ma = Macro (MultBy(a,b));
let s be 0-started State of SCM+FSA;
A31: Start-At(0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA;
assume
A32: Ma c= P;
let k be Nat;
A33: IC SCM+FSA in dom SA0 by TARSKI:def 1;
A34: IC s = SA0.IC SCM+FSA by A33,A31,GRFUNC_1:2
.= 0 by FUNCOP_1:72;
0 in dom Ma by COMPOS_1:60;
then
A35: Ma. 0 = P.0 by A32,GRFUNC_1:2;
A36: (P)/.IC s
= P.IC s by PBOOLE:143;
A37: Comput(P,s,0+1) = Following(P,Comput(P,s,0)) by EXTPRO_1:3
.= Exec(MultBy(a,b), s) by A34,A35,A36,COMPOS_1:58;
1 in dom Ma by COMPOS_1:60;
then Ma. 1 = P.1 by A32,GRFUNC_1:2;
then
A38: P.1 = halt SCM+FSA by COMPOS_1:59;
IC Exec(MultBy(a,b), s) = 0+1 by A34,SCMFSA_2:66;
then
A39: CurInstr(P,Comput(P,s,1)) = halt SCM+FSA by A38,A37,PBOOLE:143;
per cases by NAT_1:14;
suppose
k = 0;
hence thesis;
end;
suppose
A40: 1 <= k;
Comput(P,s,1).intloc 0 = s.intloc 0 by A37,SCMFSA_2:66;
hence thesis by A39,A40,EXTPRO_1:5;
end;
end;
end;
registration
cluster keeping_0 sequential for Instruction of SCM+FSA;
existence
proof
take i = (the read-write Int-Location) := intloc 1;
thus i is keeping_0;
thus thesis;
end;
end;
registration
let i be keeping_0 Instruction of SCM+FSA;
cluster Macro i -> keeping_0;
coherence by Def1;
end;
registration
let a, b be read-write Int-Location;
cluster Divide(a, b) -> keeping_0;
coherence
proof
set Ma = Macro (Divide(a,b));
let s be 0-started State of SCM+FSA;
A1: Start-At(0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA;
assume
A2: Ma c= P;
let k be Nat;
A3: IC SCM+FSA in dom SA0 by TARSKI:def 1;
A4: IC s = SA0.IC SCM+FSA by A3,A1,GRFUNC_1:2
.= 0 by FUNCOP_1:72;
0 in dom Ma by COMPOS_1:60;
then
A5: Ma. 0 = P.0 by A2,GRFUNC_1:2;
A6: (P)/.IC s
= P.IC s by PBOOLE:143;
A7: Comput(P,s,0+1) = Following(P,Comput(P,s,0)) by EXTPRO_1:3
.= Exec(Divide(a,b), s) by A4,A5,A6,COMPOS_1:58;
1 in dom Ma by COMPOS_1:60;
then Ma. 1 = P.1 by A2,GRFUNC_1:2;
then
A8: P.1 = halt SCM+FSA by COMPOS_1:59;
IC Exec(Divide(a,b), s) = 0+1 by A4,SCMFSA_2:67;
then
A9: CurInstr(P,Comput(P,s,1)) = halt SCM+FSA by A8,A7,PBOOLE:143;
per cases by NAT_1:14;
suppose
k = 0;
hence thesis;
end;
suppose
A10: 1 <= k;
Comput(P,s,1).intloc 0 = s.intloc 0 by A7,SCMFSA_2:67;
hence thesis by A9,A10,EXTPRO_1:5;
end;
end;
end;
registration
let a be Int-Location, f be FinSeq-Location, b be read-write Int-Location;
cluster b := (f,a) -> keeping_0;
coherence
proof
set Ma = Macro (b:=(f,a));
let s be 0-started State of SCM+FSA;
A1: Start-At(0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA;
assume
A2: Ma c= P;
let k be Nat;
A3: IC SCM+FSA in dom SA0 by TARSKI:def 1;
A4: IC s = SA0.IC SCM+FSA by A3,A1,GRFUNC_1:2
.= 0 by FUNCOP_1:72;
0 in dom Ma by COMPOS_1:60;
then
A5: Ma. 0 = P.0 by A2,GRFUNC_1:2;
A6: (P)/.IC s
= P.IC s by PBOOLE:143;
A7: Comput(P,s,0+1) = Following(P,Comput(P,s,0)) by EXTPRO_1:3
.= Exec(b:=(f,a), s) by A4,A5,A6,COMPOS_1:58;
1 in dom Ma by COMPOS_1:60;
then Ma. 1 = P.1 by A2,GRFUNC_1:2;
then
A8: P.1 = halt SCM+FSA by COMPOS_1:59;
IC Exec(b:=(f,a), s) = 0+1 by A4,SCMFSA_2:72;
then
A9: CurInstr(P,Comput(P,s,1)) = halt SCM+FSA by A8,A7,PBOOLE:143;
per cases by NAT_1:14;
suppose
k = 0;
hence thesis;
end;
suppose
A10: 1 <= k;
Comput(P,s,1).intloc 0 = s.intloc 0 by A7,SCMFSA_2:72;
hence thesis by A9,A10,EXTPRO_1:5;
end;
end;
end;
registration
let f be FinSeq-Location, b be read-write Int-Location;
cluster b :=len f -> keeping_0;
coherence
proof
set Ma = Macro (b:=len f);
let s be 0-started State of SCM+FSA;
A1: Start-At(0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA;
assume
A2: Ma c= P;
let k be Nat;
A3: IC SCM+FSA in dom SA0 by TARSKI:def 1;
A4: IC s = SA0.IC SCM+FSA by A3,A1,GRFUNC_1:2
.= 0 by FUNCOP_1:72;
0 in dom Ma by COMPOS_1:60;
then
A5: Ma. 0 = P.0 by A2,GRFUNC_1:2;
A6: (P)/.IC s = P.IC s by PBOOLE:143;
A7: Comput(P,s,0+1) = Following(P,Comput(P,s,0)) by EXTPRO_1:3
.= Exec(b:=len f, s) by A4,A5,A6,COMPOS_1:58;
1 in dom Ma by COMPOS_1:60;
then Ma. 1 = P.1 by A2,GRFUNC_1:2;
then
A8: P.1 = halt SCM+FSA by COMPOS_1:59;
IC Exec(b:=len f, s) = 0+1 by A4,SCMFSA_2:74;
then
A9: CurInstr(P,Comput(P,s,1)) = halt SCM+FSA by A8,A7,PBOOLE:143;
per cases by NAT_1:14;
suppose
k = 0;
hence thesis;
end;
suppose
A10: 1 <= k;
Comput(P,s,1).intloc 0 = s.intloc 0 by A7,SCMFSA_2:74;
hence thesis by A9,A10,EXTPRO_1:5;
end;
end;
end;
registration
let i be sequential Instruction of SCM+FSA;
cluster Macro i -> really-closed;
coherence
proof set F = Macro i;
let l be Nat;
A1: dom F = {0,1} by COMPOS_1:61;
assume
A2: l in dom F;
then per cases by COMPOS_1:60;
suppose
A3: l = 0;
then F/.l = F.0 by A2,PARTFUN1:def 6
.= i by COMPOS_1:58;
then NIC (F/.l, l) = {0 + 1} by A3,AMISTD_1:12;
hence NIC (F/.l, l) c= dom F by A1,ZFMISC_1:7;
end;
suppose
A4: l = 1;
then F/.l = F.1 by A2,PARTFUN1:def 6
.= halt SCM+FSA by COMPOS_1:59;
then NIC (F/.l, l) = {1} by A4,AMISTD_1:2;
hence NIC (F/.l, l) c= dom F by A1,ZFMISC_1:7;
end;
end;
end;
:: registration
:: let i be keeping_0 Instruction of SCM+FSA;
:: cluster Macro i -> really-closed;
:: coherence;
:: end;
registration let i be sequential Instruction of SCM+FSA, J be
parahalting really-closed Program of SCM+FSA; cluster i ";" J ->
parahalting really-closed; coherence; end;
registration
let I be parahalting really-closed Program of SCM+FSA,
j be sequential Instruction of SCM+FSA;
cluster I ";" j -> parahalting really-closed;
coherence;
end;
registration
let i,j be sequential Instruction of SCM+FSA;
cluster i ";" j -> parahalting really-closed;
coherence;
end;
registration
let i be keeping_0 sequential Instruction of SCM+FSA,
J be keeping_0 really-closed Program of SCM+FSA;
cluster i ";" J -> keeping_0;
coherence;
end;
registration
let I be keeping_0 really-closed Program of SCM+FSA,
j be keeping_0 sequential Instruction of SCM+FSA;
cluster I ";" j -> keeping_0;
coherence;
end;
registration
let i, j be keeping_0 sequential Instruction of SCM+FSA;
cluster i ";" j -> keeping_0;
coherence;
end;
begin :: Consequenses of the main theorem
::$CT
theorem Th3:
DataPart s1 = DataPart s2 implies DataPart Exec (i, s1) =
DataPart Exec (i, s2)
proof
assume
A1: DataPart s1 = DataPart s2;
set l = i;
A2: dom Exec(l,s1) = the carrier of SCM+FSA by PARTFUN1:def 2;
then
A3: dom Exec(l,s1) = dom Exec(l,s2) by PARTFUN1:def 2;
A4: dom ((Exec (l,s1)) | (Data-Locations SCM+FSA)) = (
Data-Locations SCM+FSA) by A2,RELAT_1:62;
A5: dom Exec(l,s2) = the carrier of SCM+FSA by PARTFUN1:def 2;
then
A6: dom ((Exec (l,s2)) | (Data-Locations SCM+FSA)) = (
Data-Locations SCM+FSA) by RELAT_1:62;
InsCode i = 0 or ... or InsCode i = 12 by NAT_1:60,SCMFSA_2:16;
then per cases;
suppose
InsCode i = 0;
then
A7: i = halt SCM+FSA by SCMFSA_2:95;
then Exec (i,s1) = s1 by EXTPRO_1:def 3;
hence thesis by A1,A7,EXTPRO_1:def 3;
end;
suppose
InsCode i = 1;
then consider db,da being Int-Location such that
A8: l = db := da by SCMFSA_2:30;
A9: for x being object st x in ((Data-Locations SCM+FSA) \ {db})
holds (Exec (l,s1) | (Data-Locations SCM+FSA \ {db})).x = (Exec (l,
s2) | (Data-Locations SCM+FSA \ {db})).x
proof
let x be object;
assume
A10: x in ((Data-Locations SCM+FSA) \ {db});
then
A11: x in Data-Locations SCM+FSA by XBOOLE_0:def 5;
A12: not x in {db} by A10,XBOOLE_0:def 5;
per cases by A11,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in Int-Locations;
then reconsider a = x as Int-Location by AMI_2:def 16;
A13: a <> db by A12,TARSKI:def 1;
thus (Exec (l,s1) | (Data-Locations SCM+FSA \ {db})).x = (
Exec (l,s1)).a by A10,FUNCT_1:49
.= s1.a by A8,A13,SCMFSA_2:63
.= (DataPart s1).a by A11,FUNCT_1:49
.= s2.a by A1,A11,FUNCT_1:49
.= (Exec (l,s2)).a by A8,A13,SCMFSA_2:63
.= (Exec (l,s2) | (Data-Locations SCM+FSA \ {db})).x by A10,
FUNCT_1:49;
end;
suppose
x in FinSeq-Locations;
then reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;
thus (Exec (l,s1) | (Data-Locations SCM+FSA \ {db})).x = (
Exec (l,s1)).a by A10,FUNCT_1:49
.= s1.a by A8,SCMFSA_2:63
.= (DataPart s1).a by A11,FUNCT_1:49
.= s2.a by A1,A11,FUNCT_1:49
.= (Exec (l,s2)).a by A8,SCMFSA_2:63
.= (Exec (l,s2) | (Data-Locations SCM+FSA \ {db})).x by A10,
FUNCT_1:49;
end;
end;
A14: dom ((Exec (l,s2)) | (Data-Locations SCM+FSA \ {db})) = (
Data-Locations SCM+FSA \ {db}) by A5,RELAT_1:62;
dom ((Exec (l,s1)) | (Data-Locations SCM+FSA \ {db})) = (
Data-Locations SCM+FSA \ {db}) by A2,RELAT_1:62;
then
A15: Exec (l,s1) | (Data-Locations SCM+FSA \ {db} ) = Exec (l,
s2) | (Data-Locations SCM+FSA \ {db} ) by A14,A9,FUNCT_1:2;
db in Int-Locations by AMI_2:def 16;
then db in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then
A16: Data-Locations SCM+FSA = Data-Locations SCM+FSA
\/ {db} by ZFMISC_1:40
.= (Data-Locations SCM+FSA \ {db} ) \/ {db} by XBOOLE_1:39;
A17: Exec(l, s2).db = s2.da by A8,SCMFSA_2:63;
A18: Exec(l, s1).db = s1.da by A8,SCMFSA_2:63;
da in Int-Locations by AMI_2:def 16;
then
A19: da in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then s1.da = (DataPart s1).da by FUNCT_1:49
.= s2.da by A1,A19,FUNCT_1:49;
then Exec (l,s1) | {db} = Exec(l,s2) | {db} by A3,A18,A17,GRFUNC_1:29;
hence thesis by A16,A15,RELAT_1:150;
end;
suppose
InsCode i = 2;
then consider db,da being Int-Location such that
A20: l = AddTo(db,da) by SCMFSA_2:31;
A21: for x being object st x in ((Data-Locations SCM+FSA) \ {db})
holds (Exec (l,s1) | (Data-Locations SCM+FSA \ {db})).x = (Exec (l,
s2) | (Data-Locations SCM+FSA \ {db})).x
proof
let x be object;
assume
A22: x in ((Data-Locations SCM+FSA) \ {db});
then
A23: x in Data-Locations SCM+FSA by XBOOLE_0:def 5;
A24: not x in {db} by A22,XBOOLE_0:def 5;
per cases by A23,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in Int-Locations;
then reconsider a = x as Int-Location by AMI_2:def 16;
A25: a <> db by A24,TARSKI:def 1;
thus (Exec (l,s1) | (Data-Locations SCM+FSA \ {db})).x = (
Exec (l,s1)).a by A22,FUNCT_1:49
.= s1.a by A20,A25,SCMFSA_2:64
.= (DataPart s1).a by A23,FUNCT_1:49
.= s2.a by A1,A23,FUNCT_1:49
.= (Exec (l,s2)).a by A20,A25,SCMFSA_2:64
.= (Exec (l,s2) | (Data-Locations SCM+FSA \ {db})).x by A22,
FUNCT_1:49;
end;
suppose
x in FinSeq-Locations;
then reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;
thus (Exec (l,s1) | (Data-Locations SCM+FSA \ {db})).x = (
Exec (l,s1)).a by A22,FUNCT_1:49
.= s1.a by A20,SCMFSA_2:64
.= (DataPart s1).a by A23,FUNCT_1:49
.= s2.a by A1,A23,FUNCT_1:49
.= (Exec (l,s2)).a by A20,SCMFSA_2:64
.= (Exec (l,s2) | (Data-Locations SCM+FSA \ {db})).x by A22,
FUNCT_1:49;
end;
end;
A26: dom ((Exec (l,s2)) | (Data-Locations SCM+FSA \ {db})) = (
Data-Locations SCM+FSA \ {db}) by A5,RELAT_1:62;
dom ((Exec (l,s1)) | (Data-Locations SCM+FSA \ {db})) = (
Data-Locations SCM+FSA \ {db}) by A2,RELAT_1:62;
then
A27: Exec (l,s1) | (Data-Locations SCM+FSA \ {db} ) = Exec (l,
s2) | (Data-Locations SCM+FSA \ {db} ) by A26,A21,FUNCT_1:2;
db in Int-Locations by AMI_2:def 16;
then db in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then
A28: Data-Locations SCM+FSA = Data-Locations SCM+FSA
\/ {db} by ZFMISC_1:40
.= (Data-Locations SCM+FSA \ {db} ) \/ {db} by XBOOLE_1:39;
A29: Exec(l, s2).db = s2.db + s2.da by A20,SCMFSA_2:64;
A30: Exec(l, s1).db = s1.db + s1.da by A20,SCMFSA_2:64;
db in Int-Locations by AMI_2:def 16;
then
A31: db in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then
A32: s1.db = (DataPart s1).db by FUNCT_1:49
.= s2.db by A1,A31,FUNCT_1:49;
da in Int-Locations by AMI_2:def 16;
then
A33: da in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then s1.da = (DataPart s1).da by FUNCT_1:49
.= s2.da by A1,A33,FUNCT_1:49;
then Exec (l,s1) | {db} = Exec(l,s2) | {db} by A3,A30,A29,A32,GRFUNC_1:29;
hence thesis by A28,A27,RELAT_1:150;
end;
suppose
InsCode i = 3;
then consider db,da being Int-Location such that
A34: l = SubFrom(db,da) by SCMFSA_2:32;
A35: for x being object st x in ((Data-Locations SCM+FSA) \ {db})
holds (Exec (l,s1) | (Data-Locations SCM+FSA \ {db})).x = (Exec (l,
s2) | (Data-Locations SCM+FSA \ {db})).x
proof
let x be object;
assume
A36: x in ((Data-Locations SCM+FSA) \ {db});
then
A37: x in Data-Locations SCM+FSA by XBOOLE_0:def 5;
A38: not x in {db} by A36,XBOOLE_0:def 5;
per cases by A37,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in Int-Locations;
then reconsider a = x as Int-Location by AMI_2:def 16;
A39: a <> db by A38,TARSKI:def 1;
thus (Exec (l,s1) | (Data-Locations SCM+FSA \ {db})).x = (
Exec (l,s1)).a by A36,FUNCT_1:49
.= s1.a by A34,A39,SCMFSA_2:65
.= (DataPart s1).a by A37,FUNCT_1:49
.= s2.a by A1,A37,FUNCT_1:49
.= (Exec (l,s2)).a by A34,A39,SCMFSA_2:65
.= (Exec (l,s2) | (Data-Locations SCM+FSA \ {db})).x by A36,
FUNCT_1:49;
end;
suppose
x in FinSeq-Locations;
then reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;
thus (Exec (l,s1) | (Data-Locations SCM+FSA \ {db})).x = (
Exec (l,s1)).a by A36,FUNCT_1:49
.= s1.a by A34,SCMFSA_2:65
.= (DataPart s1).a by A37,FUNCT_1:49
.= s2.a by A1,A37,FUNCT_1:49
.= (Exec (l,s2)).a by A34,SCMFSA_2:65
.= (Exec (l,s2) | (Data-Locations SCM+FSA \ {db})).x by A36,
FUNCT_1:49;
end;
end;
A40: dom ((Exec (l,s2)) | (Data-Locations SCM+FSA \ {db})) = (
Data-Locations SCM+FSA \ {db}) by A5,RELAT_1:62;
dom ((Exec (l,s1)) | (Data-Locations SCM+FSA \ {db})) = (
Data-Locations SCM+FSA \ {db}) by A2,RELAT_1:62;
then
A41: Exec (l,s1) | (Data-Locations SCM+FSA \ {db} ) = Exec (l,
s2) | (Data-Locations SCM+FSA \ {db} ) by A40,A35,FUNCT_1:2;
db in Int-Locations by AMI_2:def 16;
then db in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then
A42: Data-Locations SCM+FSA = Data-Locations SCM+FSA
\/ {db} by ZFMISC_1:40
.= (Data-Locations SCM+FSA \ {db} ) \/ {db} by XBOOLE_1:39;
A43: Exec(l, s2).db = s2.db - s2.da by A34,SCMFSA_2:65;
A44: Exec(l, s1).db = s1.db - s1.da by A34,SCMFSA_2:65;
db in Int-Locations by AMI_2:def 16;
then
A45: db in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then
A46: s1.db = (DataPart s1).db by FUNCT_1:49
.= s2.db by A1,A45,FUNCT_1:49;
da in Int-Locations by AMI_2:def 16;
then
A47: da in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then s1.da = (DataPart s1).da by FUNCT_1:49
.= s2.da by A1,A47,FUNCT_1:49;
then Exec (l,s1) | {db} = Exec(l,s2) | {db} by A3,A44,A43,A46,GRFUNC_1:29;
hence thesis by A42,A41,RELAT_1:150;
end;
suppose
InsCode i = 4;
then consider db,da being Int-Location such that
A48: l = MultBy(db,da) by SCMFSA_2:33;
A49: for x being object st x in ((Data-Locations SCM+FSA) \ {db})
holds (Exec (l,s1) | (Data-Locations SCM+FSA \ {db})).x = (Exec (l,
s2) | (Data-Locations SCM+FSA \ {db})).x
proof
let x be object;
assume
A50: x in ((Data-Locations SCM+FSA) \ {db});
then
A51: x in Data-Locations SCM+FSA by XBOOLE_0:def 5;
A52: not x in {db} by A50,XBOOLE_0:def 5;
per cases by A51,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in Int-Locations;
then reconsider a = x as Int-Location by AMI_2:def 16;
A53: a <> db by A52,TARSKI:def 1;
thus (Exec (l,s1) | (Data-Locations SCM+FSA \ {db})).x = (
Exec (l,s1)).a by A50,FUNCT_1:49
.= s1.a by A48,A53,SCMFSA_2:66
.= (DataPart s1).a by A51,FUNCT_1:49
.= s2.a by A1,A51,FUNCT_1:49
.= (Exec (l,s2)).a by A48,A53,SCMFSA_2:66
.= (Exec (l,s2) | (Data-Locations SCM+FSA \ {db})).x by A50,
FUNCT_1:49;
end;
suppose
x in FinSeq-Locations;
then reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;
thus (Exec (l,s1) | (Data-Locations SCM+FSA \ {db})).x = (
Exec (l,s1)).a by A50,FUNCT_1:49
.= s1.a by A48,SCMFSA_2:66
.= (DataPart s1).a by A51,FUNCT_1:49
.= s2.a by A1,A51,FUNCT_1:49
.= (Exec (l,s2)).a by A48,SCMFSA_2:66
.= (Exec (l,s2) | (Data-Locations SCM+FSA \ {db})).x by A50,
FUNCT_1:49;
end;
end;
A54: dom ((Exec (l,s2)) | (Data-Locations SCM+FSA \ {db})) = (
Data-Locations SCM+FSA \ {db}) by A5,RELAT_1:62;
dom ((Exec (l,s1)) | (Data-Locations SCM+FSA \ {db})) = (
Data-Locations SCM+FSA \ {db}) by A2,RELAT_1:62;
then
A55: Exec (l,s1) | (Data-Locations SCM+FSA \ {db} ) = Exec (l,
s2) | (Data-Locations SCM+FSA \ {db} ) by A54,A49,FUNCT_1:2;
db in Int-Locations by AMI_2:def 16;
then db in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then
A56: Data-Locations SCM+FSA = Data-Locations SCM+FSA
\/ {db} by ZFMISC_1:40
.= (Data-Locations SCM+FSA \ {db} ) \/ {db} by XBOOLE_1:39;
A57: Exec(l, s2).db = s2.db * s2.da by A48,SCMFSA_2:66;
A58: Exec(l, s1).db = s1.db * s1.da by A48,SCMFSA_2:66;
db in Int-Locations by AMI_2:def 16;
then
A59: db in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then
A60: s1.db = (DataPart s1).db by FUNCT_1:49
.= s2.db by A1,A59,FUNCT_1:49;
da in Int-Locations by AMI_2:def 16;
then
A61: da in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then s1.da = (DataPart s1).da by FUNCT_1:49
.= s2.da by A1,A61,FUNCT_1:49;
then Exec (l,s1) | {db} = Exec(l,s2) | {db} by A3,A58,A57,A60,GRFUNC_1:29;
hence thesis by A56,A55,RELAT_1:150;
end;
suppose
InsCode i = 5;
then consider db,da being Int-Location such that
A62: l = Divide(db,da) by SCMFSA_2:34;
hereby
per cases;
suppose
A63: da <> db;
A64: for x being object st x in ((Data-Locations SCM+FSA) \ {
db,da} ) holds (Exec (l,s1) | (Data-Locations SCM+FSA \ {db,da})).x
= (Exec (l,s2) | (Data-Locations SCM+FSA \ {db,da})).x
proof
let x be object;
assume
A65: x in ((Data-Locations SCM+FSA) \ {db,da});
then
A66: x in Data-Locations SCM+FSA by XBOOLE_0:def 5;
A67: not x in {db,da} by A65,XBOOLE_0:def 5;
per cases by A66,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in Int-Locations;
then reconsider a = x as Int-Location by AMI_2:def 16;
A68: a <> da by A67,TARSKI:def 2;
A69: a <> db by A67,TARSKI:def 2;
thus (Exec (l,s1) | (Data-Locations SCM+FSA \ {db,da}))
.x = (Exec (l,s1)).a by A65,FUNCT_1:49
.= s1.a by A62,A68,A69,SCMFSA_2:67
.= (DataPart s1).a by A66,FUNCT_1:49
.= s2.a by A1,A66,FUNCT_1:49
.= (Exec (l,s2)).a by A62,A68,A69,SCMFSA_2:67
.= (Exec (l,s2) | (Data-Locations SCM+FSA \ {db,da}
)).x by A65,FUNCT_1:49;
end;
suppose
x in FinSeq-Locations;
then reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;
thus (Exec (l,s1) | (Data-Locations SCM+FSA \ {db,da}))
.x = (Exec (l,s1)).a by A65,FUNCT_1:49
.= s1.a by A62,SCMFSA_2:67
.= (DataPart s1).a by A66,FUNCT_1:49
.= s2.a by A1,A66,FUNCT_1:49
.= (Exec (l,s2)).a by A62,SCMFSA_2:67
.= (Exec (l,s2) | (Data-Locations SCM+FSA \ {db,da}
)).x by A65,FUNCT_1:49;
end;
end;
A70: dom ((Exec (l,s2)) | (Data-Locations SCM+FSA \ {db,da
})) = (Data-Locations SCM+FSA \ {db,da}) by A5,RELAT_1:62;
dom ((Exec (l,s1)) | (Data-Locations SCM+FSA \ {db,da
})) = (Data-Locations SCM+FSA \ {db,da}) by A2,RELAT_1:62;
then
A71: Exec (l,s1) | (Data-Locations SCM+FSA \ {db,da} ) =
Exec (l,s2) | (Data-Locations SCM+FSA \ {db,da} ) by A70,A64,FUNCT_1:2;
A72: Exec(l, s2).da = s2.db mod s2.da by A62,SCMFSA_2:67;
db in Int-Locations by AMI_2:def 16;
then
A73: db in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then
A74: s1.db = (DataPart s1).db by FUNCT_1:49
.= s2.db by A1,A73,FUNCT_1:49;
da in Int-Locations by AMI_2:def 16;
then
A75: da in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
db in Int-Locations by AMI_2:def 16;
then db in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then
A76: Data-Locations SCM+FSA
= Data-Locations SCM+FSA \/ {db,da} by A75,ZFMISC_1:42
.= (Data-Locations SCM+FSA \ {db,da} ) \/ {db,da} by XBOOLE_1:39;
A77: Exec(l, s1).da = s1.db mod s1.da by A62,SCMFSA_2:67;
A78: Exec(l, s2).db = s2.db div s2.da by A62,A63,SCMFSA_2:67;
A79: Exec(l, s1).db = s1.db div s1.da by A62,A63,SCMFSA_2:67;
da in Int-Locations by AMI_2:def 16;
then
A80: da in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then s1.da = (DataPart s1).da by FUNCT_1:49
.= s2.da by A1,A80,FUNCT_1:49;
then Exec (l,s1) | {db,da} = Exec(l,s2) | {db,da} by A3,A79,A77,A78,A72
,A74,GRFUNC_1:30;
hence thesis by A76,A71,RELAT_1:150;
end;
suppose
A81: da = db;
A82: for x being object st x in ((Data-Locations SCM+FSA) \ {
db}) holds (Exec (l,s1) | (Data-Locations SCM+FSA \ {db})).x = (Exec
(l,s2) | (Data-Locations SCM+FSA \ {db})).x
proof
let x be object;
assume
A83: x in ((Data-Locations SCM+FSA) \ {db});
then
A84: x in Data-Locations SCM+FSA by XBOOLE_0:def 5;
A85: not x in {db} by A83,XBOOLE_0:def 5;
per cases by A84,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in Int-Locations;
then reconsider a = x as Int-Location by AMI_2:def 16;
A86: a <> db by A85,TARSKI:def 1;
thus (Exec (l,s1) | (Data-Locations SCM+FSA \ {db})).x
= (Exec (l,s1)).a by A83,FUNCT_1:49
.= s1.a by A62,A81,A86,SCMFSA_2:68
.= (DataPart s1).a by A84,FUNCT_1:49
.= s2.a by A1,A84,FUNCT_1:49
.= (Exec (l,s2)).a by A62,A81,A86,SCMFSA_2:68
.= (Exec (l,s2) | (Data-Locations SCM+FSA \ {db})).
x by A83,FUNCT_1:49;
end;
suppose
x in FinSeq-Locations;
then reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;
thus (Exec (l,s1) | (Data-Locations SCM+FSA \ {db})).x
= (Exec (l,s1)).a by A83,FUNCT_1:49
.= s1.a by A62,A81,SCMFSA_2:68
.= (s1 | (Data-Locations SCM+FSA)).a by A84,FUNCT_1:49
.= s2.a by A1,A84,FUNCT_1:49
.= (Exec (l,s2)).a by A62,A81,SCMFSA_2:68
.= (Exec (l,s2) | (Data-Locations SCM+FSA \ {db})).
x by A83,FUNCT_1:49;
end;
end;
A87: dom ((Exec (l,s2)) | (Data-Locations SCM+FSA \ {db}))
= (Data-Locations SCM+FSA \ {db}) by A5,RELAT_1:62;
dom ((Exec (l,s1)) | (Data-Locations SCM+FSA \ {db}))
= (Data-Locations SCM+FSA \ {db}) by A2,RELAT_1:62;
then
A88: Exec (l,s1) | (Data-Locations SCM+FSA \ {db} ) = Exec
(l,s2) | (Data-Locations SCM+FSA \ {db} ) by A87,A82,FUNCT_1:2;
db in Int-Locations by AMI_2:def 16;
then db in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then
A89: Data-Locations SCM+FSA = Data-Locations SCM+FSA \/ {db} by ZFMISC_1:40
.= (Data-Locations SCM+FSA \ {db} ) \/ {db} by XBOOLE_1:39;
A90: Exec(l, s2).db = s2.db mod s2.da by A62,A81,SCMFSA_2:68;
A91: Exec(l, s1).db = s1.db mod s1.da by A62,A81,SCMFSA_2:68;
db in Int-Locations by AMI_2:def 16;
then
A92: db in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then
A93: s1.db = (DataPart s1).db by FUNCT_1:49
.= s2.db by A1,A92,FUNCT_1:49;
da in Int-Locations by AMI_2:def 16;
then
A94: da in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then s1.da = (DataPart s1).da by FUNCT_1:49
.= s2.da by A1,A94,FUNCT_1:49;
then Exec (l,s1) | {db} = Exec(l,s2) | {db} by A3,A91,A90,A93,
GRFUNC_1:29;
hence thesis by A89,A88,RELAT_1:150;
end;
end;
end;
suppose
InsCode i = 6;
then
A95: ex l1 st i = goto l1 by SCMFSA_2:35;
for x being object st x in ((Data-Locations SCM+FSA)) holds
(DataPart Exec (l,s1)).x = (DataPart Exec (l,s2)).x
proof
let x be object;
assume
A96: x in ((Data-Locations SCM+FSA));
per cases by A96,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in Int-Locations;
then reconsider a = x as Int-Location by AMI_2:def 16;
thus (DataPart Exec (l,s1)).x = (Exec (l,s1)).a by A96,FUNCT_1:49
.= s1.a by A95,SCMFSA_2:69
.= (DataPart s1).a by A96,FUNCT_1:49
.= s2.a by A1,A96,FUNCT_1:49
.= (Exec (l,s2)).a by A95,SCMFSA_2:69
.= (DataPart Exec (l,s2)).x by A96,FUNCT_1:49;
end;
suppose
x in FinSeq-Locations;
then reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;
thus (DataPart Exec (l,s1)).x = (Exec (l,s1)).a by A96,FUNCT_1:49
.= s1.a by A95,SCMFSA_2:69
.= (DataPart s1).a by A96,FUNCT_1:49
.= s2.a by A1,A96,FUNCT_1:49
.= (Exec (l,s2)).a by A95,SCMFSA_2:69
.= (DataPart Exec (l,s2)).x by A96,FUNCT_1:49;
end;
end;
hence thesis by A4,A6,FUNCT_1:2;
end;
suppose
InsCode i = 7;
then
A97: ex l1, a st i = a=0_goto l1 by SCMFSA_2:36;
for x being object st x in ((Data-Locations SCM+FSA)) holds
(DataPart Exec (l,s1)).x = (DataPart Exec (l,s2)).x
proof
let x be object;
assume
A98: x in ((Data-Locations SCM+FSA));
per cases by A98,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in Int-Locations;
then reconsider a = x as Int-Location by AMI_2:def 16;
thus (DataPart Exec (l,s1)).x = (Exec (l,s1)).a by A98,FUNCT_1:49
.= s1.a by A97,SCMFSA_2:70
.= (DataPart s1).a by A98,FUNCT_1:49
.= s2.a by A1,A98,FUNCT_1:49
.= (Exec (l,s2)).a by A97,SCMFSA_2:70
.= (DataPart Exec (l,s2)).x by A98,FUNCT_1:49;
end;
suppose
x in FinSeq-Locations;
then reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;
thus (DataPart Exec (l,s1)).x = (Exec (l,s1)).a by A98,FUNCT_1:49
.= s1.a by A97,SCMFSA_2:70
.= (DataPart s1).a by A98,FUNCT_1:49
.= s2.a by A1,A98,FUNCT_1:49
.= (Exec (l,s2)).a by A97,SCMFSA_2:70
.= (DataPart Exec (l,s2)).x by A98,FUNCT_1:49;
end;
end;
hence thesis by A4,A6,FUNCT_1:2;
end;
suppose
InsCode i = 8;
then
A99: ex l1, a st i = a>0_goto l1 by SCMFSA_2:37;
for x being object st x in ((Data-Locations SCM+FSA)) holds
(DataPart Exec (l,s1)).x = (DataPart Exec (l,s2)).x
proof
let x be object;
assume
A100: x in ((Data-Locations SCM+FSA));
per cases by A100,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in Int-Locations;
then reconsider a = x as Int-Location by AMI_2:def 16;
thus (DataPart Exec (l,s1)).x = (Exec (l,s1)).a by A100,FUNCT_1:49
.= s1.a by A99,SCMFSA_2:71
.= (DataPart s1).a by A100,FUNCT_1:49
.= s2.a by A1,A100,FUNCT_1:49
.= (Exec (l,s2)).a by A99,SCMFSA_2:71
.= (DataPart Exec (l,s2)).x by A100,FUNCT_1:49;
end;
suppose
x in FinSeq-Locations;
then reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;
thus (DataPart Exec (l,s1)).x = (Exec (l,s1)).a by A100,FUNCT_1:49
.= s1.a by A99,SCMFSA_2:71
.= (DataPart s1).a by A100,FUNCT_1:49
.= s2.a by A1,A100,FUNCT_1:49
.= (Exec (l,s2)).a by A99,SCMFSA_2:71
.= (DataPart Exec (l,s2)).x by A100,FUNCT_1:49;
end;
end;
hence thesis by A4,A6,FUNCT_1:2;
end;
suppose
InsCode i = 9;
then consider da,db being Int-Location, fa being FinSeq-Location such that
A101: l = db:=(fa,da) by SCMFSA_2:38;
A102: for x being object st x in ((Data-Locations SCM+FSA) \ {db})
holds (Exec (l,s1) | (Data-Locations SCM+FSA \ {db})).x = (Exec (l,
s2) | (Data-Locations SCM+FSA \ {db})).x
proof
let x be object;
assume
A103: x in ((Data-Locations SCM+FSA) \ {db});
then
A104: x in Data-Locations SCM+FSA by XBOOLE_0:def 5;
A105: not x in {db} by A103,XBOOLE_0:def 5;
per cases by A104,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in Int-Locations;
then reconsider a = x as Int-Location by AMI_2:def 16;
A106: a <> db by A105,TARSKI:def 1;
thus (Exec (l,s1) | (Data-Locations SCM+FSA \ {db})).x = (
Exec (l,s1)).a by A103,FUNCT_1:49
.= s1.a by A101,A106,SCMFSA_2:72
.= (DataPart s1).a by A104,FUNCT_1:49
.= s2.a by A1,A104,FUNCT_1:49
.= (Exec (l,s2)).a by A101,A106,SCMFSA_2:72
.= (Exec (l,s2) | (Data-Locations SCM+FSA \ {db})).x by A103,
FUNCT_1:49;
end;
suppose
x in FinSeq-Locations;
then reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;
thus (Exec (l,s1) | (Data-Locations SCM+FSA \ {db})).x = (
Exec (l,s1)).a by A103,FUNCT_1:49
.= s1.a by A101,SCMFSA_2:72
.= (DataPart s1).a by A104,FUNCT_1:49
.= s2.a by A1,A104,FUNCT_1:49
.= (Exec (l,s2)).a by A101,SCMFSA_2:72
.= (Exec (l,s2) | (Data-Locations SCM+FSA \ {db})).x by A103,
FUNCT_1:49;
end;
end;
A107: dom ((Exec (l,s2)) | (Data-Locations SCM+FSA \ {db})) = (
Data-Locations SCM+FSA \ {db}) by A5,RELAT_1:62;
dom ((Exec (l,s1)) | (Data-Locations SCM+FSA \ {db})) = (
Data-Locations SCM+FSA \ {db}) by A2,RELAT_1:62;
then
A108: Exec (l,s1) | (Data-Locations SCM+FSA \ {db} ) = Exec (l,
s2) | (Data-Locations SCM+FSA \ {db} ) by A107,A102,FUNCT_1:2;
db in Int-Locations by AMI_2:def 16;
then db in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then
A109: Data-Locations SCM+FSA = Data-Locations SCM+FSA \/ {db} by ZFMISC_1:40
.= (Data-Locations SCM+FSA \ {db} ) \/ {db} by XBOOLE_1:39;
A110: ex k2 being Nat st k2 = |.s2.da.| & Exec(l, s2).db = (
s2.fa)/.k2 by A101,SCMFSA_2:72;
A111: ex k1 being Nat st k1 = |.s1.da.| & Exec(l, s1).db = (
s1.fa)/.k1 by A101,SCMFSA_2:72;
fa in FinSeq-Locations by SCMFSA_2:def 5;
then
A112: fa in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then
A113: s1.fa = (DataPart s1).fa by FUNCT_1:49
.= s2.fa by A1,A112,FUNCT_1:49;
da in Int-Locations by AMI_2:def 16;
then
A114: da in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then s1.da = (DataPart s1).da by FUNCT_1:49
.= s2.da by A1,A114,FUNCT_1:49;
then Exec (l,s1) | {db} = Exec(l,s2) | {db} by A3,A111,A110,A113,
GRFUNC_1:29;
hence thesis by A109,A108,RELAT_1:150;
end;
suppose
InsCode i = 10;
then consider da,db being Int-Location, fa being FinSeq-Location such that
A115: l = (fa,da):=db by SCMFSA_2:39;
A116: for x being object st x in ((Data-Locations SCM+FSA) \ {fa})
holds (Exec (l,s1) | (Data-Locations SCM+FSA \ {fa})).x = (Exec (l,
s2) | (Data-Locations SCM+FSA \ {fa})).x
proof
let x be object;
assume
A117: x in ((Data-Locations SCM+FSA) \ {fa});
then
A118: x in Data-Locations SCM+FSA by XBOOLE_0:def 5;
A119: not x in {fa} by A117,XBOOLE_0:def 5;
per cases by A118,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in Int-Locations;
then reconsider a = x as Int-Location by AMI_2:def 16;
thus (Exec (l,s1) | (Data-Locations SCM+FSA \ {fa})).x = (
Exec (l,s1)).a by A117,FUNCT_1:49
.= s1.a by A115,SCMFSA_2:73
.= (DataPart s1).a by A118,FUNCT_1:49
.= s2.a by A1,A118,FUNCT_1:49
.= (Exec (l,s2)).a by A115,SCMFSA_2:73
.= (Exec (l,s2) | (Data-Locations SCM+FSA \ {fa})).x by A117,
FUNCT_1:49;
end;
suppose
x in FinSeq-Locations;
then reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;
A120: a <> fa by A119,TARSKI:def 1;
thus (Exec (l,s1) | (Data-Locations SCM+FSA \ {fa})).x = (
Exec (l,s1)).a by A117,FUNCT_1:49
.= s1.a by A115,A120,SCMFSA_2:73
.= (DataPart s1).a by A118,FUNCT_1:49
.= s2.a by A1,A118,FUNCT_1:49
.= (Exec (l,s2)).a by A115,A120,SCMFSA_2:73
.= (Exec (l,s2) | (Data-Locations SCM+FSA \ {fa})).x by A117,
FUNCT_1:49;
end;
end;
A121: dom ((Exec (l,s2)) | (Data-Locations SCM+FSA \ {fa})) = (
Data-Locations SCM+FSA \ {fa}) by A5,RELAT_1:62;
dom ((Exec (l,s1)) | (Data-Locations SCM+FSA \ {fa})) = (
Data-Locations SCM+FSA \ {fa}) by A2,RELAT_1:62;
then
A122: Exec (l,s1) | (Data-Locations SCM+FSA \ {fa} ) = Exec (l,
s2) | (Data-Locations SCM+FSA \ {fa} ) by A121,A116,FUNCT_1:2;
fa in FinSeq-Locations by SCMFSA_2:def 5;
then fa in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then
A123: Data-Locations SCM+FSA = Data-Locations SCM+FSA \/ {fa} by ZFMISC_1:40
.= (Data-Locations SCM+FSA \ {fa} ) \/ {fa} by XBOOLE_1:39;
fa in FinSeq-Locations by SCMFSA_2:def 5;
then
A124: fa in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then
A125: s1.fa = (DataPart s1).fa by FUNCT_1:49
.= s2.fa by A1,A124,FUNCT_1:49;
db in Int-Locations by AMI_2:def 16;
then
A126: db in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then
A127: s1.db = (DataPart s1).db by FUNCT_1:49
.= s2.db by A1,A126,FUNCT_1:49;
A128: ex k2 being Nat st k2 = |.s2.da.| & Exec(l, s2).fa =
s2.fa+*(k2,s2.db) by A115,SCMFSA_2:73;
A129: ex k1 being Nat st k1 = |.s1.da.| & Exec(l, s1).fa =
s1.fa+*(k1,s1.db) by A115,SCMFSA_2:73;
da in Int-Locations by AMI_2:def 16;
then
A130: da in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then s1.da = (DataPart s1).da by FUNCT_1:49
.= s2.da by A1,A130,FUNCT_1:49;
then Exec (l,s1) | {fa} = Exec(l,s2) | {fa} by A3,A129,A128,A127,A125,
GRFUNC_1:29;
hence thesis by A123,A122,RELAT_1:150;
end;
suppose
InsCode i = 11;
then consider da being Int-Location, fa being FinSeq-Location such that
A131: l = da:=len fa by SCMFSA_2:40;
A132: for x being object st x in ((Data-Locations SCM+FSA) \ {da})
holds (Exec (l,s1) | (Data-Locations SCM+FSA \ {da})).x = (Exec (l,
s2) | (Data-Locations SCM+FSA \ {da})).x
proof
let x be object;
assume
A133: x in ((Data-Locations SCM+FSA) \ {da});
then
A134: x in Data-Locations SCM+FSA by XBOOLE_0:def 5;
A135: not x in {da} by A133,XBOOLE_0:def 5;
per cases by A134,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in Int-Locations;
then reconsider a = x as Int-Location by AMI_2:def 16;
A136: a <> da by A135,TARSKI:def 1;
thus (Exec (l,s1) | (Data-Locations SCM+FSA \ {da})).x = (
Exec (l,s1)).a by A133,FUNCT_1:49
.= s1.a by A131,A136,SCMFSA_2:74
.= (DataPart s1).a by A134,FUNCT_1:49
.= s2.a by A1,A134,FUNCT_1:49
.= (Exec (l,s2)).a by A131,A136,SCMFSA_2:74
.= (Exec (l,s2) | (Data-Locations SCM+FSA \ {da})).x by A133,
FUNCT_1:49;
end;
suppose
x in FinSeq-Locations;
then reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;
thus (Exec (l,s1) | (Data-Locations SCM+FSA \ {da})).x = (
Exec (l,s1)).a by A133,FUNCT_1:49
.= s1.a by A131,SCMFSA_2:74
.= (DataPart s1).a by A134,FUNCT_1:49
.= s2.a by A1,A134,FUNCT_1:49
.= (Exec (l,s2)).a by A131,SCMFSA_2:74
.= (Exec (l,s2) | (Data-Locations SCM+FSA \ {da})).x by A133,
FUNCT_1:49;
end;
end;
da in Int-Locations by AMI_2:def 16;
then da in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then
A137: Data-Locations SCM+FSA = Data-Locations SCM+FSA \/ {da} by ZFMISC_1:40
.= (Data-Locations SCM+FSA \ {da} ) \/ {da} by XBOOLE_1:39;
fa in FinSeq-Locations by SCMFSA_2:def 5;
then
A138: fa in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then s1.fa = (s1 | (Data-Locations SCM+FSA)).fa by FUNCT_1:49
.= s2.fa by A1,A138,FUNCT_1:49;
then Exec (l,s1).da = len(s2.fa) by A131,SCMFSA_2:74
.= Exec (l,s2).da by A131,SCMFSA_2:74;
then
A139: Exec (l,s1) | {da} = Exec(l,s2) | {da} by A2,A5,GRFUNC_1:29;
A140: dom ((Exec (l,s2)) | (Data-Locations SCM+FSA \ {da})) = (
Data-Locations SCM+FSA \ {da}) by A5,RELAT_1:62;
dom ((Exec (l,s1)) | (Data-Locations SCM+FSA \ {da})) = (
Data-Locations SCM+FSA \ {da}) by A2,RELAT_1:62;
then Exec (l,s1) | (Data-Locations SCM+FSA \ {da} ) = Exec (l,
s2) | (Data-Locations SCM+FSA \ {da} ) by A140,A132,FUNCT_1:2;
hence thesis by A137,A139,RELAT_1:150;
end;
suppose
InsCode i = 12;
then consider da being Int-Location, fa being FinSeq-Location such that
A141: i = fa:=<0,...,0>da by SCMFSA_2:41;
set l = i;
A142: dom ((Exec (l,s2)) | (Data-Locations SCM+FSA \ {fa})) = (
Data-Locations SCM+FSA \ {fa}) by A5,RELAT_1:62;
A143: ex k2 being Nat st k2 = |.s2.da.| & Exec(l, s2).fa =
k2 |->0 by A141,SCMFSA_2:75;
A144: ex k1 being Nat st k1 = |.s1.da.| & Exec(l, s1).fa =
k1 |->0 by A141,SCMFSA_2:75;
A145: for x being object st x in ((Data-Locations SCM+FSA) \ {fa})
holds (Exec (l,s1) | (Data-Locations SCM+FSA \ {fa})).x = (Exec (l,
s2) | (Data-Locations SCM+FSA \ {fa})).x
proof
let x be object;
assume
A146: x in ((Data-Locations SCM+FSA) \ {fa});
then
A147: x in Data-Locations SCM+FSA by XBOOLE_0:def 5;
A148: not x in {fa} by A146,XBOOLE_0:def 5;
per cases by A147,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in Int-Locations;
then reconsider a = x as Int-Location by AMI_2:def 16;
thus (Exec (l,s1) | (Data-Locations SCM+FSA \ {fa})).x = (
Exec (l,s1)).a by A146,FUNCT_1:49
.= s1.a by A141,SCMFSA_2:75
.= (DataPart s1).a by A147,FUNCT_1:49
.= s2.a by A1,A147,FUNCT_1:49
.= (Exec (l,s2)).a by A141,SCMFSA_2:75
.= (Exec (l,s2) | (Data-Locations SCM+FSA \ {fa})).x by A146,
FUNCT_1:49;
end;
suppose
x in FinSeq-Locations;
then reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;
A149: a <> fa by A148,TARSKI:def 1;
thus (Exec (l,s1) | (Data-Locations SCM+FSA \ {fa})).x = (
Exec (l,s1)).a by A146,FUNCT_1:49
.= s1.a by A141,A149,SCMFSA_2:75
.= (DataPart s1).a by A147,FUNCT_1:49
.= s2.a by A1,A147,FUNCT_1:49
.= (Exec (l,s2)).a by A141,A149,SCMFSA_2:75
.= (Exec (l,s2) | (Data-Locations SCM+FSA \ {fa})).x by A146,
FUNCT_1:49;
end;
end;
dom ((Exec (l,s1)) | (Data-Locations SCM+FSA \ {fa})) = (
Data-Locations SCM+FSA \ {fa}) by A2,RELAT_1:62;
then
A150: Exec (l,s1) | (Data-Locations SCM+FSA \ {fa} ) = Exec (l,
s2) | (Data-Locations SCM+FSA \ {fa} ) by A142,A145,FUNCT_1:2;
fa in FinSeq-Locations by SCMFSA_2:def 5;
then fa in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then
A151: Data-Locations SCM+FSA = Data-Locations SCM+FSA \/ {fa} by ZFMISC_1:40
.= (Data-Locations SCM+FSA \ {fa} ) \/ {fa} by XBOOLE_1:39;
da in Int-Locations by AMI_2:def 16;
then
A152: da in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
then s1.da = (DataPart s1).da by FUNCT_1:49
.= s2.da by A1,A152,FUNCT_1:49;
then Exec (l,s1) | {fa} = Exec(l,s2) | {fa} by A3,A144,A143,GRFUNC_1:29;
hence thesis by A151,A150,RELAT_1:150;
end;
end;
Lm2: now
set IF = Data-Locations SCM+FSA;
let I be keeping_0 parahalting Program of SCM+FSA, s be State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
set IE = IExec(I,P,s);
now
A1: dom Initialized IE = the carrier of SCM+FSA by PARTFUN1:def 2;
A2: the carrier of SCM+FSA = {IC SCM+FSA} \/ Data-Locations SCM+FSA
by STRUCT_0:4;
A3: dom IE = the carrier of SCM+FSA by PARTFUN1:def 2;
hence dom DataPart Initialized IE = dom IE /\ IF by A1,RELAT_1:61;
then
A4: dom DataPart Initialized IE= Data-Locations SCM+FSA
by A3,A2,XBOOLE_1:21;
let x be object;
assume
A5: x in dom DataPart Initialized IE;
per cases by A5,A4,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in Int-Locations;
then reconsider x9 = x as Int-Location by AMI_2:def 16;
per cases;
suppose
A6: x9 is read-write;
thus (DataPart Initialized IE).x = (Initialized IE).x by A5,A4,
FUNCT_1:49
.= IE.x by A6,SCMFSA_M:37;
end;
suppose
x9 is read-only;
then
A7: x9 = intloc 0;
thus (DataPart Initialized IE).x = (Initialized IE).x9 by A5,A4,
FUNCT_1:49
.= 1 by A7,SCMFSA_M:9
.= IE.x by A7,SCMFSA6B:11;
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 A5,A4,FUNCT_1:49
.= IE.x by SCMFSA_M:37;
end;
end;
hence DataPart Initialized IE = DataPart IE by FUNCT_1:46;
end;
theorem Th4:
for i being sequential Instruction of SCM+FSA
holds Exec(i,Initialized s) = IExec(Macro i,P,s)
proof
let i be sequential Instruction of SCM+FSA;
set Mi = Macro i;
set sI = s+*Initialize((intloc 0).-->1),
pI = P+*Mi;
A1: Mi c= pI by FUNCT_4:25;
set Is = Initialized s;
set IC1 = IC Comput(P+*Mi,sI,1);
reconsider Mi as parahalting Program of SCM+FSA;
IC sI = 0 by MEMSTR_0:def 11;
then IC sI in dom Mi by AFINSQ_1:65;
then
A2: IC1 in dom Mi by A1,AMISTD_1:21;
A3: 1 in dom Mi by COMPOS_1:60;
A4: 0 in dom Mi by COMPOS_1:60;
A5: Mi. 0 = i by COMPOS_1:58;
A6: IC sI = 0 by MEMSTR_0:def 11;
A7: Comput(P+*Mi,sI,0+1) = Following(P+*Mi,Comput(P+*Mi,sI,0)) by EXTPRO_1:3
.= Exec(pI. 0, sI) by A6,PBOOLE:143
.= Exec(i, sI) by A5,A1,A4,GRFUNC_1:2;
per cases by A2,COMPOS_1:60;
suppose
A8: IC1 = 0;
then
A9: CurInstr(P+*Mi,Comput(P+*Mi,sI,1)) = (P+*Mi). 0 by PBOOLE:143
.= i by A5,A4,FUNCT_4:13;
IC sI = 0 by A6;
then
A10: InsCode i in {0, 6, 7, 8} by A7,A8,SCMFSA6A:3;
hereby
per cases by A10,ENUMSET1:def 2;
suppose
InsCode i = 0;
then
A11: i = halt SCM+FSA by SCMFSA_2:95;
then P+*Mi halts_on sI by A9,EXTPRO_1:29;
hence thesis by A7,A9,A11,EXTPRO_1:def 9;
end;
suppose
A12: InsCode i = 6 or InsCode i = 7 or InsCode i = 8;
A13: now
let a;
per cases by A12;
suppose
InsCode i = 6;
then ex l st i = goto l by SCMFSA_2:35;
hence sI.a = Exec(i, sI).a;
end;
suppose
InsCode i = 7;
then ex l, b st i = b=0_goto l by SCMFSA_2:36;
hence sI.a = Exec(i, sI).a;
end;
suppose
InsCode i = 8;
then ex l, b st i = b>0_goto l by SCMFSA_2:37;
hence sI.a = Exec(i, sI).a;
end;
end;
A14: now
let f;
per cases by A12;
suppose
InsCode i = 6;
then ex l st i = goto l by SCMFSA_2:35;
hence sI.f = Exec(i, sI).f;
end;
suppose
InsCode i = 7;
then ex l, a st i = a=0_goto l by SCMFSA_2:36;
hence sI.f = Exec(i, sI).f;
end;
suppose
InsCode i = 8;
then ex l, a st i = a>0_goto l by SCMFSA_2:37;
hence sI.f = Exec(i, sI).f;
end;
end;
A15: Following(P+*Mi,sI)
= Following(P+*Mi,Comput(P+*Mi,sI,0))
.= Exec(i, sI) by A7,EXTPRO_1:3;
A16: InsCode halt SCM+FSA = 0 by COMPOS_1:70;
for n being Nat holds
CurInstr(P+*Mi,Comput(P+*Mi,sI,n)) <> halt SCM+FSA
by A9,A12,A13,A14,A7,A8,A6,A15,A16,AMISTD_2:11,SCMFSA_2:104;
then
A17: not P+*Mi halts_on sI;
Mi c= P+*Mi by FUNCT_4:25;
hence Exec(i,Initialized s) = IExec(Macro i,P,s)
by A17,AMISTD_1:def 11;
end;
end;
end;
suppose
A18: IC1 = 1;
A19: Mi.1 = halt SCM+FSA by COMPOS_1:59;
A20: CurInstr(P+*Mi,Comput(P+*Mi,sI,1))
= (P+*Mi). 1 by A18,PBOOLE:143
.= halt SCM+FSA by A19,A1,A3,GRFUNC_1:2;
then P+*Mi halts_on sI by EXTPRO_1:29;
hence thesis by A7,A20,EXTPRO_1:def 9;
end;
end;
theorem Th5:
for I being keeping_0 parahalting really-closed Program of SCM+FSA,
j being sequential Instruction of SCM+FSA holds IExec(I ";" j,P,s).a
= Exec(j,IExec(I,P,s)).a
proof
let I be keeping_0 parahalting really-closed Program of SCM+FSA,
j be sequential Instruction of SCM+FSA;
set Mj = Macro j;
set SA = Start-At (IC IExec(Mj,P,IExec(I,P,s)) + card I,SCM+FSA);
A1: not a in dom SA by SCMFSA_2:102;
A2: DataPart Initialized IExec(I,P,s) = DataPart IExec(I,P,s) by Lm2;
a in Int-Locations by AMI_2:def 16;
then
A3: a in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
thus IExec(I ";" j,P,s).a = IncIC(IExec(Mj,P,IExec(I,P,s)),card I).a
by SCMFSA6B:20
.= IExec(Mj,P,IExec(I,P,s)).a by A1,FUNCT_4:11
.= ( Exec(j, Initialized IExec(I,P,s))).a by Th4
.= (DataPart Exec(j, Initialized IExec(I,P,s))).a by A3,FUNCT_1:49
.= (DataPart Exec(j,IExec(I,P,s))).a by A2,Th3
.= Exec(j,IExec(I,P,s)).a by A3,FUNCT_1:49;
end;
theorem Th6:
for I being keeping_0 parahalting really-closed Program of SCM+FSA,
j being sequential Instruction of SCM+FSA
holds IExec(I ";" j,P,s).f = Exec(j,IExec(I,P,s)).f
proof
let I be keeping_0 parahalting really-closed Program of SCM+FSA,
j be sequential Instruction of SCM+FSA;
set Mj = Macro j;
set SA = Start-At (IC IExec(Mj,P,IExec(I,P,s)) + card I,SCM+FSA);
A1: not f in dom SA by SCMFSA_2:103;
A2: DataPart Initialized IExec(I,P,s) = DataPart IExec(I,P,s) by Lm2;
f in FinSeq-Locations by SCMFSA_2:def 5;
then
A3: f in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
thus IExec(I ";" j,P,s).f = IncIC(IExec(Mj,P,IExec(I,P,s)),card I).f
by SCMFSA6B:20
.= IExec(Mj,P,IExec(I,P,s)).f by A1,FUNCT_4:11
.= ( Exec(j, Initialized IExec(I,P,s))).f by Th4
.= (DataPart Exec(j, Initialized IExec(I,P,s))).f by A3,FUNCT_1:49
.= (DataPart Exec(j,IExec(I,P,s))).f by A2,Th3
.= Exec(j,IExec(I,P,s)).f by A3,FUNCT_1:49;
end;
theorem Th7:
for i being keeping_0 sequential Instruction of SCM+FSA, j being
sequential Instruction of SCM+FSA holds IExec(i ";" j,P,s).a
= Exec(j, Exec(i,Initialized s)).a
proof
let i be keeping_0 sequential Instruction of SCM+FSA,
j be sequential Instruction of SCM+FSA;
set Mi = Macro i;
thus IExec(i ";" j,P,s).a = IExec(Mi ";" j,P, s).a
.= Exec(j,IExec(Mi,P,s)).a by Th5
.= Exec(j, Exec(i, Initialized s)).a by Th4;
end;
theorem
for i being keeping_0 sequential Instruction of SCM+FSA, j being
sequential Instruction of SCM+FSA holds IExec(i ";" j,P,s).f = Exec(j, Exec(i,
Initialized s)).f
proof
let i be keeping_0 sequential Instruction of SCM+FSA,
j be sequential
Instruction of SCM+FSA;
set Mi = Macro i;
thus IExec(i ";" j,P,s).f = IExec(Mi ";" j,P,s).f
.= Exec(j,IExec(Mi,P,s)).f by Th6
.= Exec(j, Exec(i, Initialized s)).f by Th4;
end;
begin :: An example
definition
let a, b be Int-Location;
func swap (a, b) -> Program of SCM+FSA equals
FirstNotUsed Macro (a := b) :=
a ";" (a := b) ";" (b := FirstNotUsed Macro (a := b));
correctness;
end;
registration
let a, b be Int-Location;
cluster swap(a,b) -> parahalting really-closed;
coherence;
end;
registration
let a, b be read-write Int-Location;
cluster swap(a,b) -> keeping_0;
coherence;
end;
theorem
for a, b being read-write Int-Location holds IExec(swap(a,b),P,s).a =
s.b & IExec(swap(a,b),P,s).b = s.a
proof
let a, b be read-write Int-Location;
set i0 = FirstNotUsed Macro (a := b) := a;
set i1 = a := b;
set i2 = b := FirstNotUsed Macro (a := b);
set i01 = i0 ";" i1;
UsedILoc Macro (a := b) = UsedIntLoc (a := b) by SF_MASTR:28;
then UsedILoc Macro (a := b) = {a, b} by SF_MASTR:14;
then
A1: not FirstNotUsed Macro (a := b) in {a, b} by SF_MASTR:50;
then
A2: FirstNotUsed Macro (a := b) <> a by TARSKI:def 2;
A3: FirstNotUsed Macro (a := b) <> b by A1,TARSKI:def 2;
hereby
per cases;
suppose
A4: a <> b;
thus IExec(swap(a,b),P,s).a = Exec(i2, IExec(i01,P,s)).a by Th5
.= IExec(i01,P,s).a by A4,SCMFSA_2:63
.= Exec(i1, Exec(i0, Initialized s)).a by Th7
.= Exec(i0, Initialized s).b by SCMFSA_2:63
.= (Initialized s).b by A3,SCMFSA_2:63
.= s.b by SCMFSA_M:37;
end;
suppose
A5: a = b;
thus IExec(swap(a,b),P,s).a = Exec(i2, IExec(i01,P,s)).a by Th5
.= IExec(i01,P,s).(FirstNotUsed Macro (a := b)) by A5,SCMFSA_2:63
.= Exec(i1, Exec(i0, Initialized s)).(FirstNotUsed Macro (a := b)) by
Th7
.= Exec(i0, Initialized s).(FirstNotUsed Macro (a := b)) by A2,
SCMFSA_2:63
.= (Initialized s).a by SCMFSA_2:63
.= s.b by A5,SCMFSA_M:37;
end;
end;
thus IExec(swap(a,b),P,s).b = Exec(i2, IExec(i01,P,s)).b by Th5
.= IExec(i01,P,s).(FirstNotUsed Macro (a := b)) by SCMFSA_2:63
.= Exec(i1, Exec(i0, Initialized s)).(FirstNotUsed Macro (a := b)) by Th7
.= Exec(i0, Initialized s).(FirstNotUsed Macro (a := b)) by A2,SCMFSA_2:63
.= (Initialized s).a by SCMFSA_2:63
.= s.a by SCMFSA_M:37;
end;
theorem
UsedI*Loc swap(a, b) = {}
proof
set i0 = FirstNotUsed Macro (a := b) := a;
set i1 = a := b;
set i2 = b := FirstNotUsed Macro (a := b);
thus UsedI*Loc swap(a, b) = (UsedI*Loc (i0 ";" i1)) \/ (UsedInt*Loc i2)
by SF_MASTR:46
.= (UsedI*Loc (i0 ";" i1)) \/ {} by SF_MASTR:32
.= (UsedInt*Loc i0) \/ (UsedInt*Loc i1) by SF_MASTR:47
.= (UsedInt*Loc i0) \/ {} by SF_MASTR:32
.= {} by SF_MASTR:32;
end;
registration let i,j be sequential Instruction of SCM+FSA;
cluster i ';' j -> really-closed;
coherence;
end;
registration
let I be really-closed MacroInstruction of SCM+FSA,
j be sequential Instruction of SCM+FSA;
cluster I ';' j -> really-closed;
coherence;
end;
registration
let i be sequential Instruction of SCM+FSA,
J be really-closed MacroInstruction of SCM+FSA;
cluster i ';' J -> really-closed;
coherence;
end;