Copyright (c) 2003 Association of Mizar Users
environ
vocabulary BOOLE, SETFAM_1, FUNCT_1, ARYTM, ORDINAL2, FUNCT_4, FINSEQ_1,
FINSEQ_4, RELAT_1, CAT_1, AMISTD_2, REALSET1, FINSET_1, ARYTM_3, ARYTM_1,
ABSVALUE, INT_1, NAT_1, FUNCOP_1, TARSKI, AMI_1, AMI_2, AMI_3, AMISTD_1,
SCMPDS_2, SCMPDS_3, GOBOARD5, SQUARE_1;
notation TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL2, ORDINAL1, NUMBERS,
XCMPLX_0, XREAL_0, FUNCT_1, ABSVALUE, INT_1, NAT_1, CQC_LANG, FINSET_1,
REALSET1, STRUCT_0, GROUP_1, RELAT_1, FUNCT_4, FINSEQ_1, FINSEQ_4,
PRE_CIRC, AMI_1, AMI_2, AMI_3, AMI_5, SCMPDS_2, SCMPDS_3, AMISTD_1,
AMISTD_2;
constructors NAT_1, SCMPDS_1, SCMPDS_3, AMISTD_2, AMI_5, FINSEQ_4, REALSET1,
PRE_CIRC;
clusters ARYTM_3, FRAENKEL, INT_1, RELSET_1, AMI_1, SCMPDS_2, XREAL_0,
GOBOARD1, FUNCT_4, AMISTD_2, CQC_LANG, SCMRING1, FINSET_1, MEMBERED,
ORDINAL2;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, AMISTD_1, AMISTD_2;
theorems AMI_1, AMISTD_1, SETFAM_1, XBOOLE_0, SCMPDS_1, SCMPDS_2, SCMPDS_3,
ABSVALUE, INT_1, AXIOMS, JORDAN4, ORDINAL2, SCMFSA9A, TARSKI, FINSEQ_1,
AMI_2, AMI_3, NAT_1, XCMPLX_0, XCMPLX_1, XBOOLE_1, REAL_1, AMI_6,
RELAT_1, GROUP_4, FUNCT_4, YELLOW14, CQC_LANG, YELLOW_8, PRE_CIRC,
WSIERP_1, SCPINVAR, PEPIN;
schemes GOBOARD1;
begin :: Preliminaries
reserve r, s for real number;
theorem Th1:
0 <= r + abs(r)
proof
A1: 0 <= abs(r) by ABSVALUE:5;
then
A2: 0 + abs(r) <= abs(r) + abs(r) by AXIOMS:24;
abs(r) + abs(r) = r + abs(r) or abs(r) + r = -r + r by INT_1:30;
hence thesis by A1,A2,XCMPLX_0:def 6;
end;
theorem Th2:
0 <= -r + abs(r)
proof
r <= abs(r) by ABSVALUE:11;
then -r >= -abs(r) by REAL_1:50;
then -r+abs(r) >= -abs(r)+abs(r) by REAL_1:55;
hence thesis by XCMPLX_0:def 6;
end;
theorem Th3:
abs(r) = abs(s) implies r = s or r = -s
proof
assume
A1: abs(r) = abs(s);
assume
A2: r <> s;
per cases by INT_1:30;
suppose abs(r) = r & abs(s) = s;
hence r = -s by A1,A2;
suppose abs(r) = r & abs(s) = -s;
hence r = -s by A1;
suppose abs(r) = -r & abs(s) = s;
hence r = -s by A1;
suppose abs(r) = -r & abs(s) = -s;
hence r = -s by A1,A2,XCMPLX_1:134;
end;
theorem Th4:
for i, j being natural number st i < j & i <> 0 holds
i/j is not integer
proof
let i, j be natural number such that
A1: i < j and
A2: i <> 0;
A3: i >= 0 by NAT_1:19;
assume i/j is integer;
then reconsider r = i/j as Integer;
A4: i is Nat & j is Nat by ORDINAL2:def 21;
then i div j = 0 by A1,JORDAN4:5;
then
A5: i qua Integer div j = 0 by A4,SCMFSA9A:5;
r = [\ r /] by INT_1:47
.= i qua Integer div j by INT_1:def 7;
hence thesis by A1,A2,A3,A5,XCMPLX_1:50;
end;
theorem Th5:
{2*k where k is Nat: k > 1} is infinite
proof
set X = {2*k where k is Nat: k > 1};
assume
A1: X is finite;
A2: X c= NAT
proof
let x be set;
assume x in X;
then ex k being Nat st x = 2*k & k > 1;
hence thesis;
end;
2*2 in X;
then reconsider X as non empty finite Subset of NAT by A1,A2;
set m = max X;
m in X by PRE_CIRC:def 1;
then consider k being Nat such that
A3: m = 2*k and
A4: k > 1;
A5: m+2 = 2*k+2*1 by A3
.= 2*(k+1) by XCMPLX_1:8;
k+1 > k+0 by REAL_1:67;
then k+1 > 1 by A4,AXIOMS:22;
then m+2 in X by A5;
then m+2 <= m+0 by PRE_CIRC:def 1;
hence contradiction by REAL_1:67;
end;
theorem Th6:
for f being Function, a,b,c being set st a <> c holds
(f +* (a.-->b)).c = f.c
proof
let f be Function,
a,b,c be set such that
A1: a <> c;
set g = a.-->b;
dom g = {a} by CQC_LANG:5;
then not c in dom g by A1,TARSKI:def 1;
hence (f +* g).c = f.c by FUNCT_4:12;
end;
theorem Th7:
for f being Function, a,b,c,d being set st a <> b holds
(f +* ((a,b)-->(c,d))) .a = c &
(f +* ((a,b)-->(c,d))) .b = d
proof
let f be Function,
a,b,c,d be set such that
A1: a <> b;
set g = (a,b)-->(c,d);
A2: dom g = {a,b} by FUNCT_4:65;
then a in dom g by TARSKI:def 2;
hence (f +* g).a = g.a by FUNCT_4:14
.= c by A1,FUNCT_4:66;
b in dom g by A2,TARSKI:def 2;
hence (f +* g).b = g.b by FUNCT_4:14
.= d by A1,FUNCT_4:66;
end;
begin :: SCMPDS
reserve a, b for Int_position,
i for Instruction of SCMPDS,
l for Instruction-Location of SCMPDS,
k, k1, k2 for Integer,
n for Nat;
Lm1:
for N being with_non-empty_elements set,
S being IC-Ins-separated definite (non empty non void AMI-Struct over N),
s being State of S,
i being Instruction of S
holds Exec(s.IC s,s).IC S = IC Following s
proof
let N be with_non-empty_elements set,
S be IC-Ins-separated definite (non empty non void AMI-Struct over N),
s be State of S,
i be Instruction of S;
thus Exec(s.IC s,s).IC S = Exec(CurInstr s,s).IC S by AMI_1:def 17
.= (Following s).IC S by AMI_1:def 18
.= IC Following s by AMI_1:def 15;
end;
definition
let la, lb be Int_position,
a, b be Integer;
redefine func (la,lb) --> (a,b) -> FinPartState of SCMPDS;
coherence
proof
a is Element of INT & b is Element of INT &
ObjectKind la = INT & ObjectKind lb = INT by INT_1:def 2,SCMPDS_2:13;
hence thesis by AMI_1:58;
end;
end;
definition
cluster SCMPDS -> with-non-trivial-Instruction-Locations;
coherence
proof
thus the Instruction-Locations of SCMPDS is non trivial by SCMPDS_2:def 1;
end;
end;
definition
let l be Instruction-Location of SCMPDS;
func locnum l -> natural number means :Def1:
il.it = l;
existence
proof
consider i being Nat such that
A1: l = inspos i by SCMPDS_3:32;
l = il.i by A1,SCMPDS_3:def 2;
hence thesis;
end;
uniqueness
proof
let m, n be natural number such that
A2: il.m = l & il.n = l;
reconsider m,n as Nat by ORDINAL2:def 21;
l = inspos m & l = inspos n by A2,SCMPDS_3:def 2;
hence thesis by SCMPDS_3:31;
end;
end;
definition
let l be Instruction-Location of SCMPDS;
redefine func locnum l -> Nat;
coherence by ORDINAL2:def 21;
end;
theorem Th8:
l = 2*locnum l + 2
proof
thus 2*locnum l + 2 = il.locnum l by AMI_3:def 20
.= l by Def1;
end;
theorem
for l1, l2 being Instruction-Location of SCMPDS st l1 <> l2 holds
locnum l1 <> locnum l2
proof
let l1, l2 be Instruction-Location of SCMPDS such that
A1: l1 <> l2 & locnum l1 = locnum l2;
il.locnum l1 = l1 & il.locnum l2 = l2 by Def1;
hence thesis by A1;
end;
theorem Th10:
for l1, l2 being Instruction-Location of SCMPDS st l1 <> l2 holds
Next l1 <> Next l2
proof
let l1, l2 be Instruction-Location of SCMPDS;
assume
A1: l1 <> l2 & Next l1 = Next l2;
consider m1 being Element of SCM-Instr-Loc such that
A2: m1 = l1 & Next l1 = Next m1 by SCMPDS_2:def 19;
consider m2 being Element of SCM-Instr-Loc such that
A3: m2 = l2 & Next l2 = Next m2 by SCMPDS_2:def 19;
Next m1 = m1+2 & Next m2 = m2+2 by AMI_2:def 15;
hence contradiction by A1,A2,A3,XCMPLX_1:2;
end;
theorem Th11:
for N being with_non-empty_elements set,
S being IC-Ins-separated definite (non empty non void AMI-Struct over N),
i being Instruction of S,
l being Instruction-Location of S holds
JUMP(i) c= NIC(i,l)
proof
let N be with_non-empty_elements set,
S be IC-Ins-separated definite (non empty non void AMI-Struct over N),
i be Instruction of S,
l be Instruction-Location of S;
set X = { NIC(i,k) where k is Instruction-Location of S:
not contradiction };
let x be set;
assume x in JUMP(i);
then
A1: x in meet X by AMISTD_1:def 6;
NIC(i,l) in X;
hence thesis by A1,SETFAM_1:def 1;
end;
theorem Th12:
(for s being State of SCMPDS st IC s = l & s.l = i
holds Exec(i,s).IC SCMPDS = Next IC s)
implies
NIC(i, l) = {Next l}
proof
assume
A1: for s being State of SCMPDS st IC s = l & s.l = i
holds Exec(i, s).IC SCMPDS = Next IC s;
set X = {IC Following s where s is State of SCMPDS: IC s = l & s.l = i};
A2: NIC(i,l) = X by AMISTD_1:def 5;
hereby
let x be set;
assume x in NIC(i,l);
then consider s being State of SCMPDS such that
A3: x = IC Following s & IC s = l & s.l = i by A2;
x = Exec(s.IC s, s).IC SCMPDS by A3,Lm1
.= Next l by A1,A3;
hence x in {Next l} by TARSKI:def 1;
end;
let x be set;
assume x in {Next l};
then
A4: x = Next l by TARSKI:def 1;
consider t being State of SCMPDS;
reconsider il1 = l as Element of ObjectKind IC SCMPDS by AMI_1:def 11;
reconsider I = i as Element of ObjectKind l by AMI_1:def 14;
set u = t+*((IC SCMPDS, l)-->(il1, I));
A5: IC u = l by AMI_6:6;
A6: u.l = i by AMI_6:6;
IC Following u = Exec(u.IC u, u).IC SCMPDS by AMI_6:6
.= Next l by A1,A5,A6;
hence thesis by A2,A4,A5,A6;
end;
theorem Th13:
(for l being Instruction-Location of SCMPDS holds NIC(i,l)={Next l})
implies JUMP i is empty
proof
assume
A1: for l being Instruction-Location of SCMPDS holds NIC(i,l)={Next l};
consider p, q being Element of the Instruction-Locations of SCMPDS
such that
A2: p <> q by YELLOW_8:def 1;
set X = { NIC(i,f) where f is Instruction-Location of SCMPDS:
not contradiction };
assume not thesis;
then meet X is non empty by AMISTD_1:def 6;
then consider x being set such that
A3: x in meet X by XBOOLE_0:def 1;
NIC(i,p) = {Next p} & NIC(i,q) = {Next q} by A1;
then {Next p} in X & {Next q} in X;
then x in {Next p} & x in {Next q} by A3,SETFAM_1:def 1;
then x = Next p & x = Next q by TARSKI:def 1;
hence contradiction by A2,Th10;
end;
theorem Th14:
NIC(goto k,l) = { 2*abs(k+locnum l) + 2 }
proof
set i = goto k;
set X = { IC Following s where s is State of SCMPDS: IC s = l & s.l = i };
set t = 2*abs(k+locnum l)+2;
A1: NIC(i,l) = X by AMISTD_1:def 5;
l in { 2*k1 where k1 is Nat: k1 > 0 } by AMI_2:def 3,SCMPDS_2:def 1;
then consider k1 being Nat such that
A2: l = 2*k1 and
k1 > 0;
A3: 2*locnum l + 2 = l by Th8;
A4: now
thus 2*abs(locnum l+k) = abs(2)*abs(locnum l + k) by ABSVALUE:def 1
.= abs(2*(locnum l+k)) by ABSVALUE:10;
end;
hereby
let x be set;
assume x in NIC(i,l);
then consider s being State of SCMPDS such that
A5: x = IC Following s and
A6: IC s = l and
A7: s.l = i by A1;
consider m1 being Nat such that
A8: m1 = IC s and
A9: ICplusConst(s,k) = abs(m1-2+2*k)+2 by SCMPDS_2:def 20;
x = Exec(i,s).IC SCMPDS by A5,A6,A7,Lm1
.= abs(2*k1-2*1+2*k)+2 by A2,A6,A8,A9,SCMPDS_2:66
.= abs(2*locnum l+2*k)+2 by A2,A3,XCMPLX_1:26
.= t by A4,XCMPLX_1:8;
hence x in {t} by TARSKI:def 1;
end;
let x be set;
assume
A10: x in {t};
consider s being State of SCMPDS;
reconsider il1 = l as Element of ObjectKind IC SCMPDS by AMI_1:def 11;
reconsider I = i as Element of ObjectKind l by AMI_1:def 14;
set u = s+*((IC SCMPDS, l)-->(il1, I));
A11: u.l = i by AMI_6:6;
A12: IC u = l by AMI_6:6;
consider m1 being Nat such that
A13: m1 = IC u and
A14: ICplusConst(u,k) = abs(m1-2+2*k)+2 by SCMPDS_2:def 20;
x = t by A10,TARSKI:def 1
.= abs(2*locnum l+2*k)+2 by A4,XCMPLX_1:8
.= abs(m1-2+2*k)+2 by A3,A12,A13,XCMPLX_1:26
.= Exec(i,u).IC SCMPDS by A14,SCMPDS_2:66
.= IC Following u by A11,A12,Lm1;
hence thesis by A1,A11,A12;
end;
Lm2:
for k being natural number st k > 1 holds k-2 is Nat
proof
let k be natural number;
assume k > 1;
then k >= 1+1 by NAT_1:38;
then k - 2 >= 2 - 2 by REAL_1:49;
hence thesis by INT_1:16;
end;
theorem Th15:
NIC(return a,l) = {2*k where k is Nat: k > 1}
proof
set i = return a;
set X = {2*k where k is Nat: k > 1};
A1: NIC(i,l) = { IC Following s where s is State of SCMPDS:
IC s = l & s.l = i } by AMISTD_1:def 5;
hereby
let x be set;
assume x in NIC(i,l);
then consider s being State of SCMPDS such that
A2: x = IC Following s and
A3: IC s = l and
A4: s.l = i by A1;
A5: x = Exec(i,s).IC SCMPDS by A2,A3,A4,Lm1
.= 2*(abs(s.DataLoc(s.a,1)) div 2)+2*2 by SCMPDS_1:def 23,SCMPDS_2:70;
x in { 2*k where k is Nat: k > 0 } by A2,AMI_2:def 3,SCMPDS_2:def 1;
then consider k being Nat such that
A6: x = 2*k and k > 0;
A7: 2*k = 2*((abs(s.DataLoc(s.a,1)) div 2)+2) by A5,A6,XCMPLX_1:8;
abs(s.DataLoc(s.a,1)) div 2 >= 0 by NAT_1:18;
then (abs(s.DataLoc(s.a,1)) div 2)+2 >= 0+2 by AXIOMS:24;
then k >= 1+1 by A7,XCMPLX_1:5;
then k > 1 by NAT_1:38;
hence x in X by A6;
end;
let x be set;
assume x in X;
then consider k being Nat such that
A8: x = 2*k and
A9: k > 1;
reconsider k2 = k - 2 as Nat by A9,Lm2;
a in SCM-Data-Loc by SCMPDS_2:def 2;
then consider j being Nat such that
A10: a = 2*j+1 by AMI_2:def 2;
consider s being State of SCMPDS;
reconsider il1 = l as Element of ObjectKind IC SCMPDS by AMI_1:def 11;
reconsider I = i as Element of ObjectKind l by AMI_1:def 14;
set u = s +* ((IC SCMPDS, l)-->(il1, I));
set t = 2*j+1+2;
t = 2*j+2*1+1 by XCMPLX_1:1
.= 2*(j+1)+1 by XCMPLX_1:8;
then t in SCM-Data-Loc by AMI_2:def 2;
then reconsider t1 = t as Int_position by SCMPDS_2:9;
set g = (a,t1)-->(j,2*k2);
set v = u +* g;
A11: dom g = {a,t} by FUNCT_4:65;
A12: u.l = i by AMI_6:6;
A13: u.IC SCMPDS = IC u by AMI_1:def 15
.= l by AMI_6:6;
l <> a & l <> t1 by SCMPDS_2:53;
then not l in dom g by A11,TARSKI:def 2;
then
A14: v.l = i by A12,FUNCT_4:12;
a <> IC SCMPDS & t1 <> IC SCMPDS by SCMPDS_2:52;
then
A15: not IC SCMPDS in dom g by A11,TARSKI:def 2;
A16: IC v = v.IC SCMPDS by AMI_1:def 15
.= l by A13,A15,FUNCT_4:12;
a = 2*j+1+0 by A10;
then
A17: a <> t by XCMPLX_1:2;
then
A18: v.a = j by Th7;
A19: v.t = 2*k2 by A17,Th7;
A20: j+1 >= 0 by NAT_1:18;
A21: DataLoc(j,1) = 2*abs(j+1)+1 by SCMPDS_2:def 4
.= 2*(j+1)+1 by A20,ABSVALUE:def 1
.= 2*j+2*1+1 by XCMPLX_1:8
.= t by XCMPLX_1:1;
reconsider r = v.t as Nat by A17,Th7;
A22: r >= 0 by NAT_1:18;
x = 2*(k2 + 2) by A8,XCMPLX_1:27
.= 2*((2*k2 div 2) + 2) by GROUP_4:107
.= 2*((abs(r) div 2)+2) by A19,A22,ABSVALUE:def 1
.= 2*(abs(v.DataLoc(j,1)) div 2) + 2*2 by A21,XCMPLX_1:8
.= Exec(i,v).IC SCMPDS by A18,SCMPDS_1:def 23,SCMPDS_2:70
.= IC Following v by A14,A16,Lm1;
hence x in NIC(i,l) by A1,A14,A16;
end;
theorem Th16:
NIC(saveIC(a,k1), l) = {Next l}
proof
set i = saveIC(a,k1);
for s being State of SCMPDS st IC s = l & s.l = i
holds Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:71;
hence thesis by Th12;
end;
theorem Th17:
NIC(a:=k1, l) = {Next l}
proof
set i = a:=k1;
for s being State of SCMPDS st IC s = l & s.l = i
holds Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:57;
hence thesis by Th12;
end;
theorem Th18:
NIC((a,k1):=k2, l) = {Next l}
proof
set i = (a,k1):=k2;
for s being State of SCMPDS st IC s = l & s.l = i
holds Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:58;
hence thesis by Th12;
end;
theorem Th19:
NIC((a,k1):=(b,k2), l) = {Next l}
proof
set i = (a,k1):=(b,k2);
for s being State of SCMPDS st IC s = l & s.l = i
holds Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:59;
hence thesis by Th12;
end;
theorem Th20:
NIC(AddTo(a,k1,k2), l) = {Next l}
proof
set i = AddTo(a,k1,k2);
for s being State of SCMPDS st IC s = l & s.l = i
holds Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:60;
hence thesis by Th12;
end;
theorem Th21:
NIC(AddTo(a,k1,b,k2), l) = {Next l}
proof
set i = AddTo(a,k1,b,k2);
for s being State of SCMPDS st IC s = l & s.l = i
holds Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:61;
hence thesis by Th12;
end;
theorem Th22:
NIC(SubFrom(a,k1,b,k2), l) = {Next l}
proof
set i = SubFrom(a,k1,b,k2);
for s being State of SCMPDS st IC s = l & s.l = i
holds Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:62;
hence thesis by Th12;
end;
theorem Th23:
NIC(MultBy(a,k1,b,k2), l) = {Next l}
proof
set i = MultBy(a,k1,b,k2);
for s being State of SCMPDS st IC s = l & s.l = i
holds Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:63;
hence thesis by Th12;
end;
theorem Th24:
NIC(Divide(a,k1,b,k2), l) = {Next l}
proof
set i = Divide(a,k1,b,k2);
for s being State of SCMPDS st IC s = l & s.l = i
holds Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:64;
hence thesis by Th12;
end;
theorem
NIC((a,k1)<>0_goto k2,l) = { Next l, abs( 2*(k2+locnum l) ) + 2 }
proof
set i = (a,k1)<>0_goto k2;
set X = { IC Following s where s is State of SCMPDS: IC s = l & s.l = i };
set t = abs(2*(k2+locnum l))+2;
A1: NIC(i,l) = X by AMISTD_1:def 5;
l in { 2*w1 where w1 is Nat: w1 > 0 } by AMI_2:def 3,SCMPDS_2:def 1;
then consider w1 being Nat such that
A2: l = 2*w1 and
w1 > 0;
A3: 2*locnum l + 2 = l by Th8;
hereby
let x be set;
assume x in NIC(i,l);
then consider s being State of SCMPDS such that
A4: x = IC Following s and
A5: IC s = l and
A6: s.l = i by A1;
consider m1 being Nat such that
A7: m1 = IC s and
A8: ICplusConst(s,k2) = abs(m1-2+2*k2)+2 by SCMPDS_2:def 20;
per cases;
suppose
A9: s.DataLoc(s.a,k1) <> 0;
x = Exec(i,s).IC SCMPDS by A4,A5,A6,Lm1
.= abs(2*w1-2*1+2*k2)+2 by A2,A5,A7,A8,A9,SCMPDS_2:67
.= abs(2*locnum l+2*k2)+2 by A2,A3,XCMPLX_1:26
.= t by XCMPLX_1:8;
hence x in {Next l,t} by TARSKI:def 2;
suppose
A10: s.DataLoc(s.a,k1) = 0;
x = Exec(i,s).IC SCMPDS by A4,A5,A6,Lm1
.= Next l by A5,A10,SCMPDS_2:67;
hence x in {Next l,t} by TARSKI:def 2;
end;
let x be set;
assume
A11: x in {Next l,t};
consider s being State of SCMPDS;
reconsider il1 = l as Element of ObjectKind IC SCMPDS by AMI_1:def 11;
reconsider I = i as Element of ObjectKind l by AMI_1:def 14;
set u = s+*((IC SCMPDS, l)-->(il1, I));
per cases by A11,TARSKI:def 2;
suppose
A12: x = Next l;
set u1 = u +* (a.-->0);
set u2 = u1 +* (DataLoc(u1.a,k1).-->0);
A13: l <> a by SCMPDS_2:53;
l <> DataLoc(u1.a,k1) by SCMPDS_2:53;
then
A14: u2.l = u1.l by Th6
.= u.l by A13,Th6
.= i by AMI_6:6;
A15: IC SCMPDS <> DataLoc(u1.a,k1) by SCMPDS_2:52;
A16: IC SCMPDS <> a by SCMPDS_2:52;
A17: IC u2 = u2.IC SCMPDS by AMI_1:def 15
.= u1.IC SCMPDS by A15,Th6
.= u.IC SCMPDS by A16,Th6
.= IC u by AMI_1:def 15
.= il1 by AMI_6:6;
A18: u2.DataLoc(u1.a,k1) = 0 by YELLOW14:3;
u2.DataLoc(u2.a,k1) = 0
proof
per cases;
suppose a = DataLoc(u1.a,k1);
hence thesis by A18,YELLOW14:3;
suppose a <> DataLoc(u1.a,k1);
then u2.a = u1.a by Th6;
hence thesis by YELLOW14:3;
end;
then x = Exec(i,u2).IC SCMPDS by A12,A17,SCMPDS_2:67
.= IC Following u2 by A14,A17,Lm1;
hence thesis by A1,A14,A17;
suppose
A19: x = t;
set u1 = u +* (a.-->1);
set u2 = u1 +* (DataLoc(u1.a,k1).-->1);
A20: l <> a by SCMPDS_2:53;
l <> DataLoc(u1.a,k1) by SCMPDS_2:53;
then
A21: u2.l = u1.l by Th6
.= u.l by A20,Th6
.= i by AMI_6:6;
A22: IC SCMPDS <> DataLoc(u1.a,k1) by SCMPDS_2:52;
A23: IC SCMPDS <> a by SCMPDS_2:52;
A24: IC u2 = u2.IC SCMPDS by AMI_1:def 15
.= u1.IC SCMPDS by A22,Th6
.= u.IC SCMPDS by A23,Th6
.= IC u by AMI_1:def 15
.= il1 by AMI_6:6;
A25: u2.DataLoc(u1.a,k1) = 1 by YELLOW14:3;
A26: u2.DataLoc(u2.a,k1) <> 0
proof
per cases;
suppose a = DataLoc(u1.a,k1);
hence thesis by A25,YELLOW14:3;
suppose a <> DataLoc(u1.a,k1);
then u2.a = u1.a by Th6;
hence thesis by YELLOW14:3;
end;
consider m1 being Nat such that
A27: m1 = IC u2 and
A28: ICplusConst(u2,k2) = abs(m1-2+2*k2)+2 by SCMPDS_2:def 20;
x = abs(2*locnum l+2*k2)+2 by A19,XCMPLX_1:8
.= abs(m1-2+2*k2)+2 by A3,A24,A27,XCMPLX_1:26
.= Exec(i,u2).IC SCMPDS by A26,A28,SCMPDS_2:67
.= IC Following u2 by A21,A24,Lm1;
hence thesis by A1,A21,A24;
end;
theorem
NIC((a,k1)<=0_goto k2,l) = { Next l, abs( 2*(k2+locnum l) ) + 2 }
proof
set i = (a,k1)<=0_goto k2;
set X = { IC Following s where s is State of SCMPDS: IC s = l & s.l = i };
set t = abs(2*(k2+locnum l))+2;
A1: NIC(i,l) = X by AMISTD_1:def 5;
l in { 2*w1 where w1 is Nat: w1 > 0 } by AMI_2:def 3,SCMPDS_2:def 1;
then consider w1 being Nat such that
A2: l = 2*w1 and
w1 > 0;
A3: 2*locnum l + 2 = l by Th8;
hereby
let x be set;
assume x in NIC(i,l);
then consider s being State of SCMPDS such that
A4: x = IC Following s and
A5: IC s = l and
A6: s.l = i by A1;
consider m1 being Nat such that
A7: m1 = IC s and
A8: ICplusConst(s,k2) = abs(m1-2+2*k2)+2 by SCMPDS_2:def 20;
per cases;
suppose
A9: s.DataLoc(s.a,k1) <= 0;
x = Exec(i,s).IC SCMPDS by A4,A5,A6,Lm1
.= abs(2*w1-2*1+2*k2)+2 by A2,A5,A7,A8,A9,SCMPDS_2:68
.= abs(2*locnum l+2*k2)+2 by A2,A3,XCMPLX_1:26
.= t by XCMPLX_1:8;
hence x in {Next l,t} by TARSKI:def 2;
suppose
A10: s.DataLoc(s.a,k1) > 0;
x = Exec(i,s).IC SCMPDS by A4,A5,A6,Lm1
.= Next l by A5,A10,SCMPDS_2:68;
hence x in {Next l,t} by TARSKI:def 2;
end;
let x be set;
assume
A11: x in {Next l,t};
consider s being State of SCMPDS;
reconsider il1 = l as Element of ObjectKind IC SCMPDS by AMI_1:def 11;
reconsider I = i as Element of ObjectKind l by AMI_1:def 14;
set u = s+*((IC SCMPDS, l)-->(il1, I));
per cases by A11,TARSKI:def 2;
suppose
A12: x = Next l;
set u1 = u +* (a.-->1);
set u2 = u1 +* (DataLoc(u1.a,k1).-->1);
A13: l <> a by SCMPDS_2:53;
l <> DataLoc(u1.a,k1) by SCMPDS_2:53;
then
A14: u2.l = u1.l by Th6
.= u.l by A13,Th6
.= i by AMI_6:6;
A15: IC SCMPDS <> DataLoc(u1.a,k1) by SCMPDS_2:52;
A16: IC SCMPDS <> a by SCMPDS_2:52;
A17: IC u2 = u2.IC SCMPDS by AMI_1:def 15
.= u1.IC SCMPDS by A15,Th6
.= u.IC SCMPDS by A16,Th6
.= IC u by AMI_1:def 15
.= il1 by AMI_6:6;
A18: u2.DataLoc(u1.a,k1) = 1 by YELLOW14:3;
A19: 1 > 0;
u2.DataLoc(u2.a,k1) > 0
proof
per cases;
suppose a = DataLoc(u1.a,k1);
hence thesis by A18,A19,YELLOW14:3;
suppose a <> DataLoc(u1.a,k1);
then u2.a = u1.a by Th6;
hence thesis by A19,YELLOW14:3;
end;
then x = Exec(i,u2).IC SCMPDS by A12,A17,SCMPDS_2:68
.= IC Following u2 by A14,A17,Lm1;
hence thesis by A1,A14,A17;
suppose
A20: x = t;
set u1 = u +* (a.-->0);
set u2 = u1 +* (DataLoc(u1.a,k1).-->0);
A21: l <> a by SCMPDS_2:53;
l <> DataLoc(u1.a,k1) by SCMPDS_2:53;
then
A22: u2.l = u1.l by Th6
.= u.l by A21,Th6
.= i by AMI_6:6;
A23: IC SCMPDS <> DataLoc(u1.a,k1) by SCMPDS_2:52;
A24: IC SCMPDS <> a by SCMPDS_2:52;
A25: IC u2 = u2.IC SCMPDS by AMI_1:def 15
.= u1.IC SCMPDS by A23,Th6
.= u.IC SCMPDS by A24,Th6
.= IC u by AMI_1:def 15
.= il1 by AMI_6:6;
A26: u2.DataLoc(u1.a,k1) = 0 by YELLOW14:3;
A27: u2.DataLoc(u2.a,k1) <= 0
proof
per cases;
suppose a = DataLoc(u1.a,k1);
hence thesis by A26,YELLOW14:3;
suppose a <> DataLoc(u1.a,k1);
then u2.a = u1.a by Th6;
hence thesis by YELLOW14:3;
end;
consider m1 being Nat such that
A28: m1 = IC u2 and
A29: ICplusConst(u2,k2) = abs(m1-2+2*k2)+2 by SCMPDS_2:def 20;
x = abs(2*locnum l+2*k2)+2 by A20,XCMPLX_1:8
.= abs(m1-2+2*k2)+2 by A3,A25,A28,XCMPLX_1:26
.= Exec(i,u2).IC SCMPDS by A27,A29,SCMPDS_2:68
.= IC Following u2 by A22,A25,Lm1;
hence thesis by A1,A22,A25;
end;
theorem
NIC((a,k1)>=0_goto k2,l) = { Next l, abs( 2*(k2+locnum l) ) + 2 }
proof
set i = (a,k1)>=0_goto k2;
set X = { IC Following s where s is State of SCMPDS: IC s = l & s.l = i };
set t = abs(2*(k2+locnum l))+2;
A1: NIC(i,l) = X by AMISTD_1:def 5;
l in { 2*w1 where w1 is Nat: w1 > 0 } by AMI_2:def 3,SCMPDS_2:def 1;
then consider w1 being Nat such that
A2: l = 2*w1 and
w1 > 0;
A3: 2*locnum l + 2 = l by Th8;
hereby
let x be set;
assume x in NIC(i,l);
then consider s being State of SCMPDS such that
A4: x = IC Following s and
A5: IC s = l and
A6: s.l = i by A1;
consider m1 being Nat such that
A7: m1 = IC s and
A8: ICplusConst(s,k2) = abs(m1-2+2*k2)+2 by SCMPDS_2:def 20;
per cases;
suppose
A9: s.DataLoc(s.a,k1) >= 0;
x = Exec(i,s).IC SCMPDS by A4,A5,A6,Lm1
.= abs(2*w1-2*1+2*k2)+2 by A2,A5,A7,A8,A9,SCMPDS_2:69
.= abs(2*locnum l+2*k2)+2 by A2,A3,XCMPLX_1:26
.= t by XCMPLX_1:8;
hence x in {Next l,t} by TARSKI:def 2;
suppose
A10: s.DataLoc(s.a,k1) < 0;
x = Exec(i,s).IC SCMPDS by A4,A5,A6,Lm1
.= Next l by A5,A10,SCMPDS_2:69;
hence x in {Next l,t} by TARSKI:def 2;
end;
let x be set;
assume
A11: x in {Next l,t};
consider s being State of SCMPDS;
reconsider il1 = l as Element of ObjectKind IC SCMPDS by AMI_1:def 11;
reconsider I = i as Element of ObjectKind l by AMI_1:def 14;
set u = s+*((IC SCMPDS, l)-->(il1, I));
per cases by A11,TARSKI:def 2;
suppose
A12: x = Next l;
set u1 = u +* (a.-->-1);
set u2 = u1 +* (DataLoc(u1.a,k1).-->-1);
A13: l <> a by SCMPDS_2:53;
l <> DataLoc(u1.a,k1) by SCMPDS_2:53;
then
A14: u2.l = u1.l by Th6
.= u.l by A13,Th6
.= i by AMI_6:6;
A15: IC SCMPDS <> DataLoc(u1.a,k1) by SCMPDS_2:52;
A16: IC SCMPDS <> a by SCMPDS_2:52;
A17: IC u2 = u2.IC SCMPDS by AMI_1:def 15
.= u1.IC SCMPDS by A15,Th6
.= u.IC SCMPDS by A16,Th6
.= IC u by AMI_1:def 15
.= il1 by AMI_6:6;
A18: u2.DataLoc(u1.a,k1) = -1 by YELLOW14:3;
A19: -1 < 0;
u2.DataLoc(u2.a,k1) < 0
proof
per cases;
suppose a = DataLoc(u1.a,k1);
hence thesis by A18,A19,YELLOW14:3;
suppose a <> DataLoc(u1.a,k1);
then u2.a = u1.a by Th6;
hence thesis by A19,YELLOW14:3;
end;
then x = Exec(i,u2).IC SCMPDS by A12,A17,SCMPDS_2:69
.= IC Following u2 by A14,A17,Lm1;
hence thesis by A1,A14,A17;
suppose
A20: x = t;
set u1 = u +* (a.-->0);
set u2 = u1 +* (DataLoc(u1.a,k1).-->0);
A21: l <> a by SCMPDS_2:53;
l <> DataLoc(u1.a,k1) by SCMPDS_2:53;
then
A22: u2.l = u1.l by Th6
.= u.l by A21,Th6
.= i by AMI_6:6;
A23: IC SCMPDS <> DataLoc(u1.a,k1) by SCMPDS_2:52;
A24: IC SCMPDS <> a by SCMPDS_2:52;
A25: IC u2 = u2.IC SCMPDS by AMI_1:def 15
.= u1.IC SCMPDS by A23,Th6
.= u.IC SCMPDS by A24,Th6
.= IC u by AMI_1:def 15
.= il1 by AMI_6:6;
A26: u2.DataLoc(u1.a,k1) = 0 by YELLOW14:3;
A27: u2.DataLoc(u2.a,k1) >= 0
proof
per cases;
suppose a = DataLoc(u1.a,k1);
hence thesis by A26,YELLOW14:3;
suppose a <> DataLoc(u1.a,k1);
then u2.a = u1.a by Th6;
hence thesis by YELLOW14:3;
end;
consider m1 being Nat such that
A28: m1 = IC u2 and
A29: ICplusConst(u2,k2) = abs(m1-2+2*k2)+2 by SCMPDS_2:def 20;
x = abs(2*locnum l+2*k2)+2 by A20,XCMPLX_1:8
.= abs(m1-2+2*k2)+2 by A3,A25,A28,XCMPLX_1:26
.= Exec(i,u2).IC SCMPDS by A27,A29,SCMPDS_2:69
.= IC Following u2 by A22,A25,Lm1;
hence thesis by A1,A22,A25;
end;
Lm3: JUMP goto k = {}
proof
set i = goto k;
set X = { NIC(i,l) where l is Instruction-Location of SCMPDS:
not contradiction };
hereby
let x be set;
assume
A1: x in JUMP i;
set l1 = inspos 0;
A2: NIC(i,l1) in X;
A3: JUMP i = meet X by AMISTD_1:def 6;
then x in NIC(i,l1) by A1,A2,SETFAM_1:def 1;
then x in { IC Following s1 where s1 is State of SCMPDS:
IC s1 = l1 & s1.l1 = i } by AMISTD_1:def 5;
then consider s1 being State of SCMPDS such that
A4: x = IC Following s1 and
A5: IC s1 = l1 and
A6: s1.l1 = i;
consider m1 being Nat such that
A7: m1 = IC s1 and
A8: ICplusConst(s1,k) = abs(m1-2+2*k)+2 by SCMPDS_2:def 20;
A9: m1 = il.0 by A5,A7,SCMPDS_3:def 2
.= 2*0+2 by AMI_3:def 20;
A10: x = (Following s1).IC SCMPDS by A4,AMI_1:def 15
.= Exec(CurInstr s1,s1).IC SCMPDS by AMI_1:def 18
.= Exec(i,s1).IC SCMPDS by A5,A6,AMI_1:def 17
.= abs(m1-2+2*k)+2 by A8,SCMPDS_2:66;
set l2 = inspos 1;
NIC(i,l2) in X;
then x in NIC(i,l2) by A1,A3,SETFAM_1:def 1;
then x in { IC Following s2 where s2 is State of SCMPDS:
IC s2 = l2 & s2.l2 = i } by AMISTD_1:def 5;
then consider s2 being State of SCMPDS such that
A11: x = IC Following s2 and
A12: IC s2 = l2 and
A13: s2.l2 = i;
consider m2 being Nat such that
A14: m2 = IC s2 and
A15: ICplusConst(s2,k) = abs(m2-2+2*k)+2 by SCMPDS_2:def 20;
A16: m2 = il.1 by A12,A14,SCMPDS_3:def 2
.= 2*1+2 by AMI_3:def 20;
x = (Following s2).IC SCMPDS by A11,AMI_1:def 15
.= Exec(CurInstr s2,s2).IC SCMPDS by AMI_1:def 18
.= Exec(i,s2).IC SCMPDS by A12,A13,AMI_1:def 17
.= abs(m2-2+2*k)+2 by A15,SCMPDS_2:66;
then
A17: abs(m1-2+2*k) = abs(m2-2+2*k) by A10,XCMPLX_1:2;
per cases by A9,A16,A17,Th3;
suppose 0+2*k = 2+2*k;
hence x in {} by XCMPLX_1:2;
suppose
A18: 2*k = -(2+2*k);
0 = -(2*k) + 2*k by XCMPLX_0:def 6
.= 2 + (2*k + 2*k) by A18,XCMPLX_1:1
.= 2 + ((2+2)*k) by XCMPLX_1:8;
then -2 = 4*k by XCMPLX_0:def 6;
then -2/4 = 4*k/4;
then
A19: -2/4 = k by XCMPLX_1:90;
for i being Integer holds -i is integer;
then --1/2 is integer by A19;
hence x in {} by Th4;
end;
thus thesis by XBOOLE_1:2;
end;
definition
let k;
cluster JUMP (goto k) -> empty;
coherence by Lm3;
end;
theorem Th28:
JUMP (return a) = {2*k where k is Nat: k > 1}
proof
set i = return a;
set A = {2*k where k is Nat: k > 1};
JUMP i c= NIC(i,inspos(0)) by Th11;
hence JUMP i c= A by Th15;
let x be set;
assume
A1: x in A;
set X = { NIC(i,l) where l is Instruction-Location of SCMPDS:
not contradiction };
now
NIC(i,inspos(0)) in X;
hence X <> {};
let y be set;
assume y in X;
then consider l being Instruction-Location of SCMPDS such that
A2: y = NIC(i,l);
A3: NIC(i,l) = { IC Following s where s is State of SCMPDS:
IC s = l & s.l = i } by AMISTD_1:def 5;
a in SCM-Data-Loc by SCMPDS_2:def 2;
then consider j being Nat such that
A4: a = 2*j+1 by AMI_2:def 2;
consider s being State of SCMPDS;
reconsider il1 = l as Element of ObjectKind IC SCMPDS by AMI_1:def 11;
reconsider I = i as Element of ObjectKind l by AMI_1:def 14;
set u = s+*((IC SCMPDS, l)-->(il1, I));
consider k being Nat such that
A5: x = 2*k and
A6: k > 1 by A1;
set t = 2*j+1+2;
t = 2*j+2*1+1 by XCMPLX_1:1
.= 2*(j+1)+1 by XCMPLX_1:8;
then t in SCM-Data-Loc by AMI_2:def 2;
then reconsider t1 = t as Int_position by SCMPDS_2:9;
reconsider k2 = k-2 as Nat by A6,Lm2;
set g = (a,t1)-->(j,2*k2);
set v = u +* g;
A7: dom g = {a,t1} by FUNCT_4:65;
A8: u.l = i by AMI_6:6;
A9: u.IC SCMPDS = IC u by AMI_1:def 15
.= l by AMI_6:6;
l <> a & l <> t1 by SCMPDS_2:53;
then not l in dom g by A7,TARSKI:def 2;
then
A10: v.l = i by A8,FUNCT_4:12;
a <> IC SCMPDS & t1 <> IC SCMPDS by SCMPDS_2:52;
then
A11: not IC SCMPDS in dom g by A7,TARSKI:def 2;
A12: IC v = v.IC SCMPDS by AMI_1:def 15
.= l by A9,A11,FUNCT_4:12;
a = 2*j+1+0 by A4;
then
A13: a <> t1 by XCMPLX_1:2;
then
A14: v.a = j by Th7;
A15: v.t1 = 2*k2 by A13,Th7;
A16: j+1 >= 0 by NAT_1:18;
A17: DataLoc(j,1) = 2*abs(j+1)+1 by SCMPDS_2:def 4
.= 2*(j+1)+1 by A16,ABSVALUE:def 1
.= 2*j+2*1+1 by XCMPLX_1:8
.= t by XCMPLX_1:1;
reconsider r = v.t as Nat by A13,Th7;
A18: r >= 0 by NAT_1:18;
x = 2*(k2 + 2) by A5,XCMPLX_1:27
.= 2*((2*k2 div 2) + 2) by GROUP_4:107
.= 2*((abs(r) div 2)+2) by A15,A18,ABSVALUE:def 1
.= 2*(abs(v.DataLoc(j,1)) div 2) + 2*2 by A17,XCMPLX_1:8
.= Exec(i,v).IC SCMPDS by A14,SCMPDS_1:def 23,SCMPDS_2:70
.= IC Following v by A10,A12,Lm1;
hence x in y by A2,A3,A10,A12;
end;
then x in meet X by SETFAM_1:def 1;
hence thesis by AMISTD_1:def 6;
end;
definition
let a;
cluster JUMP (return a) -> infinite;
coherence by Th5,Th28;
end;
definition
let a,k1;
cluster JUMP (saveIC(a,k1)) -> empty;
coherence
proof
for l being Instruction-Location of SCMPDS holds
NIC(saveIC(a,k1),l)={Next l} by Th16;
hence thesis by Th13;
end;
end;
definition
let a,k1;
cluster JUMP (a:=k1) -> empty;
coherence
proof
for l being Instruction-Location of SCMPDS holds NIC(a:=k1,l)={Next l}
by Th17;
hence thesis by Th13;
end;
end;
definition
let a,k1,k2;
cluster JUMP ((a,k1):=k2) -> empty;
coherence
proof
for l being Instruction-Location of SCMPDS holds NIC((a,k1):=k2,l)={Next l}
by Th18;
hence thesis by Th13;
end;
end;
definition
let a,b,k1,k2;
cluster JUMP ((a,k1):=(b,k2)) -> empty;
coherence
proof
for l being Instruction-Location of SCMPDS holds
NIC((a,k1):=(b,k2),l)={Next l} by Th19;
hence thesis by Th13;
end;
end;
definition
let a,k1,k2;
cluster JUMP (AddTo(a,k1,k2)) -> empty;
coherence
proof
for l being Instruction-Location of SCMPDS holds
NIC(AddTo(a,k1,k2),l)={Next l} by Th20;
hence thesis by Th13;
end;
end;
definition
let a,b,k1,k2;
cluster JUMP (AddTo(a,k1,b,k2)) -> empty;
coherence
proof
for l being Instruction-Location of SCMPDS holds
NIC(AddTo(a,k1,b,k2),l)={Next l} by Th21;
hence thesis by Th13;
end;
cluster JUMP (SubFrom(a,k1,b,k2)) -> empty;
coherence
proof
for l being Instruction-Location of SCMPDS holds
NIC(SubFrom(a,k1,b,k2),l)={Next l} by Th22;
hence thesis by Th13;
end;
cluster JUMP (MultBy(a,k1,b,k2)) -> empty;
coherence
proof
for l being Instruction-Location of SCMPDS holds
NIC(MultBy(a,k1,b,k2),l)={Next l} by Th23;
hence thesis by Th13;
end;
cluster JUMP (Divide(a,k1,b,k2)) -> empty;
coherence
proof
for l being Instruction-Location of SCMPDS holds
NIC(Divide(a,k1,b,k2),l)={Next l} by Th24;
hence thesis by Th13;
end;
end;
Lm4:
for a,b being real number holds a+b + (a+b+b) = 2*a+(b+b+b)
proof
let a,b be real number;
thus a+b + (a+b+b) = a+b + (a+b)+b by XCMPLX_1:1
.= a+b + a+b+b by XCMPLX_1:1
.= 1*a+1*a+b+b+b by XCMPLX_1:1
.= (1+1)*a+b+b+b by XCMPLX_1:8
.= 2*a+(b+b)+b by XCMPLX_1:1
.= 2*a+(b+b+b) by XCMPLX_1:1;
end;
Lm5:
for b,c,d being real number st 2*b+2-2+2*d = 2*(b+c)+2-2+2*d
holds b = b+c
proof
let b,c,d be real number;
assume 2*b+2-2+2*d = 2*(b+c)+2-2+2*d;
then 2*b+2-2 = 2*(b+c)+2-2 by XCMPLX_1:2;
then 2*b+2 = 2*(b+c)+2 by XCMPLX_1:19;
then 2*b = 2*(b+c) by XCMPLX_1:2;
hence b = b+c by XCMPLX_1:5;
end;
Lm6:
for a,c,d being real number st
2*(a+c)+2-2+2*d = -(2*(a+c+c)+2-2+2*d)
holds d + a = (-2)*(c+c+c)/4
proof
let a,c,d be real number;
set b = a+c;
set e = b+c;
set xx = c+c+c;
A1: b + e = 2*a+xx by Lm4;
assume 2*(a+c)+2-2+2*d = -(2*(a+c+c)+2-2+2*d);
then 2*b+2*d = -(2*e+2-2+2*d) by XCMPLX_1:26;
then
A2: 2*b+2*d = -(2*e+2*d) by XCMPLX_1:26;
A3: 4*d/4 = d by XCMPLX_1:90;
0 = -(2*e+2*d) + (2*e+2*d) by XCMPLX_0:def 6
.= 2*b + 2*d + 2*e + 2*d by A2,XCMPLX_1:1
.= 2*b + 2*e + 2*d + 2*d by XCMPLX_1:1
.= 2*b + 2*e + (2*d + 2*d) by XCMPLX_1:1
.= 2*b + 2*e + (d*(2+2)) by XCMPLX_1:8
.= 2*(b+e) + 4*d by XCMPLX_1:8;
then (-2*(b+e))/4 = 4*d/4 by XCMPLX_0:def 6;
then d = ((-2)*(2*a+xx))/4 by A1,A3,XCMPLX_1:175
.= ((-2)*xx + (-2)*(2*a)) / 4 by XCMPLX_1:8
.= (-2)*xx/4 + (-2)*(2*a)/4 by XCMPLX_1:63
.= (-2)*xx/4 + (-2)*2*a/4 by XCMPLX_1:4
.= (-2)*xx/4 + ((-4)*a)/4
.= (-2)*xx/4 + (-4*a)/4 by XCMPLX_1:175
.= (-2)*xx/4 + -4*a/4 by XCMPLX_1:188
.= (-2)*xx/4 + -a by XCMPLX_1:90
.= (-2)*xx/4 - a by XCMPLX_0:def 8;
hence d + a = (-2)*xx/4 by XCMPLX_1:27;
end;
Lm7:
5/3 is not integer
proof
not 3 qua Integer divides 5
proof
assume not thesis;
then 3 divides 5 by SCPINVAR:2;
then
A1: 5 mod 3 = 0 by PEPIN:6;
5 = 3 * 1 + 2;
hence contradiction by A1,NAT_1:def 2;
end;
hence 5/3 is not integer by WSIERP_1:22;
end;
Lm8:
for a being real number st a > 0 holds -(2*a+(1+a)) < -0
proof
let a be real number;
assume
A1: a > 0;
then
A2: 2*a > 2*0 by REAL_1:70;
1+a > 1+0 by A1,REAL_1:67;
then 2*a+(1+a) > 1+0 by A2,REAL_1:67;
then 2*a+(1+a) > 0 by AXIOMS:22;
hence -(2*a+(1+a)) < -0 by REAL_1:50;
end;
Lm9:
for a,c,d being real number st 2*(a+c)+2 = -(2*(a+c)+2*c+2*d)
holds 2*a+d = -(2*c+(1+c))
proof
let a,c,d be real number;
set b = a+c;
assume 2*b+2 = -(2*b+2*c+2*d);
then 2*0 = 2*b+2 + (2*b+2*c+2*d) by XCMPLX_0:def 6
.= 2*b+2+(2*b+(2*c+2*d)) by XCMPLX_1:1
.= 2*b+(2+2*b)+(2*c+2*d) by XCMPLX_1:1
.= 2*b+2*b+2+(2*c+2*d) by XCMPLX_1:1
.= 2*(b+b)+2+(2*c+2*d) by XCMPLX_1:8
.= 2*(b+b)+2+2*c+2*d by XCMPLX_1:1
.= 2*(b+b)+(2+2*c)+2*d by XCMPLX_1:1
.= 2*(b+b)+2*d+(2*1+2*c) by XCMPLX_1:1
.= 2*(b+b)+2*d+2*(1+c) by XCMPLX_1:8
.= 2*(b+b+d+(1+c)) by XCMPLX_1:9;
then 0 = 1*b+1*b+d+(1+c) by XCMPLX_1:5
.= (1+1)*b+d+(1+c) by XCMPLX_1:8
.= 2*a+2*c+d+(1+c) by XCMPLX_1:8
.= 2*a+d + 2*c+(1+c) by XCMPLX_1:1
.= 2*a+d + (2*c+(1+c)) by XCMPLX_1:1;
hence 2*a+d = -(2*c+(1+c)) by XCMPLX_0:def 6;
end;
Lm10:
for a,c,d being real number st 2*(a+c+c)+2 = -(2*(a+c)+2*d)
holds 2*a+d = -(2*c+(c+1))
proof
let a,c,d be real number;
set b = a+c;
assume 2*(b+c)+2 = -(2*b+2*d);
then 2*0 = 2*(b+c)+2 + (2*b+2*d) by XCMPLX_0:def 6
.= 2*(b+c)+2*1+2*(b+d) by XCMPLX_1:8
.= 2*(b+c+1+(b+d)) by XCMPLX_1:9;
then 0 = b+c+1+(b+d) by XCMPLX_1:5
.= b+(c+1)+(b+d) by XCMPLX_1:1
.= b+(b+(c+1)+d) by XCMPLX_1:1
.= b+(b+(c+1+d)) by XCMPLX_1:1
.= 1*b+1*b+(c+1+d) by XCMPLX_1:1
.= (1+1)*b+(c+1+d) by XCMPLX_1:8
.= 2*b+d+(c+1) by XCMPLX_1:1
.= 2*a+2*c+d+(c+1) by XCMPLX_1:8
.= 2*a+d+2*c+(c+1) by XCMPLX_1:1
.= 2*a+d+(2*c+(c+1)) by XCMPLX_1:1;
hence 2*a+d = -(2*c+(c+1)) by XCMPLX_0:def 6;
end;
Lm11:
for a,b,d being real number holds -d+a+4 = 1-d+(a+3)
proof
let a,b,d be real number;
thus -d+a+4 = -d+(a+(1+3)) by XCMPLX_1:1
.= -d+(1+a+3) by XCMPLX_1:1
.= -d+(1+a)+3 by XCMPLX_1:1
.= -d+1+a+3 by XCMPLX_1:1
.= 1-d+a+3 by XCMPLX_0:def 8
.= 1-d+(a+3) by XCMPLX_1:1;
end;
Lm12:
for a,b,d being real number st 2*(b+(-d+a+4)+1)= 2*(b+d)
holds 0 = a - 2*d+(2 + 3)
proof
let a,b,d be real number;
set c = -d+a+4;
assume 2*(b+c+1) = 2*(b+d);
then b+c+1 = b+d by XCMPLX_1:5;
then b+(c+1) = b+d by XCMPLX_1:1;
then c+1 = d by XCMPLX_1:2;
then
A1: c = d-1 by XCMPLX_1:26
.= -(1-d) by XCMPLX_1:143;
c = -d+(a+4) by XCMPLX_1:1;
hence 0 = -d+(a+4) + (1-d) by A1,XCMPLX_0:def 6
.= a + (4 + -d) + (1-d) by XCMPLX_1:1
.= a + (4 + -d + (1-d)) by XCMPLX_1:1
.= a + (4 + -d + (1+-d)) by XCMPLX_0:def 8
.= a + (4 + (-d + 1+-d)) by XCMPLX_1:1
.= a + (4 + (-d + -d + 1)) by XCMPLX_1:1
.= a + (4 + (-(d+d) + 1)) by XCMPLX_1:140
.= a + (4 + (-(2*d) + 1)) by XCMPLX_1:11
.= a + (-(2*d) + (4+1)) by XCMPLX_1:1
.= a + -(2*d) + (4+1) by XCMPLX_1:1
.= a - 2*d+(2 + 3) by XCMPLX_0:def 8;
end;
Lm13:
for d being real number holds
2*(abs(d)+(-d+abs(d)+4))+2-2+2*d <>
-(2*(abs(d)+(-d+abs(d)+4)+(-d+abs(d)+4))+2-2+2*d)
proof
let d be real number;
set c = -d+abs(d)+4;
set xx = c+c+c;
assume 2*(abs(d)+c)+2-2+2*d = -(2*(abs(d)+c+(-d+abs(d)+4))+2-2+2*d);
then
A1: d + abs(d) = (-2)*xx/4 by Lm6;
-d+abs(d) >= 0 by Th2;
then c >= 0+4 by AXIOMS:24;
then c > 0 by AXIOMS:22;
then 3*c > 3*0 by REAL_1:70;
then xx > 0 by XCMPLX_1:12;
then (-2)*xx < (-2)*0 by REAL_1:71;
then (-2)*xx/4 < 0/4 by REAL_1:73;
hence contradiction by A1,Th1;
end;
Lm14:
for b,d being real number holds
2*b+2 <> 2*b + (2*(-d+abs(d)+4) + 2*d)
proof
let b,d be real number;
set c = -d+abs(d)+4;
assume 2*b+2 = 2*b + (2*c + 2*d);
then 2*c+2*d = 2 by XCMPLX_1:2;
then 2*(c+d) = 2*1 by XCMPLX_1:8;
then c+d-d = 1-d by XCMPLX_1:5;
then
A1: c = 1-d+0 by XCMPLX_1:26;
A2: c = 1-d+(abs(d)+3) by Lm11;
abs(d) >= 0 by ABSVALUE:5;
then abs(d)+3 >= 0+3 by REAL_1:55;
then abs(d)+3 <> 0;
hence thesis by A1,A2,XCMPLX_1:2;
end;
Lm15:
for c,d being real number st c > 0 holds
2*(abs(d)+c)+2 <> -(2*(abs(d)+c)+2*c+2*d)
proof
let c,d be real number;
assume
A1: c > 0;
assume 2*(abs(d)+c)+2 = -(2*(abs(d)+c)+2*c+2*d);
then
A2: 2*abs(d)+d = -(2*c+(1+c)) by Lm9;
per cases;
suppose
A3: d >= 0;
then
A4: -(2*c+(1+c)) = 2*d+1*d by A2,ABSVALUE:def 1
.= (2+1)*d by XCMPLX_1:8;
3*d >= 3*0 by A3,AXIOMS:25;
hence thesis by A1,A4,Lm8;
suppose
A5: d < 0;
then abs(d) = -d by ABSVALUE:def 1;
then
A6: -(2*c+(1+c)) = (-2)*d+1*d by A2,XCMPLX_1:176
.= (-2+1)*d by XCMPLX_1:8;
(-1)*d >= (-1)*0 by A5,REAL_1:52;
hence thesis by A1,A6,Lm8;
end;
Lm16:
for b being real number, d being Integer st d <> 5 holds
2*(b+(-d+abs(d)+4)+1) <> 2*(b+d)
proof
let b be real number,
d be Integer;
assume
A1: d <> 5;
assume 2*(b+(-d+abs(d)+4)+1) = 2*(b+d);
then
A2: 0 = abs(d) - 2*d+(2 + 3) by Lm12;
per cases;
suppose d >= 0;
then abs(d) = d by ABSVALUE:def 1;
then -d+5 = 0 by A2,XCMPLX_1:187;
hence thesis by A1,XCMPLX_1:136;
suppose d < 0;
then abs(d) = -d by ABSVALUE:def 1;
then 0 = (-1)*d-2*d+(2+3) by A2,XCMPLX_1:180
.= (-1-2)*d+(2+3) by XCMPLX_1:40;
then (-3)*d/-3 = (-5)/-3 by XCMPLX_0:def 6;
hence thesis by Lm7,XCMPLX_1:90;
end;
Lm17:
for c,d being real number st -(2*c+(1+c)) < -0
holds 2*(abs(d)+c+c)+2 <> -(2*(abs(d)+c)+2*d)
proof
let c,d be real number;
assume
A1: -(2*c+(1+c)) < -0;
assume 2*(abs(d)+c+c)+2 = -(2*(abs(d)+c)+2*d);
then
A2: 2*abs(d)+d = -(2*c+(c+1)) by Lm10;
A3: 0 <= abs(d)+d by Th1;
0 <= abs(d) by ABSVALUE:5;
then 1*abs(d) <= 2*abs(d) by AXIOMS:25;
hence thesis by A1,A2,A3,AXIOMS:24;
end;
Lm18:
JUMP ((a,k1)<>0_goto 5) = {}
proof
set k2 = 5;
set i = (a,k1)<>0_goto k2;
set X = { NIC(i,l) where l is Instruction-Location of SCMPDS:
not contradiction };
hereby
let x be set;
assume
A1: x in JUMP i;
set nl1 = 5;
set nl2 = 8;
set l1 = inspos nl1;
A2: NIC(i,l1) in X;
A3: JUMP i = meet X by AMISTD_1:def 6;
then x in NIC(i,l1) by A1,A2,SETFAM_1:def 1;
then x in { IC Following s1 where s1 is State of SCMPDS:
IC s1 = l1 & s1.l1 = i } by AMISTD_1:def 5;
then consider s1 being State of SCMPDS such that
A4: x = IC Following s1 and
A5: IC s1 = l1 and
A6: s1.l1 = i;
consider m1 being Nat such that
A7: m1 = IC s1 and
A8: ICplusConst(s1,k2) = abs(m1-2+2*k2)+2 by SCMPDS_2:def 20;
A9: m1 = il.nl1 by A5,A7,SCMPDS_3:def 2
.= 2*nl1+2 by AMI_3:def 20;
set l2 = inspos nl2;
NIC(i,l2) in X;
then x in NIC(i,l2) by A1,A3,SETFAM_1:def 1;
then x in { IC Following s2 where s2 is State of SCMPDS:
IC s2 = l2 & s2.l2 = i } by AMISTD_1:def 5;
then consider s2 being State of SCMPDS such that
A10: x = IC Following s2 and
A11: IC s2 = l2 and
A12: s2.l2 = i;
consider m2 being Nat such that
A13: m2 = IC s2 and
A14: ICplusConst(s2,k2) = abs(m2-2+2*k2)+2 by SCMPDS_2:def 20;
A15: m2 = il.nl2 by A11,A13,SCMPDS_3:def 2
.= 2*nl2+2 by AMI_3:def 20;
A16: l1 <> l2 by SCMPDS_3:31;
per cases;
suppose that
A17: s1.DataLoc(s1.a,k1) <> 0 and
A18: s2.DataLoc(s2.a,k1) <> 0;
A19: x = Exec(i,s1).IC SCMPDS by A4,A5,A6,Lm1
.= abs(m1-2+2*k2)+2 by A8,A17,SCMPDS_2:67;
x = Exec(i,s2).IC SCMPDS by A10,A11,A12,Lm1
.= abs(m2-2+2*k2)+2 by A14,A18,SCMPDS_2:67;
then abs(m1-2+2*k2) = abs(m2-2+2*k2) by A19,XCMPLX_1:2;
then 2*nl1+2-2+2*k2 = 2*nl2+2-2+2*k2 or
2*nl1+2-2+2*k2 = -(2*nl2+2-2+2*k2) by A9,A15,Th3;
hence x in {};
suppose that
A20: s1.DataLoc(s1.a,k1) = 0 and
A21: s2.DataLoc(s2.a,k1) = 0;
A22: x = Exec(i,s1).IC SCMPDS by A4,A5,A6,Lm1
.= Next l1 by A5,A20,SCMPDS_2:67;
x = Exec(i,s2).IC SCMPDS by A10,A11,A12,Lm1
.= Next l2 by A11,A21,SCMPDS_2:67;
hence x in {} by A16,A22,Th10;
suppose that
A23: s1.DataLoc(s1.a,k1) = 0 and
A24: s2.DataLoc(s2.a,k1) <> 0;
consider n1 being Element of SCM-Instr-Loc such that
A25: n1 = l1 & Next l1 = Next n1 by SCMPDS_2:def 19;
consider w1 being Nat such that
A26: n1 = 2*w1+2 by SCMPDS_2:1;
A27: x = Exec(i,s1).IC SCMPDS by A4,A5,A6,Lm1
.= Next n1 by A5,A23,A25,SCMPDS_2:67
.= n1 + 2 by AMI_2:def 15;
x = Exec(i,s2).IC SCMPDS by A10,A11,A12,Lm1
.= abs(m2-2+2*k2)+2 by A14,A24,SCMPDS_2:67;
then 2*w1+2 = abs(m2-2+2*k2) by A26,A27,XCMPLX_1:2;
then 2*w1+2 = m2-2+2*k2 or 2*w1+2 = -(m2-2+2*k2) by INT_1:30;
hence x in {} by A5,A7,A9,A15,A25,A26;
suppose that
A28: s1.DataLoc(s1.a,k1) <> 0 and
A29: s2.DataLoc(s2.a,k1) = 0;
consider n2 being Element of SCM-Instr-Loc such that
A30: n2 = l2 & Next l2 = Next n2 by SCMPDS_2:def 19;
consider w2 being Nat such that
A31: n2 = 2*w2+2 by SCMPDS_2:1;
A32: x = Exec(i,s1).IC SCMPDS by A4,A5,A6,Lm1
.= abs(m1-2+2*k2)+2 by A8,A28,SCMPDS_2:67;
x = Exec(i,s2).IC SCMPDS by A10,A11,A12,Lm1
.= Next n2 by A11,A29,A30,SCMPDS_2:67
.= n2 + 2 by AMI_2:def 15;
then 2*w2+2 = abs(m1-2+2*k2) by A31,A32,XCMPLX_1:2;
then 2*w2+2 = m1-2+2*k2 or 2*w2+2 = -(m1-2+2*k2) by INT_1:30;
hence x in {} by A9,A11,A13,A15,A30,A31;
end;
thus thesis by XBOOLE_1:2;
end;
Lm19:
k2 <> 5 implies JUMP ((a,k1)<>0_goto k2) = {}
proof
assume
A1: k2 <> 5;
set i = (a,k1)<>0_goto k2;
set X = { NIC(i,l) where l is Instruction-Location of SCMPDS:
not contradiction };
hereby
let x be set;
assume
A2: x in JUMP i;
set x1 = -k2+abs(k2)+4;
x1 > -k2+abs(k2)+0 by REAL_1:53;
then
A3: x1 > 0 by Th2;
then reconsider x1 as Nat by INT_1:16;
A4: -(2*x1+(1+x1)) < -0 by A3,Lm8;
set nl1 = abs(k2)+x1;
set nl2 = nl1+x1;
set l1 = inspos nl1;
A5: NIC(i,l1) in X;
A6: JUMP i = meet X by AMISTD_1:def 6;
then x in NIC(i,l1) by A2,A5,SETFAM_1:def 1;
then x in { IC Following s1 where s1 is State of SCMPDS:
IC s1 = l1 & s1.l1 = i } by AMISTD_1:def 5;
then consider s1 being State of SCMPDS such that
A7: x = IC Following s1 and
A8: IC s1 = l1 and
A9: s1.l1 = i;
consider m1 being Nat such that
A10: m1 = IC s1 and
A11: ICplusConst(s1,k2) = abs(m1-2+2*k2)+2 by SCMPDS_2:def 20;
A12: m1 = il.nl1 by A8,A10,SCMPDS_3:def 2
.= 2*nl1+2 by AMI_3:def 20;
set l2 = inspos nl2;
NIC(i,l2) in X;
then x in NIC(i,l2) by A2,A6,SETFAM_1:def 1;
then x in { IC Following s2 where s2 is State of SCMPDS:
IC s2 = l2 & s2.l2 = i } by AMISTD_1:def 5;
then consider s2 being State of SCMPDS such that
A13: x = IC Following s2 and
A14: IC s2 = l2 and
A15: s2.l2 = i;
consider m2 being Nat such that
A16: m2 = IC s2 and
A17: ICplusConst(s2,k2) = abs(m2-2+2*k2)+2 by SCMPDS_2:def 20;
A18: m2 = il.nl2 by A14,A16,SCMPDS_3:def 2
.= 2*nl2+2 by AMI_3:def 20;
nl2+0 = nl1+x1;
then nl1 <> nl2 by A3,XCMPLX_1:2;
then
A19: l1 <> l2 by SCMPDS_3:31;
per cases;
suppose that
A20: s1.DataLoc(s1.a,k1) <> 0 and
A21: s2.DataLoc(s2.a,k1) <> 0;
A22: x = Exec(i,s1).IC SCMPDS by A7,A8,A9,Lm1
.= abs(m1-2+2*k2)+2 by A11,A20,SCMPDS_2:67;
x = Exec(i,s2).IC SCMPDS by A13,A14,A15,Lm1
.= abs(m2-2+2*k2)+2 by A17,A21,SCMPDS_2:67;
then
A23: abs(m1-2+2*k2) = abs(m2-2+2*k2) by A22,XCMPLX_1:2;
thus x in {}
proof
per cases by A12,A18,A23,Th3;
suppose 2*nl1+2-2+2*k2 = 2*nl2+2-2+2*k2;
then nl1+0 = nl2 by Lm5;
hence x in {} by A3,XCMPLX_1:2;
suppose 2*nl1+2-2+2*k2 = -(2*nl2+2-2+2*k2);
hence x in {} by Lm13;
end;
suppose that
A24: s1.DataLoc(s1.a,k1) = 0 and
A25: s2.DataLoc(s2.a,k1) = 0;
A26: x = Exec(i,s1).IC SCMPDS by A7,A8,A9,Lm1
.= Next l1 by A8,A24,SCMPDS_2:67;
x = Exec(i,s2).IC SCMPDS by A13,A14,A15,Lm1
.= Next l2 by A14,A25,SCMPDS_2:67;
hence x in {} by A19,A26,Th10;
suppose that
A27: s1.DataLoc(s1.a,k1) = 0 and
A28: s2.DataLoc(s2.a,k1) <> 0;
consider n1 being Element of SCM-Instr-Loc such that
A29: n1 = l1 & Next l1 = Next n1 by SCMPDS_2:def 19;
consider w1 being Nat such that
A30: n1 = 2*w1+2 by SCMPDS_2:1;
A31: x = Exec(i,s1).IC SCMPDS by A7,A8,A9,Lm1
.= Next n1 by A8,A27,A29,SCMPDS_2:67
.= n1 + 2 by AMI_2:def 15;
x = Exec(i,s2).IC SCMPDS by A13,A14,A15,Lm1
.= abs(m2-2+2*k2)+2 by A17,A28,SCMPDS_2:67;
then
A32: 2*w1+2 = abs(m2-2+2*k2) by A30,A31,XCMPLX_1:2;
thus x in {}
proof
per cases by A32,INT_1:30;
suppose 2*w1+2 = m2-2+2*k2;
then 2*nl1+2 = 2*nl2+2*k2 by A8,A10,A12,A18,A29,A30,XCMPLX_1:26
.= 2*nl1 + 2*x1 + 2*k2 by XCMPLX_1:8
.= 2*nl1 + (2*x1 + 2*k2) by XCMPLX_1:1;
hence x in {} by Lm14;
suppose 2*w1+2 = -(m2-2+2*k2);
then 2*nl1+2 = -(2*(nl1+x1)+2*k2) by A8,A10,A12,A18,A29,A30,XCMPLX_1:26
.= -(2*nl1+2*x1+2*k2) by XCMPLX_1:8;
hence x in {} by A3,Lm15;
end;
suppose that
A33: s1.DataLoc(s1.a,k1) <> 0 and
A34: s2.DataLoc(s2.a,k1) = 0;
consider n2 being Element of SCM-Instr-Loc such that
A35: n2 = l2 & Next l2 = Next n2 by SCMPDS_2:def 19;
consider w2 being Nat such that
A36: n2 = 2*w2+2 by SCMPDS_2:1;
A37: x = Exec(i,s1).IC SCMPDS by A7,A8,A9,Lm1
.= abs(m1-2+2*k2)+2 by A11,A33,SCMPDS_2:67;
x = Exec(i,s2).IC SCMPDS by A13,A14,A15,Lm1
.= Next n2 by A14,A34,A35,SCMPDS_2:67
.= n2 + 2 by AMI_2:def 15;
then
A38: 2*w2+2 = abs(m1-2+2*k2) by A36,A37,XCMPLX_1:2;
thus x in {}
proof
per cases by A38,INT_1:30;
suppose
A39: 2*w2+2 = m1-2+2*k2;
2*(nl2+1) = 2*nl2+2*1 by XCMPLX_1:8
.= 2*nl1+2*k2 by A12,A14,A16,A18,A35,A36,A39,XCMPLX_1:26
.= 2*(nl1+k2) by XCMPLX_1:8;
hence thesis by A1,Lm16;
suppose 2*w2+2 = -(m1-2+2*k2);
then 2*nl2+2 = -(2*nl1+2*k2) by A12,A14,A16,A18,A35,A36,XCMPLX_1:26;
hence x in {} by A4,Lm17;
end;
end;
thus thesis by XBOOLE_1:2;
end;
Lm20:
JUMP ((a,k1)<=0_goto 5) = {}
proof
set k2 = 5;
set i = (a,k1)<=0_goto k2;
set X = { NIC(i,l) where l is Instruction-Location of SCMPDS:
not contradiction };
hereby
let x be set;
assume
A1: x in JUMP i;
set nl1 = 5;
set nl2 = 8;
set l1 = inspos nl1;
A2: NIC(i,l1) in X;
A3: JUMP i = meet X by AMISTD_1:def 6;
then x in NIC(i,l1) by A1,A2,SETFAM_1:def 1;
then x in { IC Following s1 where s1 is State of SCMPDS:
IC s1 = l1 & s1.l1 = i } by AMISTD_1:def 5;
then consider s1 being State of SCMPDS such that
A4: x = IC Following s1 and
A5: IC s1 = l1 and
A6: s1.l1 = i;
consider m1 being Nat such that
A7: m1 = IC s1 and
A8: ICplusConst(s1,k2) = abs(m1-2+2*k2)+2 by SCMPDS_2:def 20;
A9: m1 = il.nl1 by A5,A7,SCMPDS_3:def 2
.= 2*nl1+2 by AMI_3:def 20;
set l2 = inspos nl2;
NIC(i,l2) in X;
then x in NIC(i,l2) by A1,A3,SETFAM_1:def 1;
then x in { IC Following s2 where s2 is State of SCMPDS:
IC s2 = l2 & s2.l2 = i } by AMISTD_1:def 5;
then consider s2 being State of SCMPDS such that
A10: x = IC Following s2 and
A11: IC s2 = l2 and
A12: s2.l2 = i;
consider m2 being Nat such that
A13: m2 = IC s2 and
A14: ICplusConst(s2,k2) = abs(m2-2+2*k2)+2 by SCMPDS_2:def 20;
A15: m2 = il.nl2 by A11,A13,SCMPDS_3:def 2
.= 2*nl2+2 by AMI_3:def 20;
A16: l1 <> l2 by SCMPDS_3:31;
per cases;
suppose that
A17: s1.DataLoc(s1.a,k1) <= 0 and
A18: s2.DataLoc(s2.a,k1) <= 0;
A19: x = Exec(i,s1).IC SCMPDS by A4,A5,A6,Lm1
.= abs(m1-2+2*k2)+2 by A8,A17,SCMPDS_2:68;
x = Exec(i,s2).IC SCMPDS by A10,A11,A12,Lm1
.= abs(m2-2+2*k2)+2 by A14,A18,SCMPDS_2:68;
then abs(m1-2+2*k2) = abs(m2-2+2*k2) by A19,XCMPLX_1:2;
then 2*nl1+2-2+2*k2 = 2*nl2+2-2+2*k2 or
2*nl1+2-2+2*k2 = -(2*nl2+2-2+2*k2) by A9,A15,Th3;
hence x in {};
suppose that
A20: s1.DataLoc(s1.a,k1) > 0 and
A21: s2.DataLoc(s2.a,k1) > 0;
A22: x = Exec(i,s1).IC SCMPDS by A4,A5,A6,Lm1
.= Next l1 by A5,A20,SCMPDS_2:68;
x = Exec(i,s2).IC SCMPDS by A10,A11,A12,Lm1
.= Next l2 by A11,A21,SCMPDS_2:68;
hence x in {} by A16,A22,Th10;
suppose that
A23: s1.DataLoc(s1.a,k1) > 0 and
A24: s2.DataLoc(s2.a,k1) <= 0;
consider n1 being Element of SCM-Instr-Loc such that
A25: n1 = l1 & Next l1 = Next n1 by SCMPDS_2:def 19;
consider w1 being Nat such that
A26: n1 = 2*w1+2 by SCMPDS_2:1;
A27: x = Exec(i,s1).IC SCMPDS by A4,A5,A6,Lm1
.= Next n1 by A5,A23,A25,SCMPDS_2:68
.= n1 + 2 by AMI_2:def 15;
x = Exec(i,s2).IC SCMPDS by A10,A11,A12,Lm1
.= abs(m2-2+2*k2)+2 by A14,A24,SCMPDS_2:68;
then 2*w1+2 = abs(m2-2+2*k2) by A26,A27,XCMPLX_1:2;
then 2*w1+2 = m2-2+2*k2 or 2*w1+2 = -(m2-2+2*k2) by INT_1:30;
hence x in {} by A5,A7,A9,A15,A25,A26;
suppose that
A28: s1.DataLoc(s1.a,k1) <= 0 and
A29: s2.DataLoc(s2.a,k1) > 0;
consider n2 being Element of SCM-Instr-Loc such that
A30: n2 = l2 & Next l2 = Next n2 by SCMPDS_2:def 19;
consider w2 being Nat such that
A31: n2 = 2*w2+2 by SCMPDS_2:1;
A32: x = Exec(i,s1).IC SCMPDS by A4,A5,A6,Lm1
.= abs(m1-2+2*k2)+2 by A8,A28,SCMPDS_2:68;
x = Exec(i,s2).IC SCMPDS by A10,A11,A12,Lm1
.= Next n2 by A11,A29,A30,SCMPDS_2:68
.= n2 + 2 by AMI_2:def 15;
then 2*w2+2 = abs(m1-2+2*k2) by A31,A32,XCMPLX_1:2;
then 2*w2+2 = m1-2+2*k2 or 2*w2+2 = -(m1-2+2*k2) by INT_1:30;
hence x in {} by A9,A11,A13,A15,A30,A31;
end;
thus thesis by XBOOLE_1:2;
end;
Lm21:
k2 <> 5 implies JUMP ((a,k1)<=0_goto k2) = {}
proof
assume
A1: k2 <> 5;
set i = (a,k1)<=0_goto k2;
set X = { NIC(i,l) where l is Instruction-Location of SCMPDS:
not contradiction };
hereby
let x be set;
assume
A2: x in JUMP i;
set x1 = -k2+abs(k2)+4;
x1 > -k2+abs(k2)+0 by REAL_1:53;
then
A3: x1 > 0 by Th2;
then reconsider x1 as Nat by INT_1:16;
A4: -(2*x1+(1+x1)) < -0 by A3,Lm8;
set nl1 = abs(k2)+x1;
set nl2 = nl1+x1;
set l1 = inspos nl1;
A5: NIC(i,l1) in X;
A6: JUMP i = meet X by AMISTD_1:def 6;
then x in NIC(i,l1) by A2,A5,SETFAM_1:def 1;
then x in { IC Following s1 where s1 is State of SCMPDS:
IC s1 = l1 & s1.l1 = i } by AMISTD_1:def 5;
then consider s1 being State of SCMPDS such that
A7: x = IC Following s1 and
A8: IC s1 = l1 and
A9: s1.l1 = i;
consider m1 being Nat such that
A10: m1 = IC s1 and
A11: ICplusConst(s1,k2) = abs(m1-2+2*k2)+2 by SCMPDS_2:def 20;
A12: m1 = il.nl1 by A8,A10,SCMPDS_3:def 2
.= 2*nl1+2 by AMI_3:def 20;
set l2 = inspos nl2;
NIC(i,l2) in X;
then x in NIC(i,l2) by A2,A6,SETFAM_1:def 1;
then x in { IC Following s2 where s2 is State of SCMPDS:
IC s2 = l2 & s2.l2 = i } by AMISTD_1:def 5;
then consider s2 being State of SCMPDS such that
A13: x = IC Following s2 and
A14: IC s2 = l2 and
A15: s2.l2 = i;
consider m2 being Nat such that
A16: m2 = IC s2 and
A17: ICplusConst(s2,k2) = abs(m2-2+2*k2)+2 by SCMPDS_2:def 20;
A18: m2 = il.nl2 by A14,A16,SCMPDS_3:def 2
.= 2*nl2+2 by AMI_3:def 20;
nl2+0 = nl1+x1;
then nl1 <> nl2 by A3,XCMPLX_1:2;
then
A19: l1 <> l2 by SCMPDS_3:31;
per cases;
suppose that
A20: s1.DataLoc(s1.a,k1) <= 0 and
A21: s2.DataLoc(s2.a,k1) <= 0;
A22: x = Exec(i,s1).IC SCMPDS by A7,A8,A9,Lm1
.= abs(m1-2+2*k2)+2 by A11,A20,SCMPDS_2:68;
x = Exec(i,s2).IC SCMPDS by A13,A14,A15,Lm1
.= abs(m2-2+2*k2)+2 by A17,A21,SCMPDS_2:68;
then
A23: abs(m1-2+2*k2) = abs(m2-2+2*k2) by A22,XCMPLX_1:2;
thus x in {}
proof
per cases by A12,A18,A23,Th3;
suppose 2*nl1+2-2+2*k2 = 2*nl2+2-2+2*k2;
then nl1+0 = nl2 by Lm5;
hence x in {} by A3,XCMPLX_1:2;
suppose 2*nl1+2-2+2*k2 = -(2*nl2+2-2+2*k2);
hence x in {} by Lm13;
end;
suppose that
A24: s1.DataLoc(s1.a,k1) > 0 and
A25: s2.DataLoc(s2.a,k1) > 0;
A26: x = Exec(i,s1).IC SCMPDS by A7,A8,A9,Lm1
.= Next l1 by A8,A24,SCMPDS_2:68;
x = Exec(i,s2).IC SCMPDS by A13,A14,A15,Lm1
.= Next l2 by A14,A25,SCMPDS_2:68;
hence x in {} by A19,A26,Th10;
suppose that
A27: s1.DataLoc(s1.a,k1) > 0 and
A28: s2.DataLoc(s2.a,k1) <= 0;
consider n1 being Element of SCM-Instr-Loc such that
A29: n1 = l1 & Next l1 = Next n1 by SCMPDS_2:def 19;
consider w1 being Nat such that
A30: n1 = 2*w1+2 by SCMPDS_2:1;
A31: x = Exec(i,s1).IC SCMPDS by A7,A8,A9,Lm1
.= Next n1 by A8,A27,A29,SCMPDS_2:68
.= n1 + 2 by AMI_2:def 15;
x = Exec(i,s2).IC SCMPDS by A13,A14,A15,Lm1
.= abs(m2-2+2*k2)+2 by A17,A28,SCMPDS_2:68;
then
A32: 2*w1+2 = abs(m2-2+2*k2) by A30,A31,XCMPLX_1:2;
thus x in {}
proof
per cases by A32,INT_1:30;
suppose 2*w1+2 = m2-2+2*k2;
then 2*nl1+2 = 2*nl2+2*k2 by A8,A10,A12,A18,A29,A30,XCMPLX_1:26
.= 2*nl1 + 2*x1 + 2*k2 by XCMPLX_1:8
.= 2*nl1 + (2*x1 + 2*k2) by XCMPLX_1:1;
hence x in {} by Lm14;
suppose 2*w1+2 = -(m2-2+2*k2);
then 2*nl1+2 = -(2*(nl1+x1)+2*k2) by A8,A10,A12,A18,A29,A30,XCMPLX_1:26
.= -(2*nl1+2*x1+2*k2) by XCMPLX_1:8;
hence x in {} by A3,Lm15;
end;
suppose that
A33: s1.DataLoc(s1.a,k1) <= 0 and
A34: s2.DataLoc(s2.a,k1) > 0;
consider n2 being Element of SCM-Instr-Loc such that
A35: n2 = l2 & Next l2 = Next n2 by SCMPDS_2:def 19;
consider w2 being Nat such that
A36: n2 = 2*w2+2 by SCMPDS_2:1;
A37: x = Exec(i,s1).IC SCMPDS by A7,A8,A9,Lm1
.= abs(m1-2+2*k2)+2 by A11,A33,SCMPDS_2:68;
x = Exec(i,s2).IC SCMPDS by A13,A14,A15,Lm1
.= Next n2 by A14,A34,A35,SCMPDS_2:68
.= n2 + 2 by AMI_2:def 15;
then
A38: 2*w2+2 = abs(m1-2+2*k2) by A36,A37,XCMPLX_1:2;
thus x in {}
proof
per cases by A38,INT_1:30;
suppose
A39: 2*w2+2 = m1-2+2*k2;
2*(nl2+1) = 2*nl2+2*1 by XCMPLX_1:8
.= 2*nl1+2*k2 by A12,A14,A16,A18,A35,A36,A39,XCMPLX_1:26
.= 2*(nl1+k2) by XCMPLX_1:8;
hence thesis by A1,Lm16;
suppose 2*w2+2 = -(m1-2+2*k2);
then 2*nl2+2 = -(2*nl1+2*k2) by A12,A14,A16,A18,A35,A36,XCMPLX_1:26;
hence x in {} by A4,Lm17;
end;
end;
thus thesis by XBOOLE_1:2;
end;
Lm22:
JUMP ((a,k1)>=0_goto 5) = {}
proof
set k2 = 5;
set i = (a,k1)>=0_goto k2;
set X = { NIC(i,l) where l is Instruction-Location of SCMPDS:
not contradiction };
hereby
let x be set;
assume
A1: x in JUMP i;
set nl1 = 5;
set nl2 = 8;
set l1 = inspos nl1;
A2: NIC(i,l1) in X;
A3: JUMP i = meet X by AMISTD_1:def 6;
then x in NIC(i,l1) by A1,A2,SETFAM_1:def 1;
then x in { IC Following s1 where s1 is State of SCMPDS:
IC s1 = l1 & s1.l1 = i } by AMISTD_1:def 5;
then consider s1 being State of SCMPDS such that
A4: x = IC Following s1 and
A5: IC s1 = l1 and
A6: s1.l1 = i;
consider m1 being Nat such that
A7: m1 = IC s1 and
A8: ICplusConst(s1,k2) = abs(m1-2+2*k2)+2 by SCMPDS_2:def 20;
A9: m1 = il.nl1 by A5,A7,SCMPDS_3:def 2
.= 2*nl1+2 by AMI_3:def 20;
set l2 = inspos nl2;
NIC(i,l2) in X;
then x in NIC(i,l2) by A1,A3,SETFAM_1:def 1;
then x in { IC Following s2 where s2 is State of SCMPDS:
IC s2 = l2 & s2.l2 = i } by AMISTD_1:def 5;
then consider s2 being State of SCMPDS such that
A10: x = IC Following s2 and
A11: IC s2 = l2 and
A12: s2.l2 = i;
consider m2 being Nat such that
A13: m2 = IC s2 and
A14: ICplusConst(s2,k2) = abs(m2-2+2*k2)+2 by SCMPDS_2:def 20;
A15: m2 = il.nl2 by A11,A13,SCMPDS_3:def 2
.= 2*nl2+2 by AMI_3:def 20;
A16: l1 <> l2 by SCMPDS_3:31;
per cases;
suppose that
A17: s1.DataLoc(s1.a,k1) >= 0 and
A18: s2.DataLoc(s2.a,k1) >= 0;
A19: x = Exec(i,s1).IC SCMPDS by A4,A5,A6,Lm1
.= abs(m1-2+2*k2)+2 by A8,A17,SCMPDS_2:69;
x = Exec(i,s2).IC SCMPDS by A10,A11,A12,Lm1
.= abs(m2-2+2*k2)+2 by A14,A18,SCMPDS_2:69;
then abs(m1-2+2*k2) = abs(m2-2+2*k2) by A19,XCMPLX_1:2;
then 2*nl1+2-2+2*k2 = 2*nl2+2-2+2*k2 or
2*nl1+2-2+2*k2 = -(2*nl2+2-2+2*k2) by A9,A15,Th3;
hence x in {};
suppose that
A20: s1.DataLoc(s1.a,k1) < 0 and
A21: s2.DataLoc(s2.a,k1) < 0;
A22: x = Exec(i,s1).IC SCMPDS by A4,A5,A6,Lm1
.= Next l1 by A5,A20,SCMPDS_2:69;
x = Exec(i,s2).IC SCMPDS by A10,A11,A12,Lm1
.= Next l2 by A11,A21,SCMPDS_2:69;
hence x in {} by A16,A22,Th10;
suppose that
A23: s1.DataLoc(s1.a,k1) < 0 and
A24: s2.DataLoc(s2.a,k1) >= 0;
consider n1 being Element of SCM-Instr-Loc such that
A25: n1 = l1 & Next l1 = Next n1 by SCMPDS_2:def 19;
consider w1 being Nat such that
A26: n1 = 2*w1+2 by SCMPDS_2:1;
A27: x = Exec(i,s1).IC SCMPDS by A4,A5,A6,Lm1
.= Next n1 by A5,A23,A25,SCMPDS_2:69
.= n1 + 2 by AMI_2:def 15;
x = Exec(i,s2).IC SCMPDS by A10,A11,A12,Lm1
.= abs(m2-2+2*k2)+2 by A14,A24,SCMPDS_2:69;
then 2*w1+2 = abs(m2-2+2*k2) by A26,A27,XCMPLX_1:2;
then 2*w1+2 = m2-2+2*k2 or 2*w1+2 = -(m2-2+2*k2) by INT_1:30;
hence x in {} by A5,A7,A9,A15,A25,A26;
suppose that
A28: s1.DataLoc(s1.a,k1) >= 0 and
A29: s2.DataLoc(s2.a,k1) < 0;
consider n2 being Element of SCM-Instr-Loc such that
A30: n2 = l2 & Next l2 = Next n2 by SCMPDS_2:def 19;
consider w2 being Nat such that
A31: n2 = 2*w2+2 by SCMPDS_2:1;
A32: x = Exec(i,s1).IC SCMPDS by A4,A5,A6,Lm1
.= abs(m1-2+2*k2)+2 by A8,A28,SCMPDS_2:69;
x = Exec(i,s2).IC SCMPDS by A10,A11,A12,Lm1
.= Next n2 by A11,A29,A30,SCMPDS_2:69
.= n2 + 2 by AMI_2:def 15;
then 2*w2+2 = abs(m1-2+2*k2) by A31,A32,XCMPLX_1:2;
then 2*w2+2 = m1-2+2*k2 or 2*w2+2 = -(m1-2+2*k2) by INT_1:30;
hence x in {} by A9,A11,A13,A15,A30,A31;
end;
thus thesis by XBOOLE_1:2;
end;
Lm23:
k2 <> 5 implies JUMP ((a,k1)>=0_goto k2) = {}
proof
assume
A1: k2 <> 5;
set i = (a,k1)>=0_goto k2;
set X = { NIC(i,l) where l is Instruction-Location of SCMPDS:
not contradiction };
hereby
let x be set;
assume
A2: x in JUMP i;
set x1 = -k2+abs(k2)+4;
x1 > -k2+abs(k2)+0 by REAL_1:53;
then
A3: x1 > 0 by Th2;
then reconsider x1 as Nat by INT_1:16;
A4: -(2*x1+(1+x1)) < -0 by A3,Lm8;
set nl1 = abs(k2)+x1;
set nl2 = nl1+x1;
set l1 = inspos nl1;
A5: NIC(i,l1) in X;
A6: JUMP i = meet X by AMISTD_1:def 6;
then x in NIC(i,l1) by A2,A5,SETFAM_1:def 1;
then x in { IC Following s1 where s1 is State of SCMPDS:
IC s1 = l1 & s1.l1 = i } by AMISTD_1:def 5;
then consider s1 being State of SCMPDS such that
A7: x = IC Following s1 and
A8: IC s1 = l1 and
A9: s1.l1 = i;
consider m1 being Nat such that
A10: m1 = IC s1 and
A11: ICplusConst(s1,k2) = abs(m1-2+2*k2)+2 by SCMPDS_2:def 20;
A12: m1 = il.nl1 by A8,A10,SCMPDS_3:def 2
.= 2*nl1+2 by AMI_3:def 20;
set l2 = inspos nl2;
NIC(i,l2) in X;
then x in NIC(i,l2) by A2,A6,SETFAM_1:def 1;
then x in { IC Following s2 where s2 is State of SCMPDS:
IC s2 = l2 & s2.l2 = i } by AMISTD_1:def 5;
then consider s2 being State of SCMPDS such that
A13: x = IC Following s2 and
A14: IC s2 = l2 and
A15: s2.l2 = i;
consider m2 being Nat such that
A16: m2 = IC s2 and
A17: ICplusConst(s2,k2) = abs(m2-2+2*k2)+2 by SCMPDS_2:def 20;
A18: m2 = il.nl2 by A14,A16,SCMPDS_3:def 2
.= 2*nl2+2 by AMI_3:def 20;
nl2+0 = nl1+x1;
then nl1 <> nl2 by A3,XCMPLX_1:2;
then
A19: l1 <> l2 by SCMPDS_3:31;
per cases;
suppose that
A20: s1.DataLoc(s1.a,k1) >= 0 and
A21: s2.DataLoc(s2.a,k1) >= 0;
A22: x = Exec(i,s1).IC SCMPDS by A7,A8,A9,Lm1
.= abs(m1-2+2*k2)+2 by A11,A20,SCMPDS_2:69;
x = Exec(i,s2).IC SCMPDS by A13,A14,A15,Lm1
.= abs(m2-2+2*k2)+2 by A17,A21,SCMPDS_2:69;
then
A23: abs(m1-2+2*k2) = abs(m2-2+2*k2) by A22,XCMPLX_1:2;
thus x in {}
proof
per cases by A12,A18,A23,Th3;
suppose 2*nl1+2-2+2*k2 = 2*nl2+2-2+2*k2;
then nl1+0 = nl2 by Lm5;
hence x in {} by A3,XCMPLX_1:2;
suppose 2*nl1+2-2+2*k2 = -(2*nl2+2-2+2*k2);
hence x in {} by Lm13;
end;
suppose that
A24: s1.DataLoc(s1.a,k1) < 0 and
A25: s2.DataLoc(s2.a,k1) < 0;
A26: x = Exec(i,s1).IC SCMPDS by A7,A8,A9,Lm1
.= Next l1 by A8,A24,SCMPDS_2:69;
x = Exec(i,s2).IC SCMPDS by A13,A14,A15,Lm1
.= Next l2 by A14,A25,SCMPDS_2:69;
hence x in {} by A19,A26,Th10;
suppose that
A27: s1.DataLoc(s1.a,k1) < 0 and
A28: s2.DataLoc(s2.a,k1) >= 0;
consider n1 being Element of SCM-Instr-Loc such that
A29: n1 = l1 & Next l1 = Next n1 by SCMPDS_2:def 19;
consider w1 being Nat such that
A30: n1 = 2*w1+2 by SCMPDS_2:1;
A31: x = Exec(i,s1).IC SCMPDS by A7,A8,A9,Lm1
.= Next n1 by A8,A27,A29,SCMPDS_2:69
.= n1 + 2 by AMI_2:def 15;
x = Exec(i,s2).IC SCMPDS by A13,A14,A15,Lm1
.= abs(m2-2+2*k2)+2 by A17,A28,SCMPDS_2:69;
then
A32: 2*w1+2 = abs(m2-2+2*k2) by A30,A31,XCMPLX_1:2;
thus x in {}
proof
per cases by A32,INT_1:30;
suppose 2*w1+2 = m2-2+2*k2;
then 2*nl1+2 = 2*nl2+2*k2 by A8,A10,A12,A18,A29,A30,XCMPLX_1:26
.= 2*nl1 + 2*x1 + 2*k2 by XCMPLX_1:8
.= 2*nl1 + (2*x1 + 2*k2) by XCMPLX_1:1;
hence x in {} by Lm14;
suppose 2*w1+2 = -(m2-2+2*k2);
then 2*nl1+2 = -(2*(nl1+x1)+2*k2) by A8,A10,A12,A18,A29,A30,XCMPLX_1:26
.= -(2*nl1+2*x1+2*k2) by XCMPLX_1:8;
hence x in {} by A3,Lm15;
end;
suppose that
A33: s1.DataLoc(s1.a,k1) >= 0 and
A34: s2.DataLoc(s2.a,k1) < 0;
consider n2 being Element of SCM-Instr-Loc such that
A35: n2 = l2 & Next l2 = Next n2 by SCMPDS_2:def 19;
consider w2 being Nat such that
A36: n2 = 2*w2+2 by SCMPDS_2:1;
A37: x = Exec(i,s1).IC SCMPDS by A7,A8,A9,Lm1
.= abs(m1-2+2*k2)+2 by A11,A33,SCMPDS_2:69;
x = Exec(i,s2).IC SCMPDS by A13,A14,A15,Lm1
.= Next n2 by A14,A34,A35,SCMPDS_2:69
.= n2 + 2 by AMI_2:def 15;
then
A38: 2*w2+2 = abs(m1-2+2*k2) by A36,A37,XCMPLX_1:2;
thus x in {}
proof
per cases by A38,INT_1:30;
suppose
A39: 2*w2+2 = m1-2+2*k2;
2*(nl2+1) = 2*nl2+2*1 by XCMPLX_1:8
.= 2*nl1+2*k2 by A12,A14,A16,A18,A35,A36,A39,XCMPLX_1:26
.= 2*(nl1+k2) by XCMPLX_1:8;
hence thesis by A1,Lm16;
suppose 2*w2+2 = -(m1-2+2*k2);
then 2*nl2+2 = -(2*nl1+2*k2) by A12,A14,A16,A18,A35,A36,XCMPLX_1:26;
hence x in {} by A4,Lm17;
end;
end;
thus thesis by XBOOLE_1:2;
end;
definition
let a,k1,k2;
cluster JUMP ((a,k1)<>0_goto k2) -> empty;
coherence
proof
k2 = 5 or k2 <> 5;
hence thesis by Lm18,Lm19;
end;
cluster JUMP ((a,k1)<=0_goto k2) -> empty;
coherence
proof
k2 = 5 or k2 <> 5;
hence thesis by Lm20,Lm21;
end;
cluster JUMP ((a,k1)>=0_goto k2) -> empty;
coherence
proof
k2 = 5 or k2 <> 5;
hence thesis by Lm22,Lm23;
end;
end;
theorem Th29:
SUCC(l) = the Instruction-Locations of SCMPDS
proof
thus SUCC(l) c= the Instruction-Locations of SCMPDS;
let x be set;
assume x in the Instruction-Locations of SCMPDS;
then reconsider x as Instruction-Location of SCMPDS;
set X = { NIC(i,l) \ JUMP i where
i is Element of the Instructions of SCMPDS: not contradiction };
set i = goto (locnum x - locnum l);
A1: locnum x >= 0 by NAT_1:18;
NIC(i,l) = { 2*abs(locnum x - locnum l + locnum l) + 2 } by Th14
.= { 2*abs(locnum x)+2 } by XCMPLX_1:27
.= { 2*locnum x + 2 } by A1,ABSVALUE:def 1
.= {x} by Th8;
then
A2: x in NIC(i,l) by TARSKI:def 1;
NIC(i,l) \ JUMP i in X;
then x in union X by A2,TARSKI:def 4;
hence thesis by AMISTD_1:def 7;
end;
theorem Th30:
for N being with_non-empty_elements set,
S being IC-Ins-separated definite (non empty non void AMI-Struct over N),
l1, l2 being Instruction-Location of S
st SUCC(l1) = the Instruction-Locations of S
holds l1 <= l2
proof
let N be with_non-empty_elements set,
S be IC-Ins-separated definite (non empty non void AMI-Struct over N),
l1, l2 be Instruction-Location of S such that
A1: SUCC(l1) = the Instruction-Locations of S;
defpred P[set,set] means
($1 = 1 implies $2 = l1) & ($1 = 2 implies $2 = l2);
A2: for n being Nat st n in Seg 2
ex d being Element of the Instruction-Locations of S st P[n,d]
proof
let n be Nat;
assume
A3: n in Seg 2;
per cases by A3,FINSEQ_1:4,TARSKI:def 2;
suppose
A4: n = 1;
take l1;
thus P[n,l1] by A4;
suppose
A5: n = 2;
take l2;
thus P[n,l2] by A5;
end;
consider f being FinSequence of the Instruction-Locations of S such that
A6: len f = 2 and
A7: for n being Nat st n in Seg 2 holds P[n,f/.n] from FinSeqDChoice(A2);
A8: 1 in Seg 2 & 2 in Seg 2 by FINSEQ_1:4,TARSKI:def 2;
dom f = Seg 2 by A6,FINSEQ_1:def 3;
then ex y being set st [1,y] in f by A8,RELAT_1:def 4;
then
reconsider f as non empty FinSequence of the Instruction-Locations of S;
take f;
thus f/.1 = l1 & f/.len f = l2 by A6,A7,A8;
let n be Nat;
assume
A9: 1 <= n;
assume n < len f;
then n < 1+1 by A6;
then n <= 1 by NAT_1:38;
then n = 1 by A9,AXIOMS:21;
then f/.n = l1 by A7,A8;
hence f/.(n+1) in SUCC f/.n by A1;
end;
definition
cluster SCMPDS -> non InsLoc-antisymmetric;
coherence
proof
assume
A1: SCMPDS is InsLoc-antisymmetric;
SUCC(inspos(1)) = the Instruction-Locations of SCMPDS &
SUCC(inspos(2)) = the Instruction-Locations of SCMPDS by Th29;
then inspos(1) <= inspos(2) & inspos(2) <= inspos(1) by Th30;
then inspos(1) = inspos(2) by A1,AMISTD_1:def 9;
hence thesis by SCMPDS_3:31;
end;
end;
definition
cluster SCMPDS -> non standard;
coherence by AMISTD_1:30;
end;