Copyright (c) 1999 Association of Mizar Users
environ
vocabulary AMI_3, CAT_1, AMI_1, SCMPDS_2, SCMFSA_7, SCMPDS_3, RELAT_1,
FINSET_1, FUNCT_1, CARD_1, TARSKI, AMI_5, BOOLE, RELOC, FUNCT_4, INT_1,
SCMFSA6A, AMI_2, FUNCT_7, SCMPDS_1, ABSVALUE, NAT_1, ARYTM_1, SCMFSA6B,
FUNCOP_1, SCMPDS_4;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0,
RELAT_1, FUNCT_1, FUNCT_4, INT_1, NAT_1, CQC_LANG, FINSET_1, STRUCT_0,
AMI_1, AMI_2, AMI_3, AMI_5, FUNCT_7, SCMPDS_1, SCMPDS_2, GROUP_1,
SCMFSA_4, SCMPDS_3, CARD_1;
constructors DOMAIN_1, NAT_1, AMI_5, FUNCT_7, SCMPDS_1, SCMFSA_4, SCMPDS_3,
WELLORD2, MEMBERED;
clusters AMI_1, INT_1, FUNCT_1, RELSET_1, XBOOLE_0, SCMPDS_2, FUNCT_7,
PRELAMB, SCMFSA_4, SCMPDS_3, FRAENKEL, XREAL_0, MEMBERED, NUMBERS,
ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, AMI_1, AMI_3, SCMPDS_3, FUNCT_7, XBOOLE_0;
theorems AMI_1, AMI_3, NAT_1, CQC_LANG, TARSKI, FUNCT_4, FUNCT_1, ZFMISC_1,
INT_1, RELAT_1, AMI_5, SCMPDS_2, AMI_2, FUNCT_2, FUNCT_7, SCMPDS_3,
CARD_1, PRE_CIRC, WELLORD2, ENUMSET1, SCMFSA_2, CARD_3, ABSVALUE,
SCMFSA6A, GRFUNC_1, CARD_2, AXIOMS, SCM_1, SCMFSA6B, FINSEQ_1, XBOOLE_0,
XBOOLE_1, XCMPLX_0, XCMPLX_1;
schemes NAT_1, DOMAIN_1, FUNCT_7, ZFREFLE1;
begin :: Definition of a program block and its basic properties
definition
mode Program-block is initial programmed FinPartState of SCMPDS;
end;
reserve l, m, n for Nat,
i,j,k for Instruction of SCMPDS,
I,J,K for Program-block;
definition let i;
func Load i -> Program-block equals
:Def1: (inspos 0).--> i;
coherence
proof set I = (inspos 0).--> i;
A1: dom I = {inspos 0} by CQC_LANG:5;
reconsider I as finite Function;
reconsider I as FinPartState of SCMPDS;
I is initial programmed
proof
thus I is initial
proof let m,n such that
A2: inspos n in dom I and
A3: m < n;
inspos n = inspos 0 by A1,A2,TARSKI:def 1;
then n = 0 by SCMPDS_3:31;
hence inspos m in dom I by A3,NAT_1:18;
end;
thus dom I c= the Instruction-Locations of SCMPDS
by A1,ZFMISC_1:37;
end;
hence thesis;
end;
correctness;
end;
definition let i;
cluster Load i -> non empty;
coherence
proof
Load i = (inspos 0) .--> i by Def1;
hence Load i is non empty;
end;
end;
theorem Th1: ::SCMFSA6A=SCMPDS_4,Th15
for P being Program-block, n holds
n < card P iff inspos n in dom P
proof let P be Program-block, n;
deffunc U(Nat) = inspos $1;
set A = { m : U(m) in dom P};
A1: now let x be set;
assume
A2: x in dom P;
dom P c= the Instruction-Locations of SCMPDS by AMI_3:def 13;
then consider n such that
A3: x = inspos n by A2,SCMPDS_3:32;
take n;
thus x = U(n) by A3;
end;
A4: for n,m st U(n) = U(m) holds n = m by SCMPDS_3:31;
A5: dom P,A are_equipotent from CardMono(A1,A4);
defpred X[Nat] means U($1) in dom P;
set A = { m : X[m] };
A6: A is Subset of NAT from SubsetD;
now let n,m such that
A7: n in A and
A8: m < n;
ex l st l = n & inspos l in dom P by A7;
then inspos m in dom P by A8,SCMPDS_3:def 5;
hence m in A;
end;
then reconsider A as Cardinal by A6,FUNCT_7:22;
A9: Card n = n & Card card P = card P by FINSEQ_1:78;
A10: Card A = A by CARD_1:def 5;
hereby assume n < card P;
then Card n in Card card P by CARD_1:73;
then n in card dom P by A9,PRE_CIRC:21;
then n in Card A by A5,CARD_1:21;
then ex m st m = n & inspos m in dom P by A10;
hence inspos n in dom P;
end;
assume inspos n in dom P;
then n in Card A by A10;
then n in card dom P by A5,CARD_1:21;
then Card n in Card card P by A9,PRE_CIRC:21;
hence n < card P by CARD_1:73;
end;
definition let I be initial FinPartState of SCMPDS;
cluster ProgramPart I -> initial;
coherence
proof let m,n such that
A1: inspos n in dom ProgramPart I and
A2: m < n;
ProgramPart I c= I by AMI_5:63;
then dom ProgramPart I c= dom I by RELAT_1:25;
then inspos m in dom I by A1,A2,SCMPDS_3:def 5;
hence inspos m in dom ProgramPart I by AMI_5:73;
end;
end;
theorem Th2: ::S6A02,Th16
dom I misses dom Shift(J,card I)
proof
A1: dom Shift(J,card I) = { inspos(l+card I):inspos l in dom J }
by SCMPDS_3:def 7;
assume dom I meets dom Shift(J,card I);
then consider x being set such that
A2: x in dom I and
A3: x in { inspos(l+card I):inspos l in dom J } by A1,XBOOLE_0:3;
consider l such that
A4: x = inspos(l+card I) and inspos l in dom J by A3;
l+card I < card I by A2,A4,Th1;
hence contradiction by NAT_1:29;
end;
theorem Th3: :: S6A03,Th17
for I being programmed FinPartState of SCMPDS
holds card Shift(I,m) = card I
proof let I be programmed FinPartState of SCMPDS;
set B = { l:inspos l in dom I };
deffunc U(Nat) = inspos $1;
A1: for x being set st x in dom I ex d being Nat st x = U(d)
proof let x be set;
A2: dom I c= the Instruction-Locations of SCMPDS by AMI_3:def 13;
assume x in dom I;
hence thesis by A2,SCMPDS_3:32;
end;
A3: for d1,d2 being Nat st U(d1) = U(d2) holds d1=d2 by SCMPDS_3:31;
deffunc V(Nat) = inspos($1+m);
defpred NC[set] means not contradiction;
defpred X[Nat] means inspos $1 in dom I;
set B = { l: U(l) in dom I },
C = { V(l): l in { n: X[n] } & NC[l] },
D = { V(l): l in B },
E = { inspos(l+m):inspos l in dom I };
A4: dom I,B are_equipotent from CardMono(A1,A3);
set B = { l: X[l] };
B is Subset of NAT from SubsetD;
then A5: B c= NAT;
set B = { l:inspos l in dom I };
A6: now let d1,d2 be Nat;
assume V(d1) = V(d2);
then d1+m = d2+m by SCMPDS_3:31;
hence d1 = d2 by XCMPLX_1:2;
end;
A7: C c= E
proof let e be set;
assume e in C;
then consider l such that
A8: e =V(l) and
A9: l in { n: X[n] } & NC[l];
ex n st n=l & X[n] by A9;
hence e in E by A8;
end;
A10: E c= D
proof let e be set;
assume e in E;
then consider l such that
A11: e = inspos(l+m) and
A12: inspos l in dom I;
l in B by A12;
hence e in D by A11;
end;
A13: D c= C
proof let e be set;
assume e in D;
then ex l st e = V(l) & l in B;
hence e in C;
end;
then E c= C by A10,XBOOLE_1:1;
then
A14: C = E by A7,XBOOLE_0:def 10;
then
A15: C = D by A10,A13,XBOOLE_0:def 10;
A16: B,D are_equipotent from CardMono'(A5,A6);
dom Shift(I,m) = E by SCMPDS_3:def 7;
then A17: dom Shift(I,m),dom I are_equipotent by A4,A14,A15,A16,WELLORD2:22;
thus card Shift(I,m) = card dom Shift(I,m) by PRE_CIRC:21
.= card dom I by A17,CARD_1:21
.= card I by PRE_CIRC:21;
end;
theorem Th4: :: S6A04,Th20
for I,J being FinPartState of SCMPDS holds
ProgramPart(I +* J) = ProgramPart I +* ProgramPart J
proof let I,J be FinPartState of SCMPDS;
A1: ProgramPart I = I|the Instruction-Locations of SCMPDS &
ProgramPart J = J|the Instruction-Locations of SCMPDS
by AMI_5:def 6;
thus ProgramPart(I +* J) = (I +* J)|the Instruction-Locations of SCMPDS
by AMI_5:def 6
.= ProgramPart I +* ProgramPart J by A1,AMI_5:6;
end;
theorem ::Th21
for I,J being FinPartState of SCMPDS holds
Shift(ProgramPart(I +* J),n) =
Shift(ProgramPart I,n) +* Shift(ProgramPart J,n)
proof let I,J be FinPartState of SCMPDS;
thus
Shift(ProgramPart(I +* J),n) = Shift(ProgramPart I +* ProgramPart J,n)
by Th4
.= Shift(ProgramPart I,n) +* Shift(ProgramPart J,n) by SCMPDS_3:41;
end;
reserve a,b,c for Int_position,
s,s1,s2 for State of SCMPDS,
k1,k2 for Integer;
definition let I;
func Initialized I -> FinPartState of SCMPDS equals
:Def2: I +* Start-At(inspos 0);
coherence;
correctness;
end;
theorem Th6: ::S6A06,Th23
InsCode i in {0,1,4,5,6} or Exec(i,s).IC SCMPDS = Next IC s
proof
assume not InsCode i in {0,1,4,5,6};
then A1: InsCode i <> 0 & InsCode i <> 1 & InsCode i <> 4 & InsCode i <> 5
& InsCode i <> 6 by ENUMSET1:24;
A2: InsCode i <= 13 by SCMPDS_2:15;
per cases by A1,A2,SCMPDS_3:1;
suppose InsCode i = 2;
then ex a,k1 st i = a:=k1 by SCMPDS_2:37;
hence Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:57;
suppose InsCode i = 3;
then ex a,k1 st i = saveIC(a,k1) by SCMPDS_2:38;
hence Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:71;
suppose InsCode i = 7;
then ex a,k1,k2 st i = (a,k1) := k2 by SCMPDS_2:42;
hence Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:58;
suppose InsCode i = 8;
then ex a,k1,k2 st i = AddTo(a,k1,k2) by SCMPDS_2:43;
hence Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:60;
suppose InsCode i = 9;
then ex a,b,k1,k2 st i = AddTo(a,k1,b,k2) by SCMPDS_2:44;
hence Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:61;
suppose InsCode i = 10;
then ex a,b,k1,k2 st i = SubFrom(a,k1,b,k2) by SCMPDS_2:45;
hence Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:62;
suppose InsCode i = 11;
then ex a,b,k1,k2 st i = MultBy(a,k1,b,k2) by SCMPDS_2:46;
hence Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:63;
suppose InsCode i = 12;
then ex a,b,k1,k2 st i = Divide(a,k1,b,k2) by SCMPDS_2:47;
hence Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:64;
suppose InsCode i = 13;
then ex a,b,k1,k2 st i = (a,k1):=(b,k2) by SCMPDS_2:48;
hence Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:59;
end;
theorem Th7: :: Th24 SF_65
IC SCMPDS in dom Initialized I
proof
A1: dom Initialized I
= dom(I +* Start-At(inspos 0)) by Def2
.= dom I \/ dom Start-At(inspos 0)
by FUNCT_4:def 1;
dom Start-At(inspos 0) = { IC SCMPDS } by AMI_3:34;
then IC SCMPDS in dom Start-At(inspos 0) by TARSKI:def 1;
hence thesis by A1,XBOOLE_0:def 2;
end;
theorem :: S6A08
IC Initialized I = inspos 0
proof
dom Start-At(inspos 0) = { IC SCMPDS } by AMI_3:34;
then A1: IC SCMPDS in dom Start-At(inspos 0) by TARSKI:def 1;
IC SCMPDS in dom Initialized I by Th7;
hence IC Initialized I = (Initialized I).IC SCMPDS by AMI_3:def 16
.= (I +* Start-At(inspos 0)).IC SCMPDS by Def2
.= (Start-At inspos 0).IC SCMPDS by A1,FUNCT_4:14
.= inspos 0 by AMI_3:50;
end;
theorem Th9: :: Th26
I c= Initialized I
proof set A = the Instruction-Locations of SCMPDS;
A1: Initialized I = I +* Start-At(inspos 0) by Def2;
dom I c= A by AMI_3:def 13;
then A2: not IC SCMPDS in dom I by AMI_1:48;
dom Start-At(inspos 0) = { IC SCMPDS } by AMI_3:34;
then dom I misses dom (Start-At (inspos 0)) by A2,ZFMISC_1:56;
hence thesis by A1,FUNCT_4:33;
end;
canceled;
theorem Th11: :: Th28
for s1,s2 being State of SCMPDS
st IC s1 = IC s2 & for a being Int_position holds s1.a = s2.a
holds s1,s2 equal_outside the Instruction-Locations of SCMPDS
proof set A = the Instruction-Locations of SCMPDS;
let s1,s2 be State of SCMPDS such that
A1: IC s1 = IC s2 and
A2: for a being Int_position holds s1.a = s2.a;
not IC SCMPDS in A by AMI_1:48;
then {IC SCMPDS} misses A by ZFMISC_1:56;
then A3: {IC SCMPDS } \/ SCM-Data-Loc misses A by SCMPDS_2:10,XBOOLE_1:70;
A4: (the carrier of SCMPDS) \ A
= {IC SCMPDS } \/ SCM-Data-Loc \ A by SCMPDS_3:5,XBOOLE_1:40
.= {IC SCMPDS } \/ SCM-Data-Loc by A3,XBOOLE_1:83;
A5: dom s1 \ A c= dom s1 by XBOOLE_1:36;
A6: dom(s1|(dom s1 \ A)) = dom s1 /\ (dom s1 \ A) by RELAT_1:90
.= dom s1 \ A by A5,XBOOLE_1:28
.= {IC SCMPDS } \/ SCM-Data-Loc by A4,AMI_3:36;
A7: dom s2 \ A c= dom s2 by XBOOLE_1:36;
A8: dom(s2|(dom s2 \ A)) = dom s2 /\ (dom s2 \ A) by RELAT_1:90
.= dom s2 \ A by A7,XBOOLE_1:28
.= {IC SCMPDS } \/ SCM-Data-Loc by A4,AMI_3:36;
now let x be set;
assume
A9: x in {IC SCMPDS } \/ SCM-Data-Loc;
per cases by A9,XBOOLE_0:def 2;
suppose x in {IC SCMPDS};
then A10: x = IC SCMPDS by TARSKI:def 1;
thus (s1|(dom s1 \ A)).x = s1.x by A6,A9,FUNCT_1:70
.= IC s1 by A10,AMI_1:def 15
.= s2.x by A1,A10,AMI_1:def 15
.= (s2|(dom s2 \ A)).x by A8,A9,FUNCT_1:70;
suppose x in SCM-Data-Loc;
then A11: x is Int_position by SCMPDS_2:9;
thus (s1|(dom s1 \ A)).x = s1.x by A6,A9,FUNCT_1:70
.= s2.x by A2,A11
.= (s2|(dom s2 \ A)).x by A8,A9,FUNCT_1:70;
end;
hence s1|(dom s1 \ A) = s2|(dom s2 \ A) by A6,A8,FUNCT_1:9;
end;
canceled;
theorem Th13: :: Th30
s1,s2 equal_outside the Instruction-Locations of SCMPDS implies
for a being Int_position holds s1.a = s2.a
proof set IL = the Instruction-Locations of SCMPDS;
assume
A1: s1,s2 equal_outside IL;
let a be Int_position;
A2: a in dom s1 by SCMPDS_2:49;
A3: a in dom s2 by SCMPDS_2:49;
a in SCM-Data-Loc by SCMPDS_2:def 2;
then A4: not a in IL by SCMPDS_2:10,XBOOLE_0:3;
then a in dom s1 \ IL by A2,XBOOLE_0:def 4;
then A5: a in dom s1 /\ (dom s1 \ IL) by A2,XBOOLE_0:def 3;
a in dom s2 \ IL by A3,A4,XBOOLE_0:def 4;
then A6: a in dom s2 /\ (dom s2 \ IL) by A3,XBOOLE_0:def 3;
thus s1.a = (s1|(dom s1 \ IL)).a by A5,FUNCT_1:71
.= (s2|(dom s2 \ IL)).a by A1,FUNCT_7:def 2
.= s2.a by A6,FUNCT_1:71;
end;
theorem Th14: :: Lm1
s1,s2 equal_outside the Instruction-Locations of SCMPDS implies
s1.DataLoc(s1.a,k1)=s2.DataLoc(s2.a,k1)
proof assume
A1: s1,s2 equal_outside the Instruction-Locations of SCMPDS;
hence s1.DataLoc(s1.a,k1)=s1.DataLoc(s2.a,k1) by Th13
.=s2.DataLoc(s2.a,k1) by A1,Th13;
end;
theorem Th15: ::Th32
s1,s2 equal_outside the Instruction-Locations of SCMPDS implies
Exec(i,s1),Exec(i,s2) equal_outside the Instruction-Locations of SCMPDS
proof assume
A1: s1,s2 equal_outside the Instruction-Locations of SCMPDS;
A2: InsCode i <= 13 by SCMPDS_2:15;
A3: IC s1 = IC s2 by A1,SCMFSA6A:29;
per cases by A2,SCMPDS_3:1;
suppose InsCode i = 0;
then consider k1 such that
A4: i = goto k1 by SCMPDS_2:35;
A5: now let a;
thus Exec(i, s1).a = s1.a by A4,SCMPDS_2:66
.=s2.a by A1,Th13
.=Exec(i, s2).a by A4,SCMPDS_2:66;
end;
IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
.= ICplusConst(s1,k1) by A4,SCMPDS_2:66
.= ICplusConst(s2,k1) by A3,SCMPDS_3:2
.= Exec(i,s2).IC SCMPDS by A4,SCMPDS_2:66
.= IC Exec(i,s2) by AMI_1:def 15;
hence Exec(i,s1),Exec(i,s2)
equal_outside the Instruction-Locations of SCMPDS by A5,Th11;
suppose InsCode i = 1;
then consider a such that
A6: i = return a by SCMPDS_2:36;
A7: now let b;
per cases;
suppose A8:a=b;
hence Exec(i, s1).b= s1.DataLoc(s1.a,RetSP) by A6,SCMPDS_2:70
.=s2.DataLoc(s2.a,RetSP) by A1,Th14
.=Exec(i,s2).b by A6,A8,SCMPDS_2:70;
suppose A9:a<>b;
hence Exec(i, s1).b = s1.b by A6,SCMPDS_2:70
.=s2.b by A1,Th13
.=Exec(i,s2).b by A6,A9,SCMPDS_2:70;
end;
IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
.= 2*(abs(s1.DataLoc(s1.a,RetIC)) div 2)+4 by A6,SCMPDS_2:70
.= 2*(abs(s1.DataLoc(s2.a,RetIC)) div 2)+4 by A1,Th13
.= 2*(abs(s2.DataLoc(s2.a,RetIC)) div 2)+4 by A1,Th13
.= Exec(i,s2).IC SCMPDS by A6,SCMPDS_2:70
.= IC Exec(i,s2) by AMI_1:def 15;
hence thesis by A7,Th11;
suppose InsCode i = 2;
then consider a,k1 such that
A10: i = a := k1 by SCMPDS_2:37;
A11: now let b;
per cases;
suppose A12:a=b;
hence Exec(i, s1).b= k1 by A10,SCMPDS_2:57
.=Exec(i,s2).b by A10,A12,SCMPDS_2:57;
suppose A13:a<>b;
hence Exec(i,s1).b = s1.b by A10,SCMPDS_2:57
.=s2.b by A1,Th13
.=Exec(i,s2).b by A10,A13,SCMPDS_2:57;
end;
IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
.= Next IC s2 by A3,A10,SCMPDS_2:57
.= Exec(i,s2).IC SCMPDS by A10,SCMPDS_2:57
.= IC Exec(i,s2) by AMI_1:def 15;
hence thesis by A11,Th11;
suppose InsCode i = 3;
then consider a,k1 such that
A14: i = saveIC(a,k1) by SCMPDS_2:38;
A15: now let b;
per cases;
suppose A16:b=DataLoc(s1.a,k1);
then A17:b=DataLoc(s2.a,k1) by A1,Th13;
thus Exec(i, s1).b=IC s2 by A3,A14,A16,SCMPDS_2:71
.=Exec(i,s2).b by A14,A17,SCMPDS_2:71;
suppose A18:b<>DataLoc(s1.a,k1);
then A19:b<>DataLoc(s2.a,k1) by A1,Th13;
thus Exec(i,s1).b = s1.b by A14,A18,SCMPDS_2:71
.=s2.b by A1,Th13
.=Exec(i,s2).b by A14,A19,SCMPDS_2:71;
end;
IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
.= Next IC s2 by A3,A14,SCMPDS_2:71
.= Exec(i,s2).IC SCMPDS by A14,SCMPDS_2:71
.= IC Exec(i,s2) by AMI_1:def 15;
hence thesis by A15,Th11;
suppose InsCode i = 4;
then consider a,k1,k2 such that
A20: i = (a,k1)<>0_goto k2 by SCMPDS_2:39;
A21: now let a;
thus Exec(i, s1).a = s1.a by A20,SCMPDS_2:67
.=s2.a by A1,Th13
.=Exec(i, s2).a by A20,SCMPDS_2:67;
end;
now
per cases;
suppose A22: s1.DataLoc(s1.a,k1) <> 0;
then A23: s2.DataLoc(s2.a,k1) <> 0 by A1,Th14;
thus IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
.= ICplusConst(s1,k2) by A20,A22,SCMPDS_2:67
.= ICplusConst(s2,k2) by A3,SCMPDS_3:2
.= Exec(i,s2).IC SCMPDS by A20,A23,SCMPDS_2:67
.= IC Exec(i,s2) by AMI_1:def 15;
suppose A24: s1.DataLoc(s1.a,k1) = 0;
then A25: s2.DataLoc(s2.a,k1) = 0 by A1,Th14;
thus IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
.= Next IC s2 by A3,A20,A24,SCMPDS_2:67
.= Exec(i,s2).IC SCMPDS by A20,A25,SCMPDS_2:67
.= IC Exec(i,s2) by AMI_1:def 15;
end;
hence thesis by A21,Th11;
suppose InsCode i = 5;
then consider a,k1,k2 such that
A26: i = (a,k1)<=0_goto k2 by SCMPDS_2:40;
A27: now let a;
thus Exec(i, s1).a = s1.a by A26,SCMPDS_2:68
.=s2.a by A1,Th13
.=Exec(i, s2).a by A26,SCMPDS_2:68;
end;
now
per cases;
suppose A28: s1.DataLoc(s1.a,k1) <= 0;
then A29: s2.DataLoc(s2.a,k1) <= 0 by A1,Th14;
thus IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
.= ICplusConst(s1,k2) by A26,A28,SCMPDS_2:68
.= ICplusConst(s2,k2) by A3,SCMPDS_3:2
.= Exec(i,s2).IC SCMPDS by A26,A29,SCMPDS_2:68
.= IC Exec(i,s2) by AMI_1:def 15;
suppose A30: s1.DataLoc(s1.a,k1) > 0;
then A31: s2.DataLoc(s2.a,k1) > 0 by A1,Th14;
thus IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
.= Next IC s2 by A3,A26,A30,SCMPDS_2:68
.= Exec(i,s2).IC SCMPDS by A26,A31,SCMPDS_2:68
.= IC Exec(i,s2) by AMI_1:def 15;
end;
hence thesis by A27,Th11;
suppose InsCode i = 6;
then consider a,k1,k2 such that
A32: i = (a,k1)>=0_goto k2 by SCMPDS_2:41;
A33: now let a;
thus Exec(i, s1).a = s1.a by A32,SCMPDS_2:69
.=s2.a by A1,Th13
.=Exec(i, s2).a by A32,SCMPDS_2:69;
end;
now
per cases;
suppose A34: s1.DataLoc(s1.a,k1) >= 0;
then A35: s2.DataLoc(s2.a,k1) >= 0 by A1,Th14;
thus IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
.= ICplusConst(s1,k2) by A32,A34,SCMPDS_2:69
.= ICplusConst(s2,k2) by A3,SCMPDS_3:2
.= Exec(i,s2).IC SCMPDS by A32,A35,SCMPDS_2:69
.= IC Exec(i,s2) by AMI_1:def 15;
suppose A36: s1.DataLoc(s1.a,k1) < 0;
then A37: s2.DataLoc(s2.a,k1) < 0 by A1,Th14;
thus IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
.= Next IC s2 by A3,A32,A36,SCMPDS_2:69
.= Exec(i,s2).IC SCMPDS by A32,A37,SCMPDS_2:69
.= IC Exec(i,s2) by AMI_1:def 15;
end;
hence thesis by A33,Th11;
suppose InsCode i = 7;
then consider a,k1,k2 such that
A38: i = (a,k1) := k2 by SCMPDS_2:42;
A39: now let b;
per cases;
suppose A40:DataLoc(s1.a,k1)=b;
then A41: DataLoc(s2.a,k1)=b by A1,Th13;
thus Exec(i, s1).b= k2 by A38,A40,SCMPDS_2:58
.=Exec(i,s2).b by A38,A41,SCMPDS_2:58;
suppose A42:DataLoc(s1.a,k1)<>b;
then A43: DataLoc(s2.a,k1)<>b by A1,Th13;
thus Exec(i,s1).b = s1.b by A38,A42,SCMPDS_2:58
.=s2.b by A1,Th13
.=Exec(i,s2).b by A38,A43,SCMPDS_2:58;
end;
IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
.= Next IC s2 by A3,A38,SCMPDS_2:58
.= Exec(i,s2).IC SCMPDS by A38,SCMPDS_2:58
.= IC Exec(i,s2) by AMI_1:def 15;
hence thesis by A39,Th11;
suppose InsCode i = 8;
then consider a,k1,k2 such that
A44: i = AddTo(a,k1,k2) by SCMPDS_2:43;
A45: now let b;
per cases;
suppose A46:DataLoc(s1.a,k1)=b;
then A47: DataLoc(s2.a,k1)=b by A1,Th13;
thus Exec(i, s1).b= s1.DataLoc(s1.a,k1)+k2 by A44,A46,SCMPDS_2:60
.= s2.DataLoc(s2.a,k1)+k2 by A1,Th14
.=Exec(i,s2).b by A44,A47,SCMPDS_2:60;
suppose A48:DataLoc(s1.a,k1)<>b;
then A49: DataLoc(s2.a,k1)<>b by A1,Th13;
thus Exec(i,s1).b = s1.b by A44,A48,SCMPDS_2:60
.=s2.b by A1,Th13
.=Exec(i,s2).b by A44,A49,SCMPDS_2:60;
end;
IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
.= Next IC s2 by A3,A44,SCMPDS_2:60
.= Exec(i,s2).IC SCMPDS by A44,SCMPDS_2:60
.= IC Exec(i,s2) by AMI_1:def 15;
hence thesis by A45,Th11;
suppose InsCode i = 9;
then consider a,b,k1,k2 such that
A50: i = AddTo(a,k1,b,k2) by SCMPDS_2:44;
A51: now let c;
per cases;
suppose A52:DataLoc(s1.a,k1)=c;
then A53: DataLoc(s2.a,k1)=c by A1,Th13;
thus Exec(i, s1).c = s1.DataLoc(s1.a,k1)+s1.DataLoc(s1.b,k2)
by A50,A52,SCMPDS_2:61
.= s2.DataLoc(s2.a,k1)+s1.DataLoc(s1.b,k2) by A1,Th14
.= s2.DataLoc(s2.a,k1)+s2.DataLoc(s2.b,k2) by A1,Th14
.=Exec(i,s2).c by A50,A53,SCMPDS_2:61;
suppose A54:DataLoc(s1.a,k1)<>c;
then A55: DataLoc(s2.a,k1)<>c by A1,Th13;
thus Exec(i,s1).c = s1.c by A50,A54,SCMPDS_2:61
.=s2.c by A1,Th13
.=Exec(i,s2).c by A50,A55,SCMPDS_2:61;
end;
IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
.= Next IC s2 by A3,A50,SCMPDS_2:61
.= Exec(i,s2).IC SCMPDS by A50,SCMPDS_2:61
.= IC Exec(i,s2) by AMI_1:def 15;
hence thesis by A51,Th11;
suppose InsCode i = 10;
then consider a,b,k1,k2 such that
A56: i = SubFrom(a,k1,b,k2) by SCMPDS_2:45;
A57: now let c;
per cases;
suppose A58:DataLoc(s1.a,k1)=c;
then A59: DataLoc(s2.a,k1)=c by A1,Th13;
thus Exec(i, s1).c = s1.DataLoc(s1.a,k1)-s1.DataLoc(s1.b,k2)
by A56,A58,SCMPDS_2:62
.= s2.DataLoc(s2.a,k1)-s1.DataLoc(s1.b,k2) by A1,Th14
.= s2.DataLoc(s2.a,k1)-s2.DataLoc(s2.b,k2) by A1,Th14
.=Exec(i,s2).c by A56,A59,SCMPDS_2:62;
suppose A60:DataLoc(s1.a,k1)<>c;
then A61: DataLoc(s2.a,k1)<>c by A1,Th13;
thus Exec(i,s1).c = s1.c by A56,A60,SCMPDS_2:62
.=s2.c by A1,Th13
.=Exec(i,s2).c by A56,A61,SCMPDS_2:62;
end;
IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
.= Next IC s2 by A3,A56,SCMPDS_2:62
.= Exec(i,s2).IC SCMPDS by A56,SCMPDS_2:62
.= IC Exec(i,s2) by AMI_1:def 15;
hence thesis by A57,Th11;
suppose InsCode i = 11;
then consider a,b,k1,k2 such that
A62: i = MultBy(a,k1,b,k2) by SCMPDS_2:46;
A63: now let c;
per cases;
suppose A64:DataLoc(s1.a,k1)=c;
then A65: DataLoc(s2.a,k1)=c by A1,Th13;
thus Exec(i, s1).c = s1.DataLoc(s1.a,k1)*s1.DataLoc(s1.b,k2)
by A62,A64,SCMPDS_2:63
.= s2.DataLoc(s2.a,k1)*s1.DataLoc(s1.b,k2) by A1,Th14
.= s2.DataLoc(s2.a,k1)*s2.DataLoc(s2.b,k2) by A1,Th14
.=Exec(i,s2).c by A62,A65,SCMPDS_2:63;
suppose A66:DataLoc(s1.a,k1)<>c;
then A67: DataLoc(s2.a,k1)<>c by A1,Th13;
thus Exec(i,s1).c = s1.c by A62,A66,SCMPDS_2:63
.=s2.c by A1,Th13
.=Exec(i,s2).c by A62,A67,SCMPDS_2:63;
end;
IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
.= Next IC s2 by A3,A62,SCMPDS_2:63
.= Exec(i,s2).IC SCMPDS by A62,SCMPDS_2:63
.= IC Exec(i,s2) by AMI_1:def 15;
hence thesis by A63,Th11;
suppose InsCode i = 12;
then consider a,b,k1,k2 such that
A68: i = Divide(a,k1,b,k2) by SCMPDS_2:47;
A69: now let c;
per cases;
suppose A70:DataLoc(s1.b,k2)=c;
then A71: DataLoc(s2.b,k2)=c by A1,Th13;
thus Exec(i, s1).c = s1.DataLoc(s1.a,k1) mod s1.DataLoc(s1.b,k2)
by A68,A70,SCMPDS_2:64
.= s2.DataLoc(s2.a,k1) mod s1.DataLoc(s1.b,k2) by A1,Th14
.= s2.DataLoc(s2.a,k1) mod s2.DataLoc(s2.b,k2) by A1,Th14
.= Exec(i,s2).c by A68,A71,SCMPDS_2:64;
suppose A72:DataLoc(s1.b,k2)<>c;
then A73: DataLoc(s2.b,k2)<>c by A1,Th13;
hereby
per cases;
suppose A74:DataLoc(s1.a,k1)<>c;
then A75: DataLoc(s2.a,k1)<>c by A1,Th13;
thus Exec(i, s1).c = s1.c by A68,A72,A74,SCMPDS_2:64
.=s2.c by A1,Th13
.=Exec(i,s2).c by A68,A73,A75,SCMPDS_2:64;
suppose A76:DataLoc(s1.a,k1)=c;
then A77: DataLoc(s2.a,k1)=c by A1,Th13;
thus Exec(i, s1).c = s1.DataLoc(s1.a,k1) div s1.DataLoc(s1.b,k2)
by A68,A72,A76,SCMPDS_2:64
.= s2.DataLoc(s2.a,k1) div s1.DataLoc(s1.b,k2) by A1,Th14
.= s2.DataLoc(s2.a,k1) div s2.DataLoc(s2.b,k2) by A1,Th14
.= Exec(i,s2).c by A68,A73,A77,SCMPDS_2:64;
end;
end;
IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
.= Next IC s2 by A3,A68,SCMPDS_2:64
.= Exec(i,s2).IC SCMPDS by A68,SCMPDS_2:64
.= IC Exec(i,s2) by AMI_1:def 15;
hence thesis by A69,Th11;
suppose InsCode i = 13;
then consider a,b,k1,k2 such that
A78: i = (a,k1):=(b,k2) by SCMPDS_2:48;
A79: now let c;
per cases;
suppose A80:DataLoc(s1.a,k1)=c;
then A81: DataLoc(s2.a,k1)=c by A1,Th13;
thus Exec(i, s1).c = s1.DataLoc(s1.b,k2) by A78,A80,SCMPDS_2:59
.= s2.DataLoc(s2.b,k2) by A1,Th14
.=Exec(i,s2).c by A78,A81,SCMPDS_2:59;
suppose A82:DataLoc(s1.a,k1)<>c;
then A83: DataLoc(s2.a,k1)<>c by A1,Th13;
thus Exec(i,s1).c = s1.c by A78,A82,SCMPDS_2:59
.=s2.c by A1,Th13
.=Exec(i,s2).c by A78,A83,SCMPDS_2:59;
end;
IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
.= Next IC s2 by A3,A78,SCMPDS_2:59
.= Exec(i,s2).IC SCMPDS by A78,SCMPDS_2:59
.= IC Exec(i,s2) by AMI_1:def 15;
hence thesis by A79,Th11;
end;
theorem
(Initialized I)|the Instruction-Locations of SCMPDS = I
proof
A1: Initialized I = I +* Start-At(inspos 0) by Def2;
A2: dom I c= the Instruction-Locations of SCMPDS by AMI_3:def 13;
A3: not IC SCMPDS in the Instruction-Locations of SCMPDS by AMI_1:48;
dom Start-At(inspos 0) = { IC SCMPDS } by AMI_3:34;
then dom Start-At(inspos 0) misses the Instruction-Locations of SCMPDS
by A3,ZFMISC_1:56;
hence (Initialized I)|the Instruction-Locations of SCMPDS = I
by A1,A2,AMI_5:13;
end;
theorem Th17: :: SF2_16
for k1,k2 be Nat st k1 <> k2 holds DataLoc(k1,0) <> DataLoc(k2,0)
proof let k1,k2 be Nat;
assume A1:k1<>k2;
assume A2:DataLoc(k1,0) = DataLoc(k2,0);
A3: k1 >= 0 & k2 >= 0 by NAT_1:18;
DataLoc(k1,0)= 2*abs(k1+0)+1 & DataLoc(k2,0)= 2*abs(k2+0)+1
by SCMPDS_2:def 4;
then 2*abs(k1)=2*abs(k2) by A2,XCMPLX_1:2;
then abs(k1)=abs(k2) by XCMPLX_1:5;
then k1=abs(k2) by A3,ABSVALUE:def 1;
hence contradiction by A1,A3,ABSVALUE:def 1;
end;
theorem Th18: :: SF2_19:
for dl being Int_position ex i being Nat
st dl = DataLoc(i,0)
proof
let dl be Int_position;
dl in SCM-Data-Loc by SCMPDS_2:def 2;
then consider i being Nat such that
A1: dl = 2*i+1 by AMI_2:def 2;
take i;
i >= 0 by NAT_1:18;
hence dl =2*abs(i+0)+1 by A1,ABSVALUE:def 1
.=DataLoc(i,0) by SCMPDS_2:def 4;
end;
scheme SCMPDSEx{ F(set) -> Instruction of SCMPDS,
G(set) -> Integer,
I() -> Instruction-Location of SCMPDS }:
ex S being State of SCMPDS st IC S = I() &
for i being Nat holds
S.inspos i = F(i) & S.DataLoc(i,0) = G(i)
proof
defpred P[set,set] means ex m st
$1 = IC SCMPDS & $2 = I() or
$1 = inspos m & $2 = F(m) or
$1 = DataLoc(m,0) & $2 = G(m);
set S1={IC SCMPDS },
S2=SCM-Data-Loc,
S3=the Instruction-Locations of SCMPDS;
A1: for e being set st e in the carrier of SCMPDS
ex u being set st P[e,u]
proof let e be set;
assume e in the carrier of SCMPDS;
then A2: e in S1 \/ S2 or e in S3 by SCMPDS_3:5,XBOOLE_0:def 2;
now per cases by A2,XBOOLE_0:def 2;
case e in S1;
hence e = IC SCMPDS by TARSKI:def 1;
case e in S2;
then e is Int_position by SCMPDS_2:9;
hence ex m st e = DataLoc(m,0) by Th18;
case e in S3;
hence ex m st e = inspos m by SCMPDS_3:32;
end;
then consider m such that
A3: e = IC SCMPDS or e = inspos m or e = DataLoc(m,0);
per cases by A3;
suppose
A4: e = IC SCMPDS;
take u = I(); thus P[e,u] by A4;
suppose
A5: e = inspos m;
take u = F(m); thus P[e,u] by A5;
suppose
A6: e = DataLoc(m,0);
take u = G(m); thus P[e,u] by A6;
end;
consider f being Function such that
A7: dom f = the carrier of SCMPDS and
A8: for e being set st e in the carrier of SCMPDS holds P[e,f.e]
from NonUniqFuncEx(A1);
A9: dom the Object-Kind of SCMPDS = the carrier of SCMPDS by FUNCT_2:def 1;
now let x be set;
assume
A10: x in dom the Object-Kind of SCMPDS;
then A11: x in S1 \/ S2 or x in S3 by A9,SCMPDS_3:5,XBOOLE_0:def 2;
consider m such that
A12: x = IC SCMPDS & f.x = I() or
x = inspos m & f.x = F(m) or
x = DataLoc(m,0) & f.x = G(m) by A8,A9,A10;
per cases by A11,XBOOLE_0:def 2;
suppose x in S2;
then A13: x is Int_position by SCMPDS_2:9;
then (the Object-Kind of SCMPDS).x = ObjectKind DataLoc(m,0) by A12,AMI_1:
def 6,SCMPDS_2:52,53
.= INT by SCMPDS_2:13;
hence f.x in (the Object-Kind of SCMPDS).x by A12,A13,INT_1:12,SCMPDS_2:52,
53;
suppose x in S1;
then A14: x = IC SCMPDS by TARSKI:def 1;
then (the Object-Kind of SCMPDS).x = ObjectKind IC SCMPDS by AMI_1:def 6
.= the Instruction-Locations of SCMPDS by AMI_1:def 11;
hence f.x in (the Object-Kind of SCMPDS).x by A12,A14,AMI_1:48,SCMPDS_2:52;
suppose A15: x in the Instruction-Locations of SCMPDS;
then (the Object-Kind of SCMPDS).x = ObjectKind inspos m by A12,AMI_1:48,
def 6,SCMPDS_2:53
.= the Instructions of SCMPDS by AMI_1:def 14;
hence f.x in (the Object-Kind of SCMPDS).x by A12,A15,AMI_1:48,SCMPDS_2:53;
end;
then reconsider f as State of SCMPDS by A7,A9,CARD_3:18;
take f;
consider m such that
A16: IC SCMPDS = IC SCMPDS & f.IC SCMPDS = I() or
IC SCMPDS = inspos m & f.IC SCMPDS = F(m) or
IC SCMPDS = DataLoc(m,0) & f.IC SCMPDS = G(m) by A8;
thus IC f = I() by A16,AMI_1:48,def 15,SCMPDS_2:52;
let i be Nat;
consider m such that
A17: inspos i = IC SCMPDS & f.inspos i = I() or
inspos i = inspos m & f.inspos i = F(m) or
inspos i = DataLoc(m,0) & f.inspos i = G(m) by A8;
thus f.inspos i = F(i) by A17,AMI_1:48,SCMPDS_2:53,SCMPDS_3:31;
consider m such that
A18: DataLoc(i,0) = IC SCMPDS & f.DataLoc(i,0) = I() or
DataLoc(i,0) = inspos m & f.DataLoc(i,0) = F(m) or
DataLoc(i,0) = DataLoc(m,0) & f.DataLoc(i,0) = G(m) by A8;
thus f.DataLoc(i,0) = G(i) by A18,Th17,SCMPDS_2:52,53;
end;
theorem :: Th34
for s being State of SCMPDS holds
dom s = {IC SCMPDS} \/ SCM-Data-Loc \/
the Instruction-Locations of SCMPDS by AMI_3:36,SCMPDS_3:5;
theorem :: T12'
for s being State of SCMPDS, x being set st x in dom s holds
x is Int_position or x = IC SCMPDS or
x is Instruction-Location of SCMPDS
proof
let s be State of SCMPDS;
let x be set;
set S1={IC SCMPDS},
S2=SCM-Data-Loc,
S3=the Instruction-Locations of SCMPDS;
A1:dom s = S1 \/ S2 \/ S3 by AMI_3:36,SCMPDS_3:5;
assume x in dom s;
then x in S1 \/ S2 or x in S3 by A1,XBOOLE_0:def 2;
then x in S1 or x in S2 or x in S3 by XBOOLE_0:def 2;
hence thesis by SCMPDS_2:9,TARSKI:def 1;
end;
theorem :: T29
for s1,s2 being State of SCMPDS holds
(for l being Instruction-Location of SCMPDS holds s1.l = s2.l)
iff s1 | the Instruction-Locations of SCMPDS =
s2 | the Instruction-Locations of SCMPDS
proof
let s1,s2 be State of SCMPDS;
A1: the Instruction-Locations of SCMPDS c= dom s1 by SCMFSA_2:3;
A2: the Instruction-Locations of SCMPDS c= dom s2 by SCMFSA_2:3;
(for l being Instruction-Location of SCMPDS holds s1.l = s2.l) iff
(for l being set st l in the Instruction-Locations of SCMPDS
holds s1.l = s2.l);
hence thesis by A1,A2,SCMFSA6A:9;
end;
theorem :: T32
for i being Instruction-Location of SCMPDS holds
not i in SCM-Data-Loc
by SCMPDS_2:10,XBOOLE_0:3;
theorem Th23: :: Th38
for s1,s2 being State of SCMPDS holds
(for a being Int_position holds s1.a = s2.a)
iff s1 | SCM-Data-Loc = s2 | SCM-Data-Loc
proof
let s1,s2 be State of SCMPDS;
set T1={IC SCMPDS},
T2=SCM-Data-Loc,
T3=the Instruction-Locations of SCMPDS;
A1: T1 \/ T2 \/ T3=T2 \/ (T1 \/ T3) by XBOOLE_1:4;
dom s1 = T1 \/ T2 \/ T3 by AMI_3:36,SCMPDS_3:5;
then A2: T2 c= dom s1 by A1,XBOOLE_1:7;
dom s2 = T1 \/ T2 \/ T3 by AMI_3:36,SCMPDS_3:5;
then A3: T2 c= dom s2 by A1,XBOOLE_1:7;
A4: now
assume A5:for a being Int_position holds s1.a = s2.a;
hereby let x be set;
assume x in SCM-Data-Loc;
then x is Int_position by SCMPDS_2:9;
hence s1.x=s2.x by A5;
end;
end;
now
assume A6:for x be set st x in SCM-Data-Loc holds s1.x = s2.x;
hereby let a be Int_position;
a in SCM-Data-Loc by SCMPDS_2:def 2;
hence s1.a=s2.a by A6;
end;
end;
hence thesis by A2,A3,A4,SCMFSA6A:9;
end;
theorem :: T19
for s1,s2 being State of SCMPDS st
s1,s2 equal_outside the Instruction-Locations of SCMPDS holds
s1 | SCM-Data-Loc = s2 | SCM-Data-Loc
proof
let s1,s2 be State of SCMPDS;
assume s1,s2 equal_outside the Instruction-Locations of SCMPDS;
then for a being Int_position holds s1.a = s2.a by Th13;
hence thesis by Th23;
end;
theorem :: T21
for s,ss being State of SCMPDS, A being set holds
(ss +* s | A) | A = s | A
proof
let s,ss be State of SCMPDS;
let A be set;
A1: dom s = the carrier of SCMPDS by AMI_3:36;
A2: dom (ss +* s | A) = dom ss \/ dom (s | A) by FUNCT_4:def 1
.= dom ss \/ (dom s /\ A) by RELAT_1:90
.= (the carrier of SCMPDS) \/ (the carrier of SCMPDS) /\ A by A1,AMI_3:36
.= the carrier of SCMPDS by XBOOLE_1:22;
A3: dom s /\ A c= dom s by XBOOLE_1:17;
A4: now let x be set;
assume A5: x in dom s /\ A;
then x in dom (s | A) by RELAT_1:90;
hence (ss +* s | A).x = (s | A).x by FUNCT_4:14
.= s.x by A5,FUNCT_1:71;
end;
thus (ss +* s | A) | A
= (ss +* s | A) | (dom s /\ A) by A1,A2,SCMFSA6A:10
.= s | (dom s /\ A) by A1,A2,A3,A4,SCMFSA6A:9
.= s | A by SCMFSA6A:10;
end;
theorem :: T18
for I,J being Program-block holds
I,J equal_outside the Instruction-Locations of SCMPDS
proof
let I,J be Program-block;
dom I c= the Instruction-Locations of SCMPDS by AMI_3:def 13;
then dom I \ the Instruction-Locations of SCMPDS = {} by XBOOLE_1:37;
then A1: dom (I | (dom I \ the Instruction-Locations of SCMPDS)) = {} by
SCMFSA6A:8;
dom J c= the Instruction-Locations of SCMPDS by AMI_3:def 13;
then dom J \ the Instruction-Locations of SCMPDS = {} by XBOOLE_1:37;
then A2: dom (J | (dom J \ the Instruction-Locations of SCMPDS)) = {} by
SCMFSA6A:8;
for x be set st x in {} holds
(I | (dom I \ the Instruction-Locations of SCMPDS)).x =
(J | (dom J \ the Instruction-Locations of SCMPDS)).x;
then I | (dom I \ the Instruction-Locations of SCMPDS) =
J | (dom J \ the Instruction-Locations of SCMPDS) by A1,A2,FUNCT_1:9;
hence I,J equal_outside the Instruction-Locations of SCMPDS
by FUNCT_7:def 2;
end;
theorem Th27: :: Th43
for I being Program-block holds
dom Initialized I = dom I \/ {IC SCMPDS}
proof
let I be Program-block;
thus dom Initialized I
= dom(I +* Start-At(inspos 0)) by Def2
.= dom I \/ dom Start-At(inspos 0) by FUNCT_4:def 1
.= dom I \/ {IC SCMPDS} by AMI_3:34;
end;
theorem Th28: :: Th44
for I being Program-block, x being set st x in dom Initialized I holds
x in dom I or x = IC SCMPDS
proof
let I be Program-block;
let x be set;
A1: dom Initialized I = dom I \/ {IC SCMPDS} by Th27;
assume x in dom Initialized I;
then x in dom I or x in {IC SCMPDS} by A1,XBOOLE_0:def 2;
hence x in dom I or x = IC SCMPDS by TARSKI:def 1;
end;
theorem Th29: :: Th46
for I being Program-block holds
(Initialized I).IC SCMPDS = inspos 0
proof
let I be Program-block;
IC SCMPDS in {IC SCMPDS} by TARSKI:def 1;
then A1: IC SCMPDS in dom Start-At inspos 0 by AMI_3:34;
thus (Initialized I).IC SCMPDS
= (I +* (Start-At (inspos 0))).IC SCMPDS by Def2
.= (Start-At (inspos 0)).IC SCMPDS by A1,FUNCT_4:14
.= (IC SCMPDS .--> inspos 0).IC SCMPDS by AMI_3:def 12
.= inspos 0 by CQC_LANG:6;
end;
theorem Th30: :: Th47
for I being Program-block holds not IC SCMPDS in dom I
proof
let I be Program-block;
dom I c= the Instruction-Locations of SCMPDS by AMI_3:def 13;
hence not IC SCMPDS in dom I by AMI_1:48;
end;
theorem Th31: :: Th48
for I being Program-block, a being Int_position holds
not a in dom Initialized I
proof
let I be Program-block;
let a be Int_position;
assume a in dom Initialized I;
then A1: a in dom I \/ {IC SCMPDS} by Th27;
per cases by A1,XBOOLE_0:def 2;
suppose A2: a in dom I;
dom I c= the Instruction-Locations of SCMPDS by AMI_3:def 13;
hence contradiction by A2,SCMPDS_2:53;
suppose a in {IC SCMPDS};
then a = IC SCMPDS by TARSKI:def 1;
hence contradiction by SCMPDS_2:52;
end;
reserve x for set;
theorem Th32: ::TN32
x in dom I implies I.x = (I +* Start-At inspos n).x
proof assume
A1: x in dom I;
A2: dom I c= the Instruction-Locations of SCMPDS by AMI_3:def 13;
A3: dom Start-At inspos n = {IC SCMPDS} by AMI_3:34;
x <> IC SCMPDS by A1,A2,AMI_1:48;
then not x in dom Start-At inspos n by A3,TARSKI:def 1;
hence thesis by FUNCT_4:12;
end;
theorem Th33: :: Th50
for I being Program-block, x being set st x in dom I holds
I.x = (Initialized I).x
proof
let I be Program-block, x be set;
assume A1: x in dom I;
thus (Initialized I).x
= (I +* Start-At(inspos 0)).x by Def2
.= I.x by A1,Th32;
end;
theorem Th34: :: Th51
for I,J being Program-block
for s being State of SCMPDS st Initialized J c= s holds
s +* Initialized I = s +* I
proof
let I,J be Program-block;
let s be State of SCMPDS;
set s1 = s +* I;
assume A1: Initialized J c= s;
then A2: dom Initialized J c= dom s by GRFUNC_1:8;
dom J \/ dom Initialized I
= dom J \/ (dom I \/ {IC SCMPDS}) by Th27
.= dom J \/ {IC SCMPDS} \/ dom I by XBOOLE_1:4
.= dom Initialized J \/ dom I by Th27;
then dom J \/ dom Initialized I c= dom s \/ dom I by A2,XBOOLE_1:13;
then dom J \/ dom Initialized I c= dom s1 by FUNCT_4:def 1;
then A3: dom Initialized I c= dom s1 by XBOOLE_1:11;
A4: now let x be set;
assume A5: x in dom Initialized I;
per cases by A5,Th28;
suppose A6: x in dom I;
hence (Initialized I).x = I.x by Th33
.= s1.x by A6,FUNCT_4:14;
suppose A7: x = IC SCMPDS;
then A8: not x in dom I by Th30;
A9: x in dom Initialized J by A7,Th7;
thus (Initialized I).x = inspos 0 by A7,Th29
.= (Initialized J).x by A7,Th29
.= s.x by A1,A9,GRFUNC_1:8
.= s1.x by A8,FUNCT_4:12;
end;
A10: dom (s +* I) = dom s \/ dom I by FUNCT_4:def 1;
A11: dom (s +* Initialized I) = dom s \/ dom Initialized I by FUNCT_4:def 1;
I c= Initialized I by Th9;
then A12: dom I c= dom Initialized I by GRFUNC_1:8;
then A13: dom (s +* I) c= dom (s +* Initialized I) by A10,A11,XBOOLE_1:9;
dom (s +* Initialized I) c= dom s \/ (dom s \/ dom I)
by A3,A10,A11,XBOOLE_1:9;
then dom (s +* Initialized I) c= dom s \/ dom s \/ dom I by XBOOLE_1:4;
then A14: dom (s +* Initialized I) = dom (s +* I) by A10,A13,XBOOLE_0:def 10;
now let x be set;
assume x in dom (s +* Initialized I);
per cases;
suppose A15: x in dom Initialized I;
hence (s +* Initialized I).x = (Initialized I).x by FUNCT_4:14
.= (s +* I).x by A4,A15;
suppose A16: not x in dom Initialized I;
then A17: not x in dom I by A12;
thus (s +* Initialized I).x = s.x by A16,FUNCT_4:12
.= (s +* I).x by A17,FUNCT_4:12;
end;
hence s +* Initialized I = s +* I by A14,FUNCT_1:9;
end;
theorem
for I,J being Program-block
for s being State of SCMPDS st Initialized J c= s holds
Initialized I c= s +* I
proof
let I,J be Program-block;
let s be State of SCMPDS;
assume Initialized J c= s;
then s +* Initialized I = s +* I by Th34;
hence Initialized I c= s +* I by FUNCT_4:26;
end;
theorem
for I,J being Program-block
for s being State of SCMPDS holds
s +* Initialized I, s +* Initialized J
equal_outside the Instruction-Locations of SCMPDS
proof
let I,J be Program-block;
let s be State of SCMPDS;
A1: IC SCMPDS in dom Initialized I & IC SCMPDS in dom Initialized J
by Th7;
A2: IC (s +* Initialized J) = (s +* Initialized J).IC SCMPDS by AMI_1:def 15
.= (Initialized J).IC SCMPDS by A1,FUNCT_4:14
.= inspos 0 by Th29
.= (Initialized I).IC SCMPDS by Th29
.= (s +* Initialized I).IC SCMPDS by A1,FUNCT_4:14
.= IC (s +* Initialized I) by AMI_1:def 15;
now let a be Int_position;
A3: not a in dom Initialized I by Th31;
not a in dom Initialized J by Th31;
hence (s +* Initialized J).a = s.a by FUNCT_4:12
.= (s +* Initialized I).a by A3,FUNCT_4:12;
end;
hence thesis by A2,Th11;
end;
begin :: Combining two consecutive blocks into one program block
definition let I,J be Program-block;
func I ';' J -> Program-block equals
:Def3: I +* Shift(J, card I);
coherence
proof set P = I +* Shift(J,card I);
P is initial
proof let m,n such that
A1: inspos n in dom P and
A2: m < n;
set D = {inspos(l+card I): inspos l in dom J };
dom Shift(J,card I) = D by SCMPDS_3:def 7;
then A3: dom P = dom I \/ D by FUNCT_4:def 1;
per cases by A1,A3,XBOOLE_0:def 2;
suppose inspos n in dom I;
then inspos m in dom I by A2,SCMPDS_3:def 5;
hence inspos m in dom P by A3,XBOOLE_0:def 2;
suppose inspos n in D;
then consider l such that
A4: inspos n = inspos(l+card I) and
A5: inspos l in dom J;
A6: n = l+card I by A4,SCMPDS_3:31;
now per cases;
case m < card I;
then inspos m in dom I by Th1;
hence inspos m in dom P by A3,XBOOLE_0:def 2;
case m >= card I;
then consider l1 being Nat such that
A7: m = card I + l1 by NAT_1:28;
l1 < l by A2,A6,A7,AXIOMS:24;
then inspos l1 in dom J by A5,SCMPDS_3:def 5;
hence inspos m in D by A7;
end;
hence inspos m in dom P by A3,XBOOLE_0:def 2;
end;
hence thesis;
end;
correctness;
end;
theorem Th37:
for I,J being Program-block, l being Instruction-Location of SCMPDS
st l in dom I holds (I ';' J).l = I.l
proof let I,J be Program-block, l be Instruction-Location of SCMPDS such
that
A1: l in dom I;
A2: now assume l in dom Shift(J,card I);
then l in { inspos(m+card I):inspos m in dom J } by SCMPDS_3:def 7;
then consider m such that
A3: l = inspos(m+card I) and inspos m in dom J;
m + card I < card I by A1,A3,Th1;
hence contradiction by NAT_1:29;
end;
thus (I ';' J).l = ( I +* Shift(J, card I)).l by Def3
.= I.l by A2,FUNCT_4:12;
end;
theorem Th38:
for I,J being Program-block, l being Instruction-Location of SCMPDS
st l in dom J holds (I ';' J).(l+card I)= J.l
proof let I,J be Program-block, l be Instruction-Location of SCMPDS such
that
A1: l in dom J;
consider n such that
A2: l=inspos n by SCMPDS_3:32;
inspos(n+card I) in { inspos(m+card I):inspos m in dom J } by A1,A2;
then inspos(n+card I) in dom Shift(J,card I) by SCMPDS_3:def 7;
then A3: l+card I in dom Shift(J,card I) by A2,SCMPDS_3:def 3;
thus (I ';' J).(l+card I) = ( I +* Shift(J, card I)).(l+card I) by Def3
.= Shift(J, card I).(l+card I) by A3,FUNCT_4:14
.=J.l by A1,SCMPDS_3:37;
end;
theorem Th39: :: Th56
for I,J being Program-block holds
dom I c= dom (I ';' J)
proof
let I,J be Program-block;
I ';' J = I +* Shift(J,card I) by Def3;
then dom (I ';' J) = dom I \/ dom Shift(J,card I)
by FUNCT_4:def 1;
hence dom I c= dom (I ';' J) by XBOOLE_1:7;
end;
theorem
for I,J being Program-block holds
I c= I ';' J
proof
let I,J be Program-block;
A1: I ';' J = I +* Shift(J,card I) by Def3;
A2: dom I c= dom (I ';' J) by Th39;
now let x be set;
assume A3: x in dom I;
dom I misses dom Shift(J,card I) by Th2;
then not x in dom Shift(J,card I) by A3,XBOOLE_0:3;
hence I.x = (I ';' J).x by A1,FUNCT_4:12;
end;
hence I c= I ';' J by A2,GRFUNC_1:8;
end;
theorem
for I,J being Program-block holds
I +* (I ';' J) = (I ';' J)
proof
let I,J be Program-block;
A1: dom I c= dom (I ';' J) by Th39;
A2: dom (I +* (I ';' J)) = dom I \/ dom (I ';' J) by FUNCT_4:def 1
.= dom (I ';' J) by A1,XBOOLE_1:12;
for x be set st x in dom (I ';' J) holds
(I +* (I ';' J)).x = (I ';' J).x by FUNCT_4:14;
hence I +* (I ';' J) = (I ';' J) by A2,FUNCT_1:9;
end;
theorem
for I,J being Program-block holds
Initialized I +* (I ';' J) = Initialized (I ';' J)
proof
let I,J be Program-block;
dom I c= dom (I ';' J) by Th39;
then A1: dom I \/ dom (I ';' J) = dom (I ';' J) by XBOOLE_1:12;
A2: dom (Initialized I+*(I ';' J))
= dom Initialized I \/ dom (I ';' J) by FUNCT_4:def 1
.= dom I \/ {IC SCMPDS} \/ dom (I ';' J) by Th27
.= dom I \/ dom (I ';' J) \/ {IC SCMPDS} by XBOOLE_1:4
.= dom Initialized (I ';' J) by A1,Th27;
now let x be set;
assume A3: x in dom Initialized (I ';' J);
per cases by A3,Th28;
suppose A4: x in dom (I ';' J);
then x <> IC SCMPDS by Th30;
then not x in {IC SCMPDS} by TARSKI:def 1;
then A5: not x in dom Start-At inspos 0 by AMI_3:34;
thus (Initialized I+*(I ';' J)).x
= (I ';' J).x by A4,FUNCT_4:14
.= ((I ';' J) +* Start-At(inspos 0)).x by A5,FUNCT_4:12
.= (Initialized (I ';' J)).x by Def2;
suppose A6: x = IC SCMPDS;
then not x in dom (I ';' J) by Th30;
hence (Initialized I+*(I ';' J)).x
= (Initialized I).x by FUNCT_4:12
.= inspos 0 by A6,Th29
.= (Initialized (I ';' J)).x by A6,Th29;
end;
hence Initialized I +* (I ';' J) = Initialized (I ';' J) by A2,FUNCT_1:9;
end;
begin :: Combining a block and a instruction into one program block
definition let i, J;
func i ';' J -> Program-block equals
:Def4: Load i ';' J;
correctness;
end;
definition let I, j;
func I ';' j -> Program-block equals
:Def5: I ';' Load j;
correctness;
end;
definition let i,j;
func i ';' j -> Program-block equals
:Def6: Load i ';' Load j;
correctness;
end;
theorem Th43: :: Th59
i ';' j = Load i ';' j
proof
thus i ';' j = Load i ';' Load j by Def6
.= Load i ';' j by Def5;
end;
theorem Th44: :: Th60
i ';' j = i ';' Load j
proof
thus i ';' j = Load i ';' Load j by Def6
.= i ';' Load j by Def4;
end;
theorem Th45: :: Th61
card(I ';' J) = card I + card J
proof
A1: card dom(I ';' J) = card(I ';' J) &
card dom I = card I & card dom J = card J by PRE_CIRC:21;
A2: card dom Shift(J, card I)
= card Shift(J, card I) by PRE_CIRC:21
.= card J by Th3
.= card dom J by PRE_CIRC:21;
A3: dom(I ';' J)
= dom(I +* Shift(J, card I)) by Def3
.= dom I \/ dom Shift(J, card I) by FUNCT_4:def 1;
dom I misses dom Shift(J,card I) by Th2;
hence card(I ';' J) = card I + card J by A1,A2,A3,CARD_2:53;
end;
theorem Th46: :: Th62
I ';' J ';' K = I ';' (J ';' K)
proof
A1: Shift(J ';' K, card I)
= Shift(J +* Shift(K, card J), card I) by Def3
.= Shift(J,card I) +* Shift(Shift(K, card J), card I) by SCMPDS_3:41
.= Shift(J,card I) +* Shift(K, card J+card I) by SCMPDS_3:39
.= Shift(J,card I) +* Shift(K, card ( I ';'J)) by Th45;
thus I ';' J ';' K
= (I ';' J) +* Shift(K, card(I ';' J)) by Def3
.= I +* Shift(J, card I) +* Shift(K, card(I ';' J)) by Def3
.= I +* Shift(J ';' K, card I) by A1,FUNCT_4:15
.= I ';' (J ';' K) by Def3;
end;
theorem Th47: :: Th63
I ';' J ';' k = I ';' (J ';' k)
proof
thus I ';' J ';' k = I ';' J ';' Load k by Def5
.= I ';' (J ';' Load k) by Th46
.= I ';' (J ';' k) by Def5;
end;
theorem
I ';' j ';' K = I ';' (j ';' K)
proof
thus I ';' j ';' K = I ';' Load j ';' K by Def5
.= I ';' (Load j ';' K) by Th46
.= I ';' (j ';' K) by Def4;
end;
theorem
I ';' j ';' k = I ';' (j ';' k)
proof
thus I ';' j ';' k = I ';' Load j ';' k by Def5
.= I ';' (Load j ';' k) by Th47
.= I ';' (j ';' k) by Th43;
end;
theorem Th50: :: Th66
i ';' J ';' K = i ';' (J ';' K)
proof
thus i ';' J ';' K = Load i ';' J ';' K by Def4
.= Load i ';' (J ';' K) by Th46
.= i ';' (J ';' K) by Def4;
end;
theorem
i ';' J ';' k = i ';' (J ';' k)
proof
thus i ';' J ';' k = Load i ';' J ';' k by Def4
.= Load i ';' (J ';' k) by Th47
.= i ';' (J ';' k) by Def4;
end;
theorem Th52: :: Th68
i ';' j ';' K = i ';' (j ';' K)
proof
thus i ';' j ';' K = i ';' Load j ';' K by Th44
.= i ';' (Load j ';' K) by Th50
.= i ';' (j ';' K) by Def4;
end;
theorem
i ';' j ';' k = i ';' (j ';' k)
proof
thus i ';' j ';' k = i ';' j ';' Load k by Def5
.= i ';' (j ';' Load k) by Th52
.= i ';' (j ';' k) by Th44;
end;
theorem Th54: :: SFM Th64:
dom I misses dom Start-At inspos n
proof
A1: dom Start-At inspos n = {IC SCMPDS} by AMI_3:34;
A2: dom I c= the Instruction-Locations of SCMPDS by AMI_3:def 13;
assume dom I /\ dom (Start-At inspos n) <> {};
then consider x being set such that
A3: x in dom I /\ dom (Start-At inspos n) by XBOOLE_0:def 1;
x in dom I & x in dom (Start-At inspos n) by A3,XBOOLE_0:def 3;
then IC SCMPDS in dom I by A1,TARSKI:def 1;
hence contradiction by A2,AMI_1:48;
end;
theorem :: TN55
Start-At inspos 0 c= Initialized I
proof
Initialized I = I +* Start-At(inspos 0) by Def2;
hence thesis by FUNCT_4:26;
end;
theorem Th56: ::TN56
I +* Start-At inspos n c= s implies I c= s
proof assume
A1: I +* Start-At inspos n c= s;
dom I misses dom Start-At inspos n by Th54;
then I +* Start-At inspos n = I \/ Start-At inspos n by FUNCT_4:32;
hence thesis by A1,XBOOLE_1:11;
end;
theorem ::S6B_5
Initialized I c= s implies I c= s
proof assume
Initialized I c= s;
then I +* Start-At inspos 0 c= s by Def2;
hence thesis by Th56;
end;
theorem Th58: ::TN58
(I +* Start-At inspos n)|the Instruction-Locations of SCMPDS = I
proof
A1: dom I c= the Instruction-Locations of SCMPDS by AMI_3:def 13;
the Instruction-Locations of SCMPDS misses dom Start-At inspos n
proof
assume not thesis; then consider x being set such that
A2: x in the Instruction-Locations of SCMPDS & x in dom Start-At inspos n
by XBOOLE_0:3;
dom Start-At inspos n = {IC SCMPDS} by AMI_3:34;
then x = IC SCMPDS by A2,TARSKI:def 1;
hence contradiction by A2,AMI_1:48;
end;
then (I +* Start-At inspos n)|the Instruction-Locations of SCMPDS
= I | the Instruction-Locations of SCMPDS by AMI_5:7;
hence thesis by A1,RELAT_1:97;
end;
reserve l,l1,loc for Instruction-Location of SCMPDS;
theorem Th59: ::TN59
not a in dom Start-At l
proof assume
A1: a in dom Start-At l;
dom Start-At l = {IC SCMPDS} by AMI_3:34;
then a = IC SCMPDS by A1,TARSKI:def 1;
hence contradiction by SCMPDS_2:52;
end;
theorem
not l1 in dom Start-At l
proof assume
A1: l1 in dom Start-At l;
dom Start-At l = {IC SCMPDS} by AMI_3:34;
then l1 = IC SCMPDS by A1,TARSKI:def 1;
hence contradiction by AMI_1:48;
end;
theorem ::TN61
not a in dom (I+*Start-At l)
proof assume
a in dom (I+*Start-At l);
then a in dom I \/ dom Start-At l by FUNCT_4:def 1;
then A1: a in dom I or a in dom Start-At l by XBOOLE_0:def 2;
A2: dom I c= the Instruction-Locations of SCMPDS by AMI_3:def 13;
a in SCM-Data-Loc by SCMPDS_2:def 2;
hence contradiction by A1,A2,Th59,SCMPDS_2:10,XBOOLE_0:3;
end;
theorem ::TN62
s+*I+*Start-At inspos 0 = s+*Start-At inspos 0+*I
proof
A1: dom I misses dom Start-At inspos 0 by Th54;
then I+*Start-At inspos 0 = I \/ Start-At inspos 0 by FUNCT_4:32
.= Start-At inspos 0 +* I by A1,FUNCT_4:32;
hence s+*I+*Start-At inspos 0
= s+*(Start-At inspos 0+*I) by FUNCT_4:15
.= s+*Start-At inspos 0+*I by FUNCT_4:15;
end;
definition
let s be State of SCMPDS, li be Int_position, k be Integer;
redefine func s+*(li,k) -> State of SCMPDS;
coherence proof
A1: dom(s+*(li,k)) = dom s by FUNCT_7:32;
A2: dom s = dom the Object-Kind of SCMPDS by CARD_3:18;
now let x be set;
assume
A3: x in dom the Object-Kind of SCMPDS;
per cases;
suppose
A4: x = li;
then A5: (s+*(li,k)).x = k by A2,A3,FUNCT_7:33;
(the Object-Kind of SCMPDS).x
= ObjectKind li by A4,AMI_1:def 6
.= INT by SCMPDS_2:13;
hence (s+*(li,k)).x in (the Object-Kind of SCMPDS).x by A5,INT_1:12;
suppose x <> li;
then (s+*(li,k)).x = s.x by FUNCT_7:34;
hence (s+*(li,k)).x in (the Object-Kind of SCMPDS).x by A3,CARD_3:18;
end;
hence s+*(li,k) is State of SCMPDS by A1,A2,CARD_3:18;
end;
end;
begin :: The notions of paraclosed,parahalting and their basic properties
definition let I be Program-block;
func stop(I) -> Program-block equals
:Def7: I ';' SCMPDS-Stop;
coherence;
end;
definition let I be Program-block, s be State of SCMPDS;
func IExec(I,s) -> State of SCMPDS equals
Result(s+*Initialized stop(I))
+* s|the Instruction-Locations of SCMPDS;
coherence by AMI_5:82;
end;
definition let I be Program-block;
attr I is paraclosed means
:Def9: for s being State of SCMPDS, n being Nat
st Initialized stop(I) c= s
holds IC (Computation s).n in dom stop(I);
attr I is parahalting means
:Def10: Initialized stop(I) is halting;
end;
Lm1:
Load halt SCMPDS is parahalting
proof
set m = Load halt SCMPDS,
m0= stop (m),
m1 = Initialized m0;
let s;
assume
A1: m1 c= s;
A2: m1 = m0 +* (Start-At inspos 0) by Def2;
dom(Start-At inspos 0) = {IC SCMPDS} by AMI_3:34;
then A3: IC SCMPDS in dom (Start-At inspos 0) by TARSKI:def 1;
then A4: IC SCMPDS in dom m1 by A2,FUNCT_4:13;
A5: m = (inspos 0).--> halt SCMPDS by Def1;
then A6: m.inspos 0 = halt SCMPDS by CQC_LANG:6;
dom m={inspos 0} by A5,CQC_LANG:5;
then A7: inspos 0 in dom m by TARSKI:def 1;
A8: m0= m ';' SCMPDS-Stop by Def7;
then A9: m0= m +* Shift(SCMPDS-Stop,card m) by Def3;
dom m0 misses dom (Start-At inspos 0) by Th54;
then A10: m0 c= m1 by A2,FUNCT_4:33;
A11: inspos 0 in dom m0 by A7,A9,FUNCT_4:13;
then A12: inspos 0 in dom m1 by A2,FUNCT_4:13;
A13: IC m1 = m1.IC SCMPDS by A4,AMI_3:def 16
.= (Start-At inspos 0).IC SCMPDS by A2,A3,FUNCT_4:14
.= inspos 0 by AMI_3:50;
take 0;
thus CurInstr((Computation s).0) = CurInstr s by AMI_1:def 19
.= s.IC s by AMI_1:def 17
.= s.IC m1 by A1,A4,AMI_5:60
.= m1.inspos 0 by A1,A12,A13,GRFUNC_1:8
.= m0.inspos 0 by A10,A11,GRFUNC_1:8
.= halt SCMPDS by A6,A7,A8,Th37;
end;
definition
cluster parahalting Program-block;
existence by Lm1;
end;
theorem Th63: ::TN63
for I being parahalting Program-block
st Initialized stop I c= s holds s is halting
proof
let I be parahalting Program-block; assume
A1: Initialized stop I c= s;
Initialized stop I is halting by Def10;
hence s is halting by A1,AMI_1:def 26;
end;
definition let I be parahalting Program-block;
cluster Initialized stop(I) -> halting;
coherence
proof
let s be State of SCMPDS;
assume Initialized stop I c= s;
hence s is halting by Th63;
end;
end;
definition
let la,lb be Instruction-Location of SCMPDS;
let a, b be Instruction of SCMPDS;
redefine func (la,lb) --> (a,b) -> FinPartState of SCMPDS;
coherence
proof
ObjectKind la = the Instructions of SCMPDS &
ObjectKind lb = the Instructions of SCMPDS by AMI_1:def 14;
hence thesis by AMI_1:58;
end;
end;
canceled;
theorem Th65:
IC s <> Next IC s
proof
assume A1: IC s = Next IC s;
consider mj be Element of SCM-Instr-Loc such that
A2: mj = IC s & Next mj = Next IC s by SCMPDS_2:def 19;
mj+0=mj+2 by A1,A2,AMI_2:def 15;
hence contradiction by XCMPLX_1:2;
end;
theorem Th66: ::TN66
s2 +*((IC s2,Next IC s2) --> (goto 1, goto -1)) is not halting
proof set m=(IC s2,Next IC s2) --> (goto 1, goto -1),
s1 = s2 +* m;
A1: dom m = {IC s2,Next IC s2} by FUNCT_4:65;
then A2: IC s2 in dom m & Next IC s2 in dom m by TARSKI:def 2;
IC s2<>Next IC s2 by Th65;
then A3: m.(IC s2) = goto 1 & m.(Next IC s2)=goto -1 by FUNCT_4:66;
A4: IC SCMPDS <> IC s2 by AMI_1:48;
IC SCMPDS <> Next IC s2 by AMI_1:48;
then A5: not IC SCMPDS in dom m by A1,A4,TARSKI:def 2;
defpred X[Nat] means
IC((Computation s1).$1) = IC s1 or IC((Computation s1).$1) = Next IC s1;
A6: X[0] by AMI_1:def 19;
A7: IC s1 = s1.IC SCMPDS by AMI_1:def 15
.= s2.IC SCMPDS by A5,FUNCT_4:12
.= IC s2 by AMI_1:def 15;
now let n;
set Cn=(Computation s1).n;
assume
A8: IC Cn = IC s1 or IC Cn = Next IC s1;
per cases by A8;
case A9:IC Cn = IC s1;
A10: CurInstr( Cn )
= Cn.IC Cn by AMI_1:def 17
.= s1.IC s1 by A9,AMI_1:54
.= goto 1 by A2,A3,A7,FUNCT_4:14;
thus IC ((Computation s1).(n+1))
= IC Following Cn by AMI_1:def 19
.= IC Exec(goto 1,Cn) by A10,AMI_1:def 18
.= Exec(goto 1,Cn).IC SCMPDS by AMI_1:def 15
.= ICplusConst(Cn,1) by SCMPDS_2:66
.= Next IC s1 by A9,SCMPDS_3:20;
case A11:IC Cn = Next IC s1;
A12: CurInstr((Computation s1).n)
= Cn.IC Cn by AMI_1:def 17
.= s1.(Next IC s1) by A11,AMI_1:54
.= goto -1 by A2,A3,A7,FUNCT_4:14;
consider j be Nat such that
A13: j = IC Cn & ICplusConst(Cn,-1)=abs(j-2+2*(-1))+2
by SCMPDS_2:def 20;
consider mj be Element of SCM-Instr-Loc such that
A14: mj = IC s1 & Next mj = Next IC s1 by SCMPDS_2:def 19;
consider i be Nat such that
A15: IC s1=2*i+2 by SCMPDS_2:1,def 1;
A16: j=2*i+2+2 by A11,A13,A14,A15,AMI_2:def 15
.=2*i+(2+2) by XCMPLX_1:1;
A17: 2*i >= 0 by NAT_1:18;
thus IC((Computation s1).(n+1))
= IC Following Cn by AMI_1:def 19
.= IC Exec(goto -1,Cn ) by A12,AMI_1:def 18
.= Exec(goto -1,Cn ).IC SCMPDS by AMI_1:def 15
.=abs(j-2+ -(2*1))+2 by A13,SCMPDS_2:66
.=abs(j+ -2 + -2)+2 by XCMPLX_0:def 8
.=abs(j+ (-2 + -2))+2 by XCMPLX_1:1
.=abs(2*i+4 + -4 )+2 by A16
.=abs(2*i)+2 by XCMPLX_1:137
.=IC s1 by A15,A17,ABSVALUE:def 1;
end;
then A18: for n st X[n] holds X[n+1];
A19: for n holds X[n] from Ind(A6,A18);
let n;
per cases by A19;
suppose IC((Computation s1).n) = IC s1;
then CurInstr((Computation s1).n)
= ((Computation s1).n).IC s1 by AMI_1:def 17
.= s1.IC s1 by AMI_1:54
.= goto 1 by A2,A3,A7,FUNCT_4:14;
hence CurInstr((Computation s1).n) <> halt SCMPDS by SCMPDS_2:85;
suppose IC((Computation s1).n) = Next IC s1;
then CurInstr((Computation s1).n)
= ((Computation s1).n).Next IC s1 by AMI_1:def 17
.= s1.Next IC s1 by AMI_1:54
.= goto -1 by A2,A3,A7,FUNCT_4:14;
hence CurInstr((Computation s1).n) <> halt SCMPDS by SCMPDS_2:85;
end;
theorem Th67: ::Th21
s1,s2 equal_outside the Instruction-Locations of SCMPDS &
I c= s1 & I c= s2 &
(for m st m < n holds IC ((Computation s2).m) in dom I)
implies
for m st m <= n holds
(Computation s1).m, (Computation s2 ).m equal_outside
the Instruction-Locations of SCMPDS
proof assume that
A1: s1,s2 equal_outside the Instruction-Locations of SCMPDS and
A2: I c= s1 and
A3: I c= s2 and
A4: for m st m < n holds IC((Computation s2).m) in dom I;
defpred X[Nat] means $1 <= n implies
(Computation s1).$1, (Computation s2 ).$1 equal_outside
the Instruction-Locations of SCMPDS;
(Computation s1).0 = s1 & (Computation s2 ).0 = s2 by AMI_1:def 19;
then A5: X[0] by A1;
A6: for m st X[m] holds X[m+1]
proof let m such that
A7: m <= n implies
(Computation s1).m, (Computation s2 ).m equal_outside
the Instruction-Locations of SCMPDS;
A8: (Computation s1).(m+1) = Following((Computation s1).m) by AMI_1:def 19
.= Exec(CurInstr((Computation s1).m),(Computation s1).m)
by AMI_1:def 18;
A9: (Computation s2).(m+1) = Following((Computation s2).m) by AMI_1:def 19
.= Exec(CurInstr((Computation s2).m),(Computation s2).m)
by AMI_1:def 18;
assume A10: m+1 <= n;
then m < n by NAT_1:38;
then A11: IC((Computation s2).m) in dom I by A4;
A12: IC ((Computation s1).m) = IC ((Computation s2).m)
by A7,A10,NAT_1:38,SCMFSA6A:29;
CurInstr((Computation s1).m)
= ((Computation s1).m).IC ((Computation s1).m) by AMI_1:def 17
.= s1.IC((Computation s1).m) by AMI_1:54
.= I.IC((Computation s1).m) by A2,A11,A12,GRFUNC_1:8
.= s2.IC((Computation s2).m) by A3,A11,A12,GRFUNC_1:8
.= ((Computation s2).m).IC ((Computation s2).m) by AMI_1:54
.= CurInstr((Computation s2).m) by AMI_1:def 17;
hence (Computation s1).(m+1), (Computation s2 ).(m+1) equal_outside
the Instruction-Locations of SCMPDS by A7,A8,A9,A10,Th15,NAT_1:38;
end;
thus for m holds X[m] from Ind(A5,A6);
end;
theorem Th68:
for s being State of SCMPDS,l being Instruction-Location of SCMPDS
holds l in dom s
proof
let s be State of SCMPDS,l be Instruction-Location of SCMPDS;
l in {IC SCMPDS} \/ SCM-Data-Loc \/ the Instruction-Locations of SCMPDS
by XBOOLE_0:def 2;
hence l in dom s by AMI_3:36,SCMPDS_3:5;
end;
reserve l1,l2 for Instruction-Location of SCMPDS,
i1,i2 for Instruction of SCMPDS;
theorem Th69:
s +*((l1,l2) --> (i1, i2)) = s +* (l1,i1) +* (l2,i2)
proof
A1: l1 in dom s by Th68;
l2 in dom s by Th68;
then A2: l2 in dom (s +* (l1,i1)) by FUNCT_7:32;
thus s +*((l1,l2) --> (i1, i2))
=s +* ((l1 .--> i1) +* (l2 .--> i2)) by AMI_1:18
.=s +* (l1 .--> i1) +* (l2 .--> i2) by FUNCT_4:15
.=s +* (l1,i1) +* (l2 .--> i2) by A1,FUNCT_7:def 3
.=s +* (l1,i1) +* (l2,i2) by A2,FUNCT_7:def 3;
end;
theorem Th70:
Next inspos n = inspos(n+1)
proof
A1: inspos n = il.n & inspos(n+1) = il.(n+1) by SCMPDS_3:def 2;
consider l be Element of SCM-Instr-Loc such that
A2: l = inspos n and
A3: Next l = Next inspos n by SCMPDS_2:def 19;
thus Next inspos n=Next il.n by A1,A2,A3,AMI_3:6
.=inspos(n+1) by A1,AMI_3:54;
end;
theorem Th71:
not IC s in dom I implies not Next IC s in dom I
proof
assume A1: not IC s in dom I;
consider m be Nat such that
A2: IC s=inspos m by SCMPDS_3:32;
A3: m >= card I by A1,A2,Th1;
A4: Next IC s=inspos(m+1) by A2,Th70;
m+1 >= m by NAT_1:29;
then m+1 >= card I by A3,AXIOMS:22;
hence thesis by A4,Th1;
end;
definition
cluster parahalting -> paraclosed Program-block;
coherence proof
let I be Program-block; assume
A1: I is parahalting;
let s be State of SCMPDS, n be Nat;
assume
A2: Initialized stop(I) c= s;
defpred X[Nat] means not IC (Computation s).$1 in dom stop(I);
assume not IC (Computation s).n in dom stop(I);
then A3: ex n st X[n];
consider n such that
A4: X[n] and
A5: for m st X[m] holds n <= m from Min(A3);
A6: not Next IC (Computation s).n in dom stop(I) by A4,Th71;
set s2 = (Computation s).n,
Ig = ((IC s2,Next IC s2) --> (goto 1, goto -1)),
s0 = s +* Ig,
s1 = s2 +* Ig,
t1= s +* (IC s2,goto 1),
t2= t1 +* (Next IC s2,goto -1),
t3= s2 +* (IC s2,goto 1),
t4= t3 +* (Next IC s2,goto -1),
IL=the Instruction-Locations of SCMPDS;
set IAt = stop(I) +* Start-At inspos 0;
dom stop(I) misses dom Start-At inspos 0 by Th54;
then A7: stop I c= IAt by FUNCT_4:33;
A8: Initialized stop(I) = IAt by Def2;
then A9: IAt is halting by A1,Def10;
(IAt) | IL = stop I by Th58;
then A10: dom stop (I) = dom(IAt) /\ IL
by RELAT_1:90;
then A11: not IC s2 in dom IAt by A4,XBOOLE_0:def 3;
A12: not Next IC s2 in dom IAt by A6,A10,XBOOLE_0:def 3;
IAt c= t1 by A2,A8,A11,SCMFSA6A:1;
then IAt c= t2 by A12,SCMFSA6A:1;
then A13: IAt c= s0 by Th69;
then A14: s0 is halting by A9,AMI_1:def 26;
A15: s,t1 equal_outside IL by SCMFSA6A:3;
t1,t2 equal_outside IL by SCMFSA6A:3;
then s,t2 equal_outside IL by A15,FUNCT_7:29;
then s,s0 equal_outside IL by Th69;
then A16: s0,s equal_outside IL by FUNCT_7:28;
A17: stop I c= s0 by A7,A13,XBOOLE_1:1;
A18: stop I c= s by A2,A7,A8,XBOOLE_1:1;
for m st m < n holds IC((Computation s).m) in dom stop I by A5;
then A19: (Computation s0).n,s2 equal_outside IL by A16,A17,A18,Th67;
A20: s2,t3 equal_outside IL by SCMFSA6A:3;
t3,t4 equal_outside IL by SCMFSA6A:3;
then s2,t4 equal_outside IL by A20,FUNCT_7:29;
then s2,s1 equal_outside IL by Th69;
then A21: (Computation s0).n, s1 equal_outside IL by A19,FUNCT_7:29;
s| IL = s2 | IL by SCMFSA6B:17;
then t1 | IL = t3 | IL by SCMFSA6A:5;
then t2 | IL = t4 | IL by SCMFSA6A:5;
then s0 | IL = t4 | IL by Th69;
then s0 | IL = s1 | IL by Th69;
then (Computation s0).n | IL = s1 | IL by SCMFSA6B:17;
then A22: (Computation s0).n = s1 by A21,SCMFSA6A:2;
s1 is not halting by Th66;
hence contradiction by A14,A22,SCM_1:27;
end;
end;
theorem Th72: :: SCMFSA8A_15
dom SCMPDS-Stop = {inspos 0} by CQC_LANG:5,SCMPDS_3:def 6;
theorem ::S8A_16
inspos 0 in dom SCMPDS-Stop & SCMPDS-Stop.inspos 0 = halt SCMPDS
by Th72,CQC_LANG:6,SCMPDS_3:def 6,TARSKI:def 1;
theorem Th74:
card SCMPDS-Stop = 1
proof
thus card SCMPDS-Stop = card dom SCMPDS-Stop by PRE_CIRC:21
.= 1 by Th72,CARD_1:79;
end;
theorem Th75: ::Th26 T9
inspos 0 in dom stop (I)
proof
card stop I =card (I ';' SCMPDS-Stop) by Def7
.=card I + 1 by Th45,Th74;
then 1 <= card stop I by NAT_1:29;
then 0 < card stop I by AXIOMS:22;
hence thesis by Th1;
end;
theorem Th76:
for p being programmed FinPartState of SCMPDS,k being Nat,
il be Instruction-Location of SCMPDS st il in dom p holds
il+k in dom Shift(p,k)
proof
let p be programmed FinPartState of SCMPDS,k be Nat,
il be Instruction-Location of SCMPDS;
assume A1: il in dom p;
dom Shift(p,k) = { loc+k : loc in dom p} by SCMPDS_3:38;
hence thesis by A1;
end;
begin :: Shiftability of program blocks and instructions
definition
let i be Instruction of SCMPDS;
let n be Nat;
pred i valid_at n means
:Def11: (InsCode i= 0 implies ex k1 st i = goto k1 & n+k1 >= 0) &
(InsCode i= 4 implies ex a,k1,k2 st i = (a,k1)<>0_goto k2 & n+k2 >= 0 ) &
(InsCode i= 5 implies ex a,k1,k2 st i = (a,k1)<=0_goto k2 & n+k2 >= 0 ) &
(InsCode i= 6 implies ex a,k1,k2 st i = (a,k1)>=0_goto k2 & n+k2 >= 0);
end;
reserve l for Nat;
theorem Th77:
for i be Instruction of SCMPDS,m,n be Nat st i valid_at m & m <= n
holds i valid_at n
proof
let i be Instruction of SCMPDS,m,n be Nat;
assume A1:i valid_at m & m <= n;
A2: now
assume InsCode i= 0;
then consider k1 such that
A3: i=goto k1 & m+k1 >= 0 by A1,Def11;
take k1;
thus i=goto k1 by A3;
thus n+k1 >= 0 by A1,A3,AXIOMS:24;
end;
A4: now
assume InsCode i= 4;
then consider a,k1,k2 such that
A5: i = (a,k1)<>0_goto k2 & m+k2 >= 0 by A1,Def11;
take a,k1,k2;
thus i = (a,k1)<>0_goto k2 by A5;
thus n+k2 >= 0 by A1,A5,AXIOMS:24;
end;
A6: now
assume InsCode i= 5;
then consider a,k1,k2 such that
A7: i = (a,k1)<=0_goto k2 & m+k2 >= 0 by A1,Def11;
take a,k1,k2;
thus i = (a,k1)<=0_goto k2 by A7;
thus n+k2 >= 0 by A1,A7,AXIOMS:24;
end;
now
assume InsCode i= 6;
then consider a,k1,k2 such that
A8: i = (a,k1)>=0_goto k2 & m+k2 >= 0 by A1,Def11;
take a,k1,k2;
thus i = (a,k1)>=0_goto k2 by A8;
thus n+k2 >= 0 by A1,A8,AXIOMS:24;
end;
hence thesis by A2,A4,A6,Def11;
end;
definition let IT be FinPartState of SCMPDS;
attr IT is shiftable means
:Def12: for n,i st inspos n in dom IT & i=IT.(inspos n) holds
InsCode i <> 1 & InsCode i <> 3 & :: return and save
i valid_at n;
end;
Lm2:
Load halt SCMPDS is shiftable
proof
set m = Load halt SCMPDS;
A1: m = (inspos 0).--> halt SCMPDS by Def1;
then A2: m.inspos 0 = halt SCMPDS by CQC_LANG:6;
A3: dom m={inspos 0} by A1,CQC_LANG:5;
now let n,i;
assume A4:inspos n in dom m & i=m.(inspos n);
then A5: inspos n= inspos 0 by A3,TARSKI:def 1;
then A6: InsCode i =0 by A2,A4,SCMPDS_2:21,93;
thus InsCode i <> 1 by A2,A4,A5,SCMPDS_2:21,93;
thus InsCode i <> 3 by A2,A4,A5,SCMPDS_2:21,93;
ex k1 st i = goto k1 & n+k1 >= 0
proof
take 0;
thus i=goto 0 by A1,A4,A5,CQC_LANG:6,SCMPDS_2:93;
thus n+0>=0 by A5,SCMPDS_3:31;
end;
hence i valid_at n by A6,Def11;
end;
hence thesis by Def12;
end;
definition
cluster parahalting shiftable Program-block;
existence by Lm1,Lm2;
end;
definition let i be Instruction of SCMPDS;
attr i is shiftable means
:Def13: InsCode i = 2 or InsCode i > 6;
end;
definition
cluster shiftable Instruction of SCMPDS;
existence
proof
take i=DataLoc(0,0):=1;
InsCode i=2 by SCMPDS_2:23;
hence thesis by Def13;
end;
end;
definition
let a,k1;
cluster a := k1 -> shiftable;
coherence
proof
InsCode (a:=k1)=2 by SCMPDS_2:23;
hence thesis by Def13;
end;
end;
definition
let a,k1,k2;
cluster (a,k1) := k2 -> shiftable;
coherence
proof
InsCode ((a,k1) := k2)=7 by SCMPDS_2:28;
hence thesis by Def13;
end;
end;
definition
let a,k1,k2;
cluster AddTo(a,k1,k2) -> shiftable;
coherence
proof
InsCode AddTo(a,k1,k2)=8 by SCMPDS_2:29;
hence thesis by Def13;
end;
end;
definition
let a,b,k1,k2;
cluster AddTo(a,k1,b,k2) -> shiftable;
coherence
proof
InsCode AddTo(a,k1,b,k2)=9 by SCMPDS_2:30;
hence thesis by Def13;
end;
cluster SubFrom(a,k1,b,k2) -> shiftable;
coherence
proof
InsCode SubFrom(a,k1,b,k2)=10 by SCMPDS_2:31;
hence thesis by Def13;
end;
cluster MultBy(a,k1,b,k2) -> shiftable;
coherence
proof
InsCode MultBy(a,k1,b,k2)=11 by SCMPDS_2:32;
hence thesis by Def13;
end;
cluster Divide(a,k1,b,k2) -> shiftable;
coherence
proof
InsCode Divide(a,k1,b,k2)=12 by SCMPDS_2:33;
hence thesis by Def13;
end;
cluster (a,k1) := (b,k2) -> shiftable;
coherence
proof
InsCode (a,k1) := (b,k2)=13 by SCMPDS_2:34;
hence thesis by Def13;
end;
end;
definition
let I,J be shiftable Program-block;
cluster I ';' J -> shiftable;
coherence
proof
set IJ=I ';' J;
A1: I ';' J = I +* Shift(J,card I) by Def3;
now let n,i such that
A2: inspos n in dom IJ and
A3: i=IJ.(inspos n);
set D = {inspos(l+card I): inspos l in dom J };
dom Shift(J,card I) = D by SCMPDS_3:def 7;
then A4: dom IJ = dom I \/ D by A1,FUNCT_4:def 1;
per cases by A2,A4,XBOOLE_0:def 2;
suppose A5:inspos n in dom I;
then I.inspos n=i by A3,Th37;
hence InsCode i <> 1 & InsCode i <> 3 & i valid_at n by A5,Def12;
suppose inspos n in D;
then consider l such that
A6: inspos n = inspos(l+card I) and
A7: inspos l in dom J;
A8: J.inspos l=IJ.(inspos l+card I) by A7,Th38
.=i by A3,A6,SCMPDS_3:def 3;
hence InsCode i <> 1 & InsCode i <> 3 by A7,Def12;
l <= l+card I by NAT_1:29;
then A9: l <= n by A6,SCMPDS_3:31;
i valid_at l by A7,A8,Def12;
hence i valid_at n by A9,Th77;
end;
hence thesis by Def12;
end;
end;
definition
let i be shiftable Instruction of SCMPDS;
cluster Load i -> shiftable;
coherence
proof
set p=Load i;
now let n,j such that
A1: inspos n in dom p and
A2: j=p.inspos n;
A3: p=inspos 0 .--> i by Def1;
then dom p = { inspos 0 } by CQC_LANG:5;
then inspos n = inspos 0 by A1,TARSKI:def 1;
then A4: j=i by A2,A3,CQC_LANG:6;
then A5: InsCode j=2 or InsCode j > 6 by Def13;
thus InsCode j <> 1 by A4,Def13;
thus InsCode j <> 3 by A4,Def13;
A6: InsCode j <> 0 by A4,Def13;
A7: InsCode j <> 4 by A4,Def13;
InsCode j <> 5 by A4,Def13;
hence j valid_at n by A5,A6,A7,Def11;
end;
hence thesis by Def12;
end;
end;
definition
let i be shiftable Instruction of SCMPDS,
J be shiftable Program-block;
cluster i ';' J -> shiftable;
coherence
proof
i ';' J=Load i ';' J by Def4;
hence thesis;
end;
end;
definition
let I be shiftable Program-block,
j be shiftable Instruction of SCMPDS;
cluster I ';' j -> shiftable;
coherence
proof
I ';' j=I ';' Load j by Def5;
hence thesis;
end;
end;
definition
let i,j be shiftable Instruction of SCMPDS;
cluster i ';' j -> shiftable;
coherence
proof
i ';' j=Load i ';' Load j by Def6;
hence thesis;
end;
end;
definition
cluster SCMPDS-Stop -> parahalting shiftable;
coherence by Def1,Lm1,Lm2,SCMPDS_3:def 6;
end;
definition
let I be shiftable Program-block;
cluster stop I -> shiftable;
coherence
proof
stop I= I ';' SCMPDS-Stop by Def7;
hence thesis;
end;
end;
theorem
for I being shiftable Program-block,k1 be Integer st
card I + k1 >= 0 holds I ';' goto k1 is shiftable
proof
let I be shiftable Program-block,k1 be Integer;
assume A1: card I + k1 >= 0;
set J= Load goto k1;
set Ig=I ';' goto k1;
A2: Ig=I ';' J by Def5;
then A3: Ig=I +* Shift(J,card I) by Def3;
now let n,i such that
A4: inspos n in dom Ig and
A5: i=Ig.(inspos n);
set D = {inspos(l+card I): inspos l in dom J };
dom Shift(J,card I) = D by SCMPDS_3:def 7;
then A6: dom Ig = dom I \/ D by A3,FUNCT_4:def 1;
per cases by A4,A6,XBOOLE_0:def 2;
suppose A7:inspos n in dom I;
then I.inspos n=i by A2,A5,Th37;
hence InsCode i <> 1 & InsCode i <> 3 & i valid_at n by A7,Def12;
suppose inspos n in D;
then consider l such that
A8: inspos n = inspos(l+card I) and
A9: inspos l in dom J;
A10: J=inspos 0 .--> goto k1 by Def1;
then dom J = { inspos 0 } by CQC_LANG:5;
then A11: inspos l = inspos 0 by A9,TARSKI:def 1;
then A12: goto k1 =J.inspos l by A10,CQC_LANG:6
.=Ig.(inspos l+card I) by A2,A9,Th38
.=i by A5,A8,SCMPDS_3:def 3;
hence InsCode i <> 1 & InsCode i <> 3 by SCMPDS_2:21;
inspos n= inspos(0+card I) by A8,A11,SCMPDS_3:31;
then A13: n+k1 >=0 by A1,SCMPDS_3:31;
InsCode i <> 4 & InsCode i <> 5 & InsCode i <> 6 by A12,SCMPDS_2:21;
hence i valid_at n by A12,A13,Def11;
end;
hence thesis by Def12;
end;
definition
let n be Nat;
cluster Load goto n -> shiftable;
coherence
proof
set k1=n;
set J= Load goto k1;
now let n,i such that
A1: inspos n in dom J and
A2: i=J.inspos n;
A3: J=inspos 0 .--> goto k1 by Def1;
then dom J = { inspos 0 } by CQC_LANG:5;
then inspos n = inspos 0 by A1,TARSKI:def 1;
then A4: goto k1 =i by A2,A3,CQC_LANG:6;
hence InsCode i <> 1 & InsCode i <> 3 by SCMPDS_2:21;
A5: n+k1 >=0 by NAT_1:18;
InsCode i <> 4 & InsCode i <> 5 & InsCode i <> 6 by A4,SCMPDS_2:21;
hence i valid_at n by A4,A5,Def11;
end;
hence thesis by Def12;
end;
end;
theorem
for I being shiftable Program-block,k1,k2 be Integer,a be Int_position st
card I + k2 >= 0 holds I ';' (a,k1)<>0_goto k2 is shiftable
proof
let I be shiftable Program-block,k1,k2 be Integer,a be Int_position;
assume A1: card I + k2 >= 0;
set ii= (a,k1)<>0_goto k2,
J= Load ii;
set Ig=I ';' ii;
A2: Ig=I ';' J by Def5;
then A3: Ig=I +* Shift(J,card I) by Def3;
now let n,i such that
A4: inspos n in dom Ig and
A5: i=Ig.(inspos n);
set D = {inspos(l+card I): inspos l in dom J };
dom Shift(J,card I) = D by SCMPDS_3:def 7;
then A6: dom Ig = dom I \/ D by A3,FUNCT_4:def 1;
per cases by A4,A6,XBOOLE_0:def 2;
suppose A7:inspos n in dom I;
then I.inspos n=i by A2,A5,Th37;
hence InsCode i <> 1 & InsCode i <> 3 & i valid_at n by A7,Def12;
suppose inspos n in D;
then consider l such that
A8: inspos n = inspos(l+card I) and
A9: inspos l in dom J;
A10: J=inspos 0 .--> ii by Def1;
then dom J = { inspos 0 } by CQC_LANG:5;
then A11: inspos l = inspos 0 by A9,TARSKI:def 1;
then A12: ii=J.inspos l by A10,CQC_LANG:6
.=Ig.(inspos l+card I) by A2,A9,Th38
.=i by A5,A8,SCMPDS_3:def 3;
hence InsCode i <> 1 & InsCode i <> 3 by SCMPDS_2:25;
inspos n= inspos(0+card I) by A8,A11,SCMPDS_3:31;
then A13: n+k2 >=0 by A1,SCMPDS_3:31;
InsCode i <> 0 & InsCode i <> 5 & InsCode i <> 6 by A12,SCMPDS_2:25;
hence i valid_at n by A12,A13,Def11;
end;
hence thesis by Def12;
end;
definition
let k1 be Integer,a be Int_position,n be Nat;
cluster Load (a,k1)<>0_goto n -> shiftable;
coherence
proof
set k2=n;
set ii= (a,k1)<>0_goto k2,
J= Load ii;
now let n,i such that
A1: inspos n in dom J and
A2: i=J.inspos n;
A3: J=inspos 0 .--> ii by Def1;
then dom J = { inspos 0 } by CQC_LANG:5;
then inspos n = inspos 0 by A1,TARSKI:def 1;
then A4: ii =i by A2,A3,CQC_LANG:6;
hence InsCode i <> 1 & InsCode i <> 3 by SCMPDS_2:25;
A5: n+k2 >=0 by NAT_1:18;
InsCode i <> 0 & InsCode i <> 5 & InsCode i <> 6 by A4,SCMPDS_2:25;
hence i valid_at n by A4,A5,Def11;
end;
hence thesis by Def12;
end;
end;
theorem
for I being shiftable Program-block,k1,k2 be Integer,a be Int_position st
card I + k2 >= 0 holds I ';' (a,k1)<=0_goto k2 is shiftable
proof
let I be shiftable Program-block,k1,k2 be Integer,a be Int_position;
assume A1: card I + k2 >= 0;
set ii= (a,k1)<=0_goto k2,
J= Load ii;
set Ig=I ';' ii;
A2: Ig=I ';' J by Def5;
then A3: Ig=I +* Shift(J,card I) by Def3;
now let n,i such that
A4: inspos n in dom Ig and
A5: i=Ig.(inspos n);
set D = {inspos(l+card I): inspos l in dom J };
dom Shift(J,card I) = D by SCMPDS_3:def 7;
then A6: dom Ig = dom I \/ D by A3,FUNCT_4:def 1;
per cases by A4,A6,XBOOLE_0:def 2;
suppose A7:inspos n in dom I;
then I.inspos n=i by A2,A5,Th37;
hence InsCode i <> 1 & InsCode i <> 3 & i valid_at n by A7,Def12;
suppose inspos n in D;
then consider l such that
A8: inspos n = inspos(l+card I) and
A9: inspos l in dom J;
A10: J=inspos 0 .--> ii by Def1;
then dom J = { inspos 0 } by CQC_LANG:5;
then A11: inspos l = inspos 0 by A9,TARSKI:def 1;
then A12: ii =J.inspos l by A10,CQC_LANG:6
.=Ig.(inspos l+card I) by A2,A9,Th38
.=i by A5,A8,SCMPDS_3:def 3;
hence InsCode i <> 1 & InsCode i <> 3 by SCMPDS_2:26;
inspos n= inspos(0+card I) by A8,A11,SCMPDS_3:31;
then A13: n+k2 >=0 by A1,SCMPDS_3:31;
InsCode i <> 0 & InsCode i <> 4 & InsCode i <> 6 by A12,SCMPDS_2:26;
hence i valid_at n by A12,A13,Def11;
end;
hence thesis by Def12;
end;
definition
let k1 be Integer,a be Int_position,n be Nat;
cluster Load (a,k1)<=0_goto n -> shiftable;
coherence
proof
set k2=n;
set ii= (a,k1)<=0_goto k2,
J= Load ii;
now let n,i such that
A1: inspos n in dom J and
A2: i=J.inspos n;
A3: J=inspos 0 .--> ii by Def1;
then dom J = { inspos 0 } by CQC_LANG:5;
then inspos n = inspos 0 by A1,TARSKI:def 1;
then A4: ii =i by A2,A3,CQC_LANG:6;
hence InsCode i <> 1 & InsCode i <> 3 by SCMPDS_2:26;
A5: n+k2 >=0 by NAT_1:18;
InsCode i <> 0 & InsCode i <> 4 & InsCode i <> 6 by A4,SCMPDS_2:26;
hence i valid_at n by A4,A5,Def11;
end;
hence thesis by Def12;
end;
end;
theorem
for I being shiftable Program-block,k1,k2 be Integer,a be Int_position st
card I + k2 >= 0 holds I ';' (a,k1)>=0_goto k2 is shiftable
proof
let I be shiftable Program-block,k1,k2 be Integer,a be Int_position;
assume A1: card I + k2 >= 0;
set ii= (a,k1)>=0_goto k2,
J= Load ii;
set Ig=I ';' ii;
A2: Ig=I ';' J by Def5;
then A3: Ig=I +* Shift(J,card I) by Def3;
now let n,i such that
A4: inspos n in dom Ig and
A5: i=Ig.(inspos n);
set D = {inspos(l+card I): inspos l in dom J };
dom Shift(J,card I) = D by SCMPDS_3:def 7;
then A6: dom Ig = dom I \/ D by A3,FUNCT_4:def 1;
per cases by A4,A6,XBOOLE_0:def 2;
suppose A7:inspos n in dom I;
then I.inspos n=i by A2,A5,Th37;
hence InsCode i <> 1 & InsCode i <> 3 & i valid_at n by A7,Def12;
suppose inspos n in D;
then consider l such that
A8: inspos n = inspos(l+card I) and
A9: inspos l in dom J;
A10: J=inspos 0 .--> ii by Def1;
then dom J = { inspos 0 } by CQC_LANG:5;
then A11: inspos l = inspos 0 by A9,TARSKI:def 1;
then A12: ii =J.inspos l by A10,CQC_LANG:6
.=Ig.(inspos l+card I) by A2,A9,Th38
.=i by A5,A8,SCMPDS_3:def 3;
hence InsCode i <> 1 & InsCode i <> 3 by SCMPDS_2:27;
inspos n= inspos(0+card I) by A8,A11,SCMPDS_3:31;
then A13: n+k2 >=0 by A1,SCMPDS_3:31;
InsCode i <> 0 & InsCode i <> 4 & InsCode i <> 5 by A12,SCMPDS_2:27;
hence i valid_at n by A12,A13,Def11;
end;
hence thesis by Def12;
end;
definition
let k1 be Integer,a be Int_position,n be Nat;
cluster Load (a,k1)>=0_goto n -> shiftable;
coherence
proof
set k2=n;
set ii= (a,k1)>=0_goto k2,
J= Load ii;
now let n,i such that
A1: inspos n in dom J and
A2: i=J.inspos n;
A3: J=inspos 0 .--> ii by Def1;
then dom J = { inspos 0 } by CQC_LANG:5;
then inspos n = inspos 0 by A1,TARSKI:def 1;
then A4: ii =i by A2,A3,CQC_LANG:6;
hence InsCode i <> 1 & InsCode i <> 3 by SCMPDS_2:27;
A5: n+k2 >=0 by NAT_1:18;
InsCode i <> 0 & InsCode i <> 4 & InsCode i <> 5 by A4,SCMPDS_2:27;
hence i valid_at n by A4,A5,Def11;
end;
hence thesis by Def12;
end;
end;
theorem Th82:
for s1,s2 being State of SCMPDS, n,m being Nat,k1 be Integer st
IC s1=inspos m & m+k1>=0 & IC s1 + n = IC s2
holds ICplusConst(s1,k1) +n = ICplusConst(s2,k1)
proof
let s1,s2 be State of SCMPDS, n,m be Nat,k1 be Integer;
assume that
A1: IC s1=inspos m and
A2: m+k1>=0 and
A3: IC s1 + n = IC s2;
consider n1 be Nat such that
A4: n1 = IC s1 & ICplusConst(s1,k1) = abs(n1-2+2*k1)+2 by SCMPDS_2:def 20;
consider n2 be Nat such that
A5: n2 = IC s2 & ICplusConst(s2,k1) = abs(n2-2+2*k1)+2 by SCMPDS_2:def 20;
reconsider mk=m+k1 as Nat by A2,INT_1:16;
A6: 2*mk >= 0 by NAT_1:18;
A7: 2*mk + 2*n >= 0 by NAT_1:18;
A8: n2=inspos ( m + n) by A1,A3,A5,SCMPDS_3:def 3
.=il.(m+n) by SCMPDS_3:def 2
.=2*(m+n)+2 by AMI_3:def 20;
consider nk be Nat such that
A9: inspos nk=ICplusConst(s1,k1) by SCMPDS_3:32;
A10: n1=il.m by A1,A4,SCMPDS_3:def 2
.=2*m+2 by AMI_3:def 20;
2*nk+2=il.nk by AMI_3:def 20
.=abs(n1-2+2*k1)+2 by A4,A9,SCMPDS_3:def 2;
then A11: 2*nk=abs(2*m+2-2+2*k1) by A10,XCMPLX_1:2
.=abs(2*m+2*k1) by XCMPLX_1:26
.=abs(2*mk) by XCMPLX_1:8
.=2*mk by A6,ABSVALUE:def 1;
thus ICplusConst(s1,k1) +n=inspos(nk +n) by A9,SCMPDS_3:def 3
.=il.(nk+n) by SCMPDS_3:def 2
.=2*(nk+n)+2 by AMI_3:def 20
.=2*mk+2*n+2 by A11,XCMPLX_1:8
.=abs(2*mk+2*n)+2 by A7,ABSVALUE:def 1
.=abs(2*m+2*k1+2*n)+2 by XCMPLX_1:8
.=abs(2*m+2*n+2*k1)+2 by XCMPLX_1:1
.=abs(2*(m+n)+2*k1)+2 by XCMPLX_1:8
.=ICplusConst(s2,k1) by A5,A8,XCMPLX_1:26;
end;
theorem Th83: ::S6A_41
for s1,s2 being State of SCMPDS, n,m being Nat,
i being Instruction of SCMPDS holds
IC s1=inspos m & i valid_at m & InsCode i <> 1 & InsCode i <> 3 &
IC s1 + n = IC s2 &
s1 | SCM-Data-Loc = s2 | SCM-Data-Loc
implies
IC Exec(i,s1) + n = IC Exec(i,s2) &
Exec(i,s1) | SCM-Data-Loc = Exec(i,s2) | SCM-Data-Loc
proof
let s1,s2 be State of SCMPDS, n ,m be Nat;
let i be Instruction of SCMPDS; assume that
A1: IC s1=inspos m and
A2: i valid_at m and
A3: InsCode i <> 1 and
A4: InsCode i <> 3 and
A5: IC s1 + n = IC s2 and
A6:s1 | SCM-Data-Loc = s2 | SCM-Data-Loc;
set D = SCM-Data-Loc;
consider k1 being Nat such that
A7: IC s1 = inspos k1 by SCMPDS_3:32;
A8: Next IC s1 + n = Next IC s2
proof
thus Next IC s1 + n = inspos (k1 + 1) + n by A7,Th70
.= inspos (k1 + 1 + n) by SCMPDS_3:def 3
.= inspos (k1 + n + 1) by XCMPLX_1:1
.= Next inspos (k1 + n) by Th70
.= Next (IC s2) by A5,A7,SCMPDS_3:def 3;
end;
set Ci=InsCode i;
A9:now assume
Ci <> 0 & Ci<>1 & Ci<>4 & Ci<>5 & Ci<> 6;
then A10: not Ci in {0,1,4,5,6} by ENUMSET1:23;
IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
.= Next IC s1 by A10,Th6;
hence IC Exec(i,s1) + n = Exec(i,s2).IC SCMPDS by A8,A10,Th6
.= IC Exec(i,s2) by AMI_1:def 15;
end;
A11: now let a,k1;
thus s1.DataLoc(s1.a,k1) =s1.DataLoc(s2.a,k1) by A6,Th23
.=s2.DataLoc(s2.a,k1) by A6,Th23;
end;
A12: Ci <= 13 by SCMPDS_2:15;
per cases by A3,A4,A12,SCMPDS_3:1;
suppose Ci = 0;
then consider k1 such that
A13: i = goto k1 & m+k1 >= 0 by A2,Def11;
A14: now let a;
thus Exec(i, s1).a = s1.a by A13,SCMPDS_2:66
.=s2.a by A6,Th23
.=Exec(i, s2).a by A13,SCMPDS_2:66;
end;
IC Exec(i,s1) = (Exec(i,s1).IC SCMPDS) by AMI_1:def 15
.= ICplusConst(s1,k1) by A13,SCMPDS_2:66;
hence IC Exec(i,s1) + n = ICplusConst(s2,k1) by A1,A5,A13,Th82
.= Exec(i,s2).IC SCMPDS by A13,SCMPDS_2:66
.= IC Exec(i,s2) by AMI_1:def 15;
thus Exec(i,s1) | D = Exec(i,s2) | D by A14,Th23;
suppose A15: Ci = 2;
then consider a,k1 such that
A16: i = a := k1 by SCMPDS_2:37;
A17: now let b;
per cases;
suppose A18:a=b;
hence Exec(i, s1).b= k1 by A16,SCMPDS_2:57
.=Exec(i,s2).b by A16,A18,SCMPDS_2:57;
suppose A19:a<>b;
hence Exec(i,s1).b = s1.b by A16,SCMPDS_2:57
.=s2.b by A6,Th23
.=Exec(i,s2).b by A16,A19,SCMPDS_2:57;
end;
thus IC Exec(i,s1) + n = IC Exec(i,s2) by A9,A15;
thus Exec(i,s1) | D = Exec(i,s2) | D by A17,Th23;
suppose Ci = 4;
then consider a,k1,k2 such that
A20: i = (a,k1)<>0_goto k2 & m+k2 >= 0 by A2,Def11;
A21: now let a;
thus Exec(i, s1).a = s1.a by A20,SCMPDS_2:67
.=s2.a by A6,Th23
.=Exec(i, s2).a by A20,SCMPDS_2:67;
end;
hereby
per cases;
suppose A22:s1.DataLoc(s1.a,k1) <> 0;
then A23:s2.DataLoc(s2.a,k1) <> 0 by A11;
IC Exec(i,s1) = (Exec(i,s1).IC SCMPDS) by AMI_1:def 15
.= ICplusConst(s1,k2) by A20,A22,SCMPDS_2:67;
hence IC Exec(i,s1) + n = ICplusConst(s2,k2) by A1,A5,A20,Th82
.= Exec(i,s2).IC SCMPDS by A20,A23,SCMPDS_2:67
.= IC Exec(i,s2) by AMI_1:def 15;
suppose A24:s1.DataLoc(s1.a,k1) = 0;
then A25:s2.DataLoc(s2.a,k1) = 0 by A11;
IC Exec(i,s1) = (Exec(i,s1).IC SCMPDS) by AMI_1:def 15
.= Next IC s1 by A20,A24,SCMPDS_2:67;
hence IC Exec(i,s1) + n = Exec(i,s2).IC SCMPDS by A8,A20,A25,SCMPDS_2:
67
.= IC Exec(i,s2) by AMI_1:def 15;
end;
thus Exec(i,s1) | D = Exec(i,s2) | D by A21,Th23;
suppose Ci = 5;
then consider a,k1,k2 such that
A26: i = (a,k1)<=0_goto k2 & m+k2 >= 0 by A2,Def11;
A27: now let a;
thus Exec(i, s1).a = s1.a by A26,SCMPDS_2:68
.=s2.a by A6,Th23
.=Exec(i, s2).a by A26,SCMPDS_2:68;
end;
hereby
per cases;
suppose A28:s1.DataLoc(s1.a,k1) <= 0;
then A29:s2.DataLoc(s2.a,k1) <= 0 by A11;
IC Exec(i,s1) = (Exec(i,s1).IC SCMPDS) by AMI_1:def 15
.= ICplusConst(s1,k2) by A26,A28,SCMPDS_2:68;
hence IC Exec(i,s1) + n = ICplusConst(s2,k2) by A1,A5,A26,Th82
.= Exec(i,s2).IC SCMPDS by A26,A29,SCMPDS_2:68
.= IC Exec(i,s2) by AMI_1:def 15;
suppose A30:s1.DataLoc(s1.a,k1) > 0;
then A31:s2.DataLoc(s2.a,k1) > 0 by A11;
IC Exec(i,s1) = (Exec(i,s1).IC SCMPDS) by AMI_1:def 15
.= Next IC s1 by A26,A30,SCMPDS_2:68;
hence IC Exec(i,s1) + n = Exec(i,s2).IC SCMPDS by A8,A26,A31,SCMPDS_2:
68
.= IC Exec(i,s2) by AMI_1:def 15;
end;
thus Exec(i,s1) | D = Exec(i,s2) | D by A27,Th23;
suppose Ci = 6;
then consider a,k1,k2 such that
A32: i = (a,k1)>=0_goto k2 & m+k2 >= 0 by A2,Def11;
A33: now let a;
thus Exec(i, s1).a = s1.a by A32,SCMPDS_2:69
.=s2.a by A6,Th23
.=Exec(i, s2).a by A32,SCMPDS_2:69;
end;
hereby
per cases;
suppose A34:s1.DataLoc(s1.a,k1) >= 0;
then A35:s2.DataLoc(s2.a,k1) >= 0 by A11;
IC Exec(i,s1) = (Exec(i,s1).IC SCMPDS) by AMI_1:def 15
.= ICplusConst(s1,k2) by A32,A34,SCMPDS_2:69;
hence IC Exec(i,s1) + n = ICplusConst(s2,k2) by A1,A5,A32,Th82
.= Exec(i,s2).IC SCMPDS by A32,A35,SCMPDS_2:69
.= IC Exec(i,s2) by AMI_1:def 15;
suppose A36:s1.DataLoc(s1.a,k1) < 0;
then A37:s2.DataLoc(s2.a,k1) < 0 by A11;
IC Exec(i,s1) = (Exec(i,s1).IC SCMPDS) by AMI_1:def 15
.= Next IC s1 by A32,A36,SCMPDS_2:69;
hence IC Exec(i,s1) + n = Exec(i,s2).IC SCMPDS by A8,A32,A37,SCMPDS_2:
69
.= IC Exec(i,s2) by AMI_1:def 15;
end;
thus Exec(i,s1) | D = Exec(i,s2) | D by A33,Th23;
suppose A38: Ci = 7;
then consider a,k1,k2 such that
A39: i = (a,k1) := k2 by SCMPDS_2:42;
A40: now let b;
per cases;
suppose A41:DataLoc(s1.a,k1)=b;
then A42: DataLoc(s2.a,k1)=b by A6,Th23;
thus Exec(i, s1).b= k2 by A39,A41,SCMPDS_2:58
.=Exec(i,s2).b by A39,A42,SCMPDS_2:58;
suppose A43:DataLoc(s1.a,k1)<>b;
then A44: DataLoc(s2.a,k1)<>b by A6,Th23;
thus Exec(i,s1).b = s1.b by A39,A43,SCMPDS_2:58
.=s2.b by A6,Th23
.=Exec(i,s2).b by A39,A44,SCMPDS_2:58;
end;
thus IC Exec(i,s1) + n = IC Exec(i,s2) by A9,A38;
thus Exec(i,s1) | D = Exec(i,s2) | D by A40,Th23;
suppose A45: Ci = 8;
then consider a,k1,k2 such that
A46: i = AddTo(a,k1,k2) by SCMPDS_2:43;
A47: now let b;
per cases;
suppose A48:DataLoc(s1.a,k1)=b;
then A49: DataLoc(s2.a,k1)=b by A6,Th23;
thus Exec(i, s1).b= s1.DataLoc(s1.a,k1)+k2 by A46,A48,SCMPDS_2:60
.= s2.DataLoc(s2.a,k1)+k2 by A11
.=Exec(i,s2).b by A46,A49,SCMPDS_2:60;
suppose A50:DataLoc(s1.a,k1)<>b;
then A51: DataLoc(s2.a,k1)<>b by A6,Th23;
thus Exec(i,s1).b = s1.b by A46,A50,SCMPDS_2:60
.=s2.b by A6,Th23
.=Exec(i,s2).b by A46,A51,SCMPDS_2:60;
end;
thus IC Exec(i,s1) + n = IC Exec(i,s2) by A9,A45;
thus Exec(i,s1) | D = Exec(i,s2) | D by A47,Th23;
suppose A52: Ci = 9;
then consider a,b,k1,k2 such that
A53: i = AddTo(a,k1,b,k2) by SCMPDS_2:44;
A54: now let c;
per cases;
suppose A55:DataLoc(s1.a,k1)=c;
then A56: DataLoc(s2.a,k1)=c by A6,Th23;
thus Exec(i, s1).c = s1.DataLoc(s1.a,k1)+s1.DataLoc(s1.b,k2)
by A53,A55,SCMPDS_2:61
.= s2.DataLoc(s2.a,k1)+s1.DataLoc(s1.b,k2) by A11
.= s2.DataLoc(s2.a,k1)+s2.DataLoc(s2.b,k2) by A11
.=Exec(i,s2).c by A53,A56,SCMPDS_2:61;
suppose A57:DataLoc(s1.a,k1)<>c;
then A58: DataLoc(s2.a,k1)<>c by A6,Th23;
thus Exec(i,s1).c = s1.c by A53,A57,SCMPDS_2:61
.=s2.c by A6,Th23
.=Exec(i,s2).c by A53,A58,SCMPDS_2:61;
end;
thus IC Exec(i,s1) + n = IC Exec(i,s2) by A9,A52;
thus Exec(i,s1) | D = Exec(i,s2) | D by A54,Th23;
suppose A59: Ci = 10;
then consider a,b,k1,k2 such that
A60: i = SubFrom(a,k1,b,k2) by SCMPDS_2:45;
A61: now let c;
per cases;
suppose A62:DataLoc(s1.a,k1)=c;
then A63: DataLoc(s2.a,k1)=c by A6,Th23;
thus Exec(i, s1).c = s1.DataLoc(s1.a,k1)-s1.DataLoc(s1.b,k2)
by A60,A62,SCMPDS_2:62
.= s2.DataLoc(s2.a,k1)-s1.DataLoc(s1.b,k2) by A11
.= s2.DataLoc(s2.a,k1)-s2.DataLoc(s2.b,k2) by A11
.=Exec(i,s2).c by A60,A63,SCMPDS_2:62;
suppose A64:DataLoc(s1.a,k1)<>c;
then A65: DataLoc(s2.a,k1)<>c by A6,Th23;
thus Exec(i,s1).c = s1.c by A60,A64,SCMPDS_2:62
.=s2.c by A6,Th23
.=Exec(i,s2).c by A60,A65,SCMPDS_2:62;
end;
thus IC Exec(i,s1) + n = IC Exec(i,s2) by A9,A59;
thus Exec(i,s1) | D = Exec(i,s2) | D by A61,Th23;
suppose A66: Ci = 11;
then consider a,b,k1,k2 such that
A67: i = MultBy(a,k1,b,k2) by SCMPDS_2:46;
A68: now let c;
per cases;
suppose A69:DataLoc(s1.a,k1)=c;
then A70: DataLoc(s2.a,k1)=c by A6,Th23;
thus Exec(i, s1).c = s1.DataLoc(s1.a,k1)*s1.DataLoc(s1.b,k2)
by A67,A69,SCMPDS_2:63
.= s2.DataLoc(s2.a,k1)*s1.DataLoc(s1.b,k2) by A11
.= s2.DataLoc(s2.a,k1)*s2.DataLoc(s2.b,k2) by A11
.=Exec(i,s2).c by A67,A70,SCMPDS_2:63;
suppose A71:DataLoc(s1.a,k1)<>c;
then A72: DataLoc(s2.a,k1)<>c by A6,Th23;
thus Exec(i,s1).c = s1.c by A67,A71,SCMPDS_2:63
.=s2.c by A6,Th23
.=Exec(i,s2).c by A67,A72,SCMPDS_2:63;
end;
thus IC Exec(i,s1) + n = IC Exec(i,s2) by A9,A66;
thus Exec(i,s1) | D = Exec(i,s2) | D by A68,Th23;
suppose A73: Ci = 12;
then consider a,b,k1,k2 such that
A74: i = Divide(a,k1,b,k2) by SCMPDS_2:47;
A75: now let c;
per cases;
suppose A76:DataLoc(s1.b,k2)=c;
then A77: DataLoc(s2.b,k2)=c by A6,Th23;
thus Exec(i, s1).c = s1.DataLoc(s1.a,k1) mod s1.DataLoc(s1.b,k2)
by A74,A76,SCMPDS_2:64
.= s2.DataLoc(s2.a,k1) mod s1.DataLoc(s1.b,k2) by A11
.= s2.DataLoc(s2.a,k1) mod s2.DataLoc(s2.b,k2) by A11
.= Exec(i,s2).c by A74,A77,SCMPDS_2:64;
suppose A78:DataLoc(s1.b,k2)<>c;
then A79: DataLoc(s2.b,k2)<>c by A6,Th23;
hereby
per cases;
suppose A80:DataLoc(s1.a,k1)<>c;
then A81: DataLoc(s2.a,k1)<>c by A6,Th23;
thus Exec(i, s1).c = s1.c by A74,A78,A80,SCMPDS_2:64
.=s2.c by A6,Th23
.=Exec(i,s2).c by A74,A79,A81,SCMPDS_2:64;
suppose A82:DataLoc(s1.a,k1)=c;
then A83: DataLoc(s2.a,k1)=c by A6,Th23;
thus Exec(i, s1).c = s1.DataLoc(s1.a,k1) div s1.DataLoc(s1.b,k2)
by A74,A78,A82,SCMPDS_2:64
.= s2.DataLoc(s2.a,k1) div s1.DataLoc(s1.b,k2) by A11
.= s2.DataLoc(s2.a,k1) div s2.DataLoc(s2.b,k2) by A11
.= Exec(i,s2).c by A74,A79,A83,SCMPDS_2:64;
end;
end;
thus IC Exec(i,s1) + n = IC Exec(i,s2) by A9,A73;
thus Exec(i,s1) | D = Exec(i,s2) | D by A75,Th23;
suppose A84: Ci = 13;
then consider a,b,k1,k2 such that
A85: i = (a,k1):=(b,k2) by SCMPDS_2:48;
A86: now let c;
per cases;
suppose A87:DataLoc(s1.a,k1)=c;
then A88: DataLoc(s2.a,k1)=c by A6,Th23;
thus Exec(i, s1).c = s1.DataLoc(s1.b,k2) by A85,A87,SCMPDS_2:59
.= s2.DataLoc(s2.b,k2) by A11
.=Exec(i,s2).c by A85,A88,SCMPDS_2:59;
suppose A89:DataLoc(s1.a,k1)<>c;
then A90: DataLoc(s2.a,k1)<>c by A6,Th23;
thus Exec(i,s1).c = s1.c by A85,A89,SCMPDS_2:59
.=s2.c by A6,Th23
.=Exec(i,s2).c by A85,A90,SCMPDS_2:59;
end;
thus IC Exec(i,s1) + n = IC Exec(i,s2) by A9,A84;
thus Exec(i,s1) | D = Exec(i,s2) | D by A86,Th23;
end;
theorem ::Th27 T0
for J being parahalting shiftable Program-block st Initialized stop J c= s1
for n being Nat st Shift(stop J,n) c= s2 &
IC s2 = inspos n &
s1 | SCM-Data-Loc = s2 | SCM-Data-Loc
for i being Nat holds
IC (Computation s1).i + n = IC (Computation s2).i &
CurInstr ((Computation s1).i) = CurInstr ((Computation s2).i) &
(Computation s1).i | SCM-Data-Loc = (Computation s2).i | SCM-Data-Loc
proof
let I be parahalting shiftable Program-block;
set SI=stop I,
II = Initialized SI;
assume
A1: II c= s1;
let n be Nat; assume that
A2: Shift(SI,n) c= s2 and
A3: IC s2 = inspos n and
A4: s1 | SCM-Data-Loc = s2 | SCM-Data-Loc;
set C1 = Computation s1;
set C2 = Computation s2;
let i be Nat;
defpred P[Nat] means
IC C1.$1 + n = IC C2.$1 &
CurInstr (C1.$1) = CurInstr (C2.$1) &
C1.$1 | SCM-Data-Loc = C2.$1 | SCM-Data-Loc;
A5: II= SI +* Start-At inspos 0 by Def2;
dom SI misses dom Start-At inspos 0 by Th54;
then A6: SI c= II by A5,FUNCT_4:33;
then A7: dom SI c= dom II by GRFUNC_1:8;
A8: inspos 0 in dom SI by Th75;
A9: P[0]
proof
A10: IC SCMPDS in dom II by Th7;
inspos 0 + n in dom Shift(SI,n) by A8,Th76;
then A11: inspos (0 + n) in dom Shift(SI,n) by SCMPDS_3:def 3;
IC C1.0 = IC s1 by AMI_1:def 19
.= s1.IC SCMPDS by AMI_1:def 15
.= II.IC SCMPDS by A1,A10,GRFUNC_1:8
.= inspos 0 by Th29;
hence IC C1.0 + n = inspos (0 + n) by SCMPDS_3:def 3
.= IC C2.0 by A3,AMI_1:def 19;
A12: s1.IC s1 = s1.(s1.IC SCMPDS) by AMI_1:def 15
.= s1.((II).IC SCMPDS) by A1,A10,GRFUNC_1:8
.= s1.inspos 0 by Th29
.= II.inspos 0 by A1,A7,A8,GRFUNC_1:8
.= SI.inspos 0 by A6,A8,GRFUNC_1:8;
thus CurInstr (C1.0)
= CurInstr s1 by AMI_1:def 19
.= s1.IC s1 by AMI_1:def 17
.= Shift(SI,n).(inspos 0 + n) by A8,A12,SCMPDS_3:37
.= Shift(SI,n).inspos (0 + n) by SCMPDS_3:def 3
.= s2.IC s2 by A2,A3,A11,GRFUNC_1:8
.= CurInstr s2 by AMI_1:def 17
.= CurInstr (C2.0) by AMI_1:def 19;
thus C1.0 | SCM-Data-Loc
= s2 | SCM-Data-Loc by A4,AMI_1:def 19
.= C2.0 | SCM-Data-Loc by AMI_1:def 19;
end;
A13: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume A14: P[k];
set i = CurInstr C1.k;
A15: C1.(k + 1) = Following C1.k by AMI_1:def 19
.= Exec(CurInstr C1.k,C1.k) by AMI_1:def 18;
A16: C2.(k + 1) = Following C2.k by AMI_1:def 19
.= Exec(CurInstr C2.k,C2.k) by AMI_1:def 18;
A17: IC C1.k in dom SI by A1,Def9;
A18: i = C1.k.(IC C1.k) by AMI_1:def 17
.= s1.IC C1.k by AMI_1:54
.= II.IC C1.k by A1,A7,A17,GRFUNC_1:8
.= SI.IC C1.k by A6,A17,GRFUNC_1:8;
consider m such that
A19: IC C1.k =inspos m by SCMPDS_3:32;
A20: InsCode i <> 1 & InsCode i <> 3 & i valid_at m by A17,A18,A19,Def12;
hence A21: IC C1.(k + 1) + n
= IC C2.(k + 1) by A14,A15,A16,A19,Th83;
set l = IC C1.(k + 1);
A22: IC C1.(k + 1) in dom SI by A1,Def9;
A23: CurInstr C1.(k + 1) = C1.(k + 1).l by AMI_1:def 17
.= s1.l by AMI_1:54
.= II.l by A1,A7,A22,GRFUNC_1:8
.= SI.l by A6,A22,GRFUNC_1:8;
A24: IC C2.(k + 1) in dom Shift(SI,n) by A21,A22,Th76;
thus CurInstr C1.(k + 1)
= Shift(SI,n).(IC C2.(k + 1)) by A21,A22,A23,SCMPDS_3:37
.= s2.IC C2.(k + 1) by A2,A24,GRFUNC_1:8
.= C2.(k + 1).IC C2.(k + 1) by AMI_1:54
.= CurInstr C2.(k + 1) by AMI_1:def 17;
thus C1.(k + 1) | SCM-Data-Loc
= C2.(k + 1) | SCM-Data-Loc by A14,A15,A16,A19,A20,Th83;
end;
for k being Nat holds P[k] from Ind(A9,A13);
hence thesis;
end;