:: SCMPDS Is Not Standard
:: by Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received September 27, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SCMPDS_2, AMI_1, INT_1, FUNCOP_1, SUBSET_1, FSM_1,
FUNCT_1, AMISTD_1, FUNCT_4, XBOOLE_0, SETFAM_1, AMI_3, COMPLEX1, ARYTM_3,
XXREAL_0, ARYTM_1, CARD_1, AMI_2, RELAT_1, GRAPHSP, TARSKI, FINSET_1,
CARD_3, AMI_WSTD, NAT_1, GOBRD13, MEMSTR_0, REAL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, CARD_3, NUMBERS,
XCMPLX_0, XXREAL_0, XREAL_0, FUNCT_1, INT_1, NAT_1, FINSET_1, COMPLEX1,
INT_2, RELAT_1, FUNCT_4, MEMSTR_0, COMPOS_1, EXTPRO_1, AMI_2, SCMPDS_2,
SCMPDS_3, AMISTD_1, AMI_WSTD;
constructors REAL_1, NAT_D, SCMPDS_1, SCMPDS_3, AMI_WSTD, PRE_POLY, AMISTD_1,
FUNCT_4, FUNCT_7;
registrations XREAL_0, NAT_1, INT_1, CARD_3, SCMPDS_2, FUNCT_1, FUNCT_4,
MEMSTR_0, AMI_3, ORDINAL1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, AMISTD_1, MEMSTR_0, SCMPDS_2;
expansions TARSKI, XBOOLE_0;
theorems AMI_WSTD, SETFAM_1, SCMPDS_2, ABSVALUE, INT_1, TARSKI, AMI_2, NAT_1,
FUNCT_4, PRE_CIRC, WSIERP_1, PEPIN, COMPLEX1, XREAL_1, FUNCT_7, NAT_D,
AMISTD_1, MEMSTR_0, CARD_3, SCMPDS_I, XTUPLE_0, ORDINAL1;
begin
reserve a, b for Int_position,
i for Instruction of SCMPDS,
l for Element of NAT,
k, k1, k2 for Integer;
definition
let la, lb be Int_position, a, b be Integer;
redefine func (la,lb) --> (a,b) -> PartState of SCMPDS; :: redefines --> (FUNCT_4, definition)
coherence
proof
A1: Values la = INT & Values lb = INT by SCMPDS_2:5;
A2: a is Element of INT & b is Element of INT by INT_1:def 2;
reconsider a as Element of Values la by A1,A2;
reconsider b as Element of Values lb by A1,A2;
(la,lb) --> (a,b) is PartState of SCMPDS;
hence thesis;
end;
end;
Lm1: JUMP goto k = {}
proof
set i = goto k;
set X = the set of all NIC(i,l) where l is Nat;
hereby
set l2 = 0;
set l1 = 1;
let x be object;
assume
A1: x in JUMP i;
NIC(i,l2) in X;
then x in NIC(i,l2) by A1,SETFAM_1:def 1;
then consider s2 being Element of product the_Values_of SCMPDS
such that
A2: x = IC Exec(i,s2) and
A3: IC s2 = l2;
consider m2 being Element of NAT such that
A4: m2 = IC s2 and
A5: ICplusConst(s2,k) = |.m2+k.| by SCMPDS_2:def 18;
NIC(i,l1) in X;
then x in NIC(i,l1) by A1,SETFAM_1:def 1;
then consider s1 being Element of product the_Values_of SCMPDS
such that
A6: x = IC Exec(i,s1) and
A7: IC s1 = l1;
consider m1 being Element of NAT such that
A8: m1 = IC s1 and
A9: ICplusConst(s1,k) = |.m1+k.| by SCMPDS_2:def 18;
|.m2+k.| = ICplusConst(s2,k) by A5
.= IC Exec(i,s2) by SCMPDS_2:54
.= IC Exec(i,s1) by A2,A6
.= ICplusConst(s1,k) by SCMPDS_2:54
.= |.m1+k.| by A9;
then per cases by A7,A8,A3,A4,ABSVALUE:28;
suppose
0+k = 1+k;
hence x in {};
end;
suppose
0+k = -(1+k);
then --1/2 is integer;
hence x in {} by NAT_D:33;
end;
end;
thus thesis;
end;
registration
let k;
cluster JUMP (goto k) -> empty;
coherence by Lm1;
end;
theorem Th1:
(for s being State of SCMPDS st IC s = l
holds Exec(i,s).IC SCMPDS = IC s + 1) implies NIC(i, l) = {l + 1}
proof
reconsider I = i as Instruction of SCMPDS;
reconsider n = l as Element of NAT;
assume
A1: for s being State of SCMPDS st IC s = l
holds Exec(i, s).IC SCMPDS = IC s + 1;
hereby
let x be object;
assume x in NIC(i,l);
then consider s being Element of product the_Values_of SCMPDS
such that
A2: x = IC Exec(i,s) and
A3: IC s = l;
x = l+1 by A1,A2,A3;
hence x in {l+1} by TARSKI:def 1;
end;
set t = the l-started State of SCMPDS;
reconsider t = the l-started State of SCMPDS
as Element of product the_Values_of SCMPDS by CARD_3:107;
A4: IC t = l by MEMSTR_0:def 11;
let x be object;
assume x in {l+1};
then
A5: x = l+1 by TARSKI:def 1;
IC Exec(I,t) = l+1 by A1,A4;
hence thesis by A5,A4;
end;
theorem Th2:
(for l being Element of NAT holds NIC(i,l)={l+1}) implies JUMP i is empty
proof
set p=1, q=2;
assume
A1: for l being Element of NAT holds NIC(i,l)={l+1};
set X = the set of all NIC(i,f) where f is Nat;
reconsider p, q as Element of NAT;
assume not thesis;
then consider x being object such that
A2: x in meet X;
NIC(i,p) = {p+1} by A1;
then {p+1} in X;
then x in {p+1} by A2,SETFAM_1:def 1;
then
A3: x = p+1 by TARSKI:def 1;
NIC(i,q) = {q+1} by A1;
then {q+1} in X;
then x in {q+1} by A2,SETFAM_1:def 1;
hence contradiction by A3,TARSKI:def 1;
end;
theorem Th3:
NIC(goto k,l) = { |.k+l.| }
proof
set s = the State of SCMPDS;
set i = goto k;
set t = |.k+l.|;
set I = i;
reconsider n = l as Element of NAT;
hereby
let x be object;
assume x in NIC(i,l);
then consider s being Element of product the_Values_of SCMPDS
such that
A1: x = IC Exec(i,s) and
A2: IC s = l;
A3: ex m1 being Element of NAT st m1 = IC s & ICplusConst(s,k ) = |.m1+k.|
by SCMPDS_2:def 18;
x = t by A1,A2,A3,SCMPDS_2:54;
hence x in {t} by TARSKI:def 1;
end;
let x be object;
reconsider u = the n-started State of SCMPDS
as Element of product the_Values_of SCMPDS by CARD_3:107;
A4: IC u = n by MEMSTR_0:def 11;
consider m1 being Element of NAT such that
A5: m1 = IC u and
A6: ICplusConst(u,k) = |.m1+k.| by SCMPDS_2:def 18;
assume x in {t};
then x = |.m1+k.| by A4,A5,TARSKI:def 1
.= IC Exec(i,u) by A6,SCMPDS_2:54;
hence thesis by A4;
end;
Lm2: for k being Nat st k > 1 holds k-2 is Element of NAT
proof
let k be Nat;
assume k > 1;
then k >= 1+1 by NAT_1:13;
then k - 2 >= 2 - 2 by XREAL_1:9;
hence thesis by INT_1:3;
end;
theorem Th4:
NIC(return a,l) = {k where k is Nat: k > 1}
proof
set s = the State of SCMPDS;
set X = {k where k is Nat: k > 1};
set i = return a;
hereby
let x be object;
assume x in NIC(i,l);
then consider s being Element of product the_Values_of SCMPDS
such that
A1: x = IC Exec(i,s) and
IC s = l;
reconsider k = x as Element of NAT by A1;
A2: (|.s.DataLoc(s.a,1).| )+2 >= 0+2 by XREAL_1:6;
k >= 1+1 by A2,A1,SCMPDS_2:58,SCMPDS_I:def 14;
then k > 1 by NAT_1:13;
hence x in X;
end;
let x be object;
set I = i;
reconsider n = l as Element of NAT;
assume x in X;
then consider k being Nat such that
A3: x = k and
A4: k > 1;
reconsider k2 = k - 2 as Element of NAT by A4,Lm2;
reconsider u = the n-started State of SCMPDS
as Element of product the_Values_of SCMPDS by CARD_3:107;
A5: IC u = n by MEMSTR_0:def 11;
a in SCM-Data-Loc by AMI_2:def 16;
then consider j being Nat such that
A6: a = [1,j] by AMI_2:23;
set t = [1,j+1];
t in SCM-Data-Loc by AMI_2:24;
then reconsider t1 = t as Int_position by AMI_2:def 16;
A7: DataLoc(j,1) = [1,|.j+1.|]
.= t by ABSVALUE:def 1;
set g = (a,t1)-->(j,k2);
reconsider v = u +* g
as Element of product the_Values_of SCMPDS by CARD_3:107;
A8: dom g = {a,t} by FUNCT_4:62;
j <> j+1;
then
A9: a <> t by A6,XTUPLE_0:1;
then
A10: v.a = j by FUNCT_4:84;
a <> IC SCMPDS & t1 <> IC SCMPDS by SCMPDS_2:43;
then
A11: not IC SCMPDS in dom g by A8,TARSKI:def 2;
A12: IC v = l by A5,A11,FUNCT_4:11;
A13: v.t = k2 by A9,FUNCT_4:84;
x = ((k2 ) + 2) by A3
.= (|.v.DataLoc(j,1).| ) + 2 by A13,A7,ABSVALUE:def 1
.= IC Exec(i,v) by A10,SCMPDS_2:58,SCMPDS_I:def 14;
hence thesis by A12;
end;
theorem Th5:
NIC(saveIC(a,k1), l) = {l+1}
proof
set i = saveIC(a,k1);
for s being State of SCMPDS st IC s = l holds Exec(i,s).IC
SCMPDS = IC s + 1 by SCMPDS_2:59;
hence thesis by Th1;
end;
theorem Th6:
NIC(a:=k1, l) = {l+1}
proof
set i = a:=k1;
for s being State of SCMPDS st IC s = l holds Exec(i,s).IC
SCMPDS = IC s + 1 by SCMPDS_2:45;
hence thesis by Th1;
end;
theorem Th7:
NIC((a,k1):=k2, l) = {l+1}
proof
set i = (a,k1):=k2;
for s being State of SCMPDS st IC s = l holds Exec(i,s).IC
SCMPDS = IC s + 1 by SCMPDS_2:46;
hence thesis by Th1;
end;
theorem Th8:
NIC((a,k1):=(b,k2), l) = {l+1}
proof
set i = (a,k1):=(b,k2);
for s being State of SCMPDS st IC s = l holds Exec(i,s).IC
SCMPDS = IC s + 1 by SCMPDS_2:47;
hence thesis by Th1;
end;
theorem Th9:
NIC(AddTo(a,k1,k2), l) = {l+1}
proof
set i = AddTo(a,k1,k2);
for s being State of SCMPDS st IC s = l holds Exec(i,s).IC
SCMPDS = IC s + 1 by SCMPDS_2:48;
hence thesis by Th1;
end;
theorem Th10:
NIC(AddTo(a,k1,b,k2), l) = {l+1}
proof
set i = AddTo(a,k1,b,k2);
for s being State of SCMPDS st IC s = l holds Exec(i,s).IC
SCMPDS = IC s + 1 by SCMPDS_2:49;
hence thesis by Th1;
end;
theorem Th11:
NIC(SubFrom(a,k1,b,k2), l) = {l+1}
proof
set i = SubFrom(a,k1,b,k2);
for s being State of SCMPDS st IC s = l holds Exec(i,s).IC
SCMPDS = IC s + 1 by SCMPDS_2:50;
hence thesis by Th1;
end;
theorem Th12:
NIC(MultBy(a,k1,b,k2), l) = {l+1}
proof
set i = MultBy(a,k1,b,k2);
for s being State of SCMPDS st IC s = l holds Exec(i,s).IC
SCMPDS = IC s + 1 by SCMPDS_2:51;
hence thesis by Th1;
end;
theorem Th13:
NIC(Divide(a,k1,b,k2), l) = {l+1}
proof
set i = Divide(a,k1,b,k2);
for s being State of SCMPDS st IC s = l holds Exec(i,s).IC
SCMPDS = IC s + 1 by SCMPDS_2:52;
hence thesis by Th1;
end;
theorem
NIC((a,k1)<>0_goto k2,l) = { l+1, |. (k2+ l) .| }
proof
set s = the State of SCMPDS;
set i = (a,k1)<>0_goto k2;
set t = |.(k2+ l).|;
set I = i;
reconsider n = l as Element of NAT;
reconsider u = the n-started State of SCMPDS
as Element of product the_Values_of SCMPDS by CARD_3:107;
hereby
let x be object;
assume x in NIC(i,l);
then consider s being Element of product the_Values_of SCMPDS
such that
A1: x = IC Exec(i,s) and
A2: IC s = l;
A3: ex m1 being Element of NAT st m1 = IC s & ICplusConst(s, k2) = |.m1+
k2.| by SCMPDS_2:def 18;
per cases;
suppose
A4: s.DataLoc(s.a,k1) <> 0;
x = t by A1,A2,A3,A4,SCMPDS_2:55;
hence x in {l+1,t} by TARSKI:def 2;
end;
suppose
A5: s.DataLoc(s.a,k1) = 0;
x = l+1 by A1,A2,A5,SCMPDS_2:55;
hence x in {l+1,t} by TARSKI:def 2;
end;
end;
let x be object;
assume
A6: x in {l+1,t};
per cases by A6,TARSKI:def 2;
suppose
A7: x = l+1;
reconsider u1 = u +* (a.-->0) as State of SCMPDS;
reconsider u2 = u1 +* (DataLoc(u1.a,k1).-->0)
as Element of product the_Values_of SCMPDS by CARD_3:107;
A8: IC u2 = u1.IC SCMPDS by FUNCT_4:83,SCMPDS_2:43
.= IC u by FUNCT_4:83,SCMPDS_2:43
.= n by MEMSTR_0:def 11;
A9: u2.DataLoc(u1.a,k1) = 0 by FUNCT_7:94;
u2.DataLoc(u2.a,k1) = 0
proof
per cases;
suppose
a = DataLoc(u1.a,k1);
hence thesis by A9;
end;
suppose
a <> DataLoc(u1.a,k1);
then u2.a = u1.a by FUNCT_4:83;
hence thesis by FUNCT_7:94;
end;
end;
then x = IC Exec(i,u2) by A7,A8,SCMPDS_2:55;
hence thesis by A8;
end;
suppose
A10: x = t;
reconsider u1 = u +* (a.-->1) as State of SCMPDS;
reconsider u2 = u1 +* (DataLoc(u1.a,k1).-->1)
as Element of product the_Values_of SCMPDS by CARD_3:107;
A11: u2.DataLoc(u1.a,k1) = 1 by FUNCT_7:94;
A12: u2.DataLoc(u2.a,k1) <> 0
proof
per cases;
suppose
a = DataLoc(u1.a,k1);
hence thesis by A11;
end;
suppose
a <> DataLoc(u1.a,k1);
then u2.a = u1.a by FUNCT_4:83;
hence thesis by FUNCT_7:94;
end;
end;
A13: IC u2 = u1.IC SCMPDS by FUNCT_4:83,SCMPDS_2:43
.= IC u by FUNCT_4:83,SCMPDS_2:43
.= n by MEMSTR_0:def 11;
ex m1 being Element of NAT st m1 = IC u2 & ICplusConst(u2,k2) = |.
m1+k2.| by SCMPDS_2:def 18;
then x = IC Exec(i,u2) by A10,A13,A12,SCMPDS_2:55;
hence thesis by A13;
end;
end;
theorem
NIC((a,k1)<=0_goto k2,l) = { l+1, |. (k2+ l) .| }
proof
set s = the State of SCMPDS;
set i = (a,k1)<=0_goto k2;
set t = |.(k2+ l).|;
set I = i;
reconsider n = l as Element of NAT;
reconsider u = the n-started State of SCMPDS
as Element of product the_Values_of SCMPDS by CARD_3:107;
hereby
let x be object;
assume x in NIC(i,l);
then consider s being Element of product the_Values_of SCMPDS
such that
A1: x = IC Exec(i,s) and
A2: IC s = l;
A3: ex m1 being Element of NAT st m1 = IC s & ICplusConst(s, k2) = |.m1+
k2.| by SCMPDS_2:def 18;
per cases;
suppose
A4: s.DataLoc(s.a,k1) <= 0;
x = t by A1,A2,A3,A4,SCMPDS_2:56;
hence x in {l+1,t} by TARSKI:def 2;
end;
suppose
A5: s.DataLoc(s.a,k1) > 0;
x = l+1 by A1,A2,A5,SCMPDS_2:56;
hence x in {l+1,t} by TARSKI:def 2;
end;
end;
let x be object;
assume
A6: x in {l+1,t};
per cases by A6,TARSKI:def 2;
suppose
A7: x = l+1;
reconsider u1 = u +* (a.-->1) as State of SCMPDS;
reconsider u2 = u1 +* (DataLoc(u1.a,k1).-->1)
as Element of product the_Values_of SCMPDS by CARD_3:107;
A8: IC u2 = u1.IC SCMPDS by FUNCT_4:83,SCMPDS_2:43
.= IC u by FUNCT_4:83,SCMPDS_2:43
.= n by MEMSTR_0:def 11;
A9: u2.DataLoc(u1.a,k1) = 1 by FUNCT_7:94;
u2.DataLoc(u2.a,k1) > 0
proof
per cases;
suppose a = DataLoc(u1.a,k1);
hence thesis by A9;
end;
suppose
a <> DataLoc(u1.a,k1);
then u2.a = u1.a by FUNCT_4:83;
hence thesis by FUNCT_7:94;
end;
end;
then x = IC Exec(i,u2) by A7,A8,SCMPDS_2:56;
hence thesis by A8;
end;
suppose
A10: x = t;
reconsider u1 = u +* (a.-->0) as State of SCMPDS;
reconsider u2 = u1 +* (DataLoc(u1.a,k1).-->0)
as Element of product the_Values_of SCMPDS by CARD_3:107;
A11: u2.DataLoc(u1.a,k1) = 0 by FUNCT_7:94;
A12: u2.DataLoc(u2.a,k1) <= 0
proof
per cases;
suppose
a = DataLoc(u1.a,k1);
hence thesis by A11;
end;
suppose
a <> DataLoc(u1.a,k1);
then u2.a = u1.a by FUNCT_4:83;
hence thesis by FUNCT_7:94;
end;
end;
A13: IC u2 = u1.IC SCMPDS by FUNCT_4:83,SCMPDS_2:43
.= IC u by FUNCT_4:83,SCMPDS_2:43
.= n by MEMSTR_0:def 11;
ex m1 being Element of NAT st m1 = IC u2 & ICplusConst(u2,k2) = |.
m1+k2.| by SCMPDS_2:def 18;
then x = IC Exec(i,u2) by A10,A13,A12,SCMPDS_2:56;
hence thesis by A13;
end;
end;
theorem
NIC((a,k1)>=0_goto k2,l) = { l+1, |. (k2+ l) .| }
proof
set s = the State of SCMPDS;
set i = (a,k1)>=0_goto k2;
set t = |.(k2+ l).|;
set I = i;
reconsider n = l as Element of NAT;
reconsider u = the n-started State of SCMPDS
as Element of product the_Values_of SCMPDS by CARD_3:107;
hereby
let x be object;
assume x in NIC(i,l);
then consider s being Element of product the_Values_of SCMPDS
such that
A1: x = IC Exec(i,s) and
A2: IC s = l;
A3: ex m1 being Element of NAT st m1 = IC s & ICplusConst(s, k2) = |.m1+
k2.| by SCMPDS_2:def 18;
per cases;
suppose
A4: s.DataLoc(s.a,k1) >= 0;
x = t by A1,A2,A3,A4,SCMPDS_2:57;
hence x in {l+1,t} by TARSKI:def 2;
end;
suppose
A5: s.DataLoc(s.a,k1) < 0;
x = l+1 by A1,A2,A5,SCMPDS_2:57;
hence x in {l+1,t} by TARSKI:def 2;
end;
end;
let x be object;
assume
A6: x in {l+1,t};
per cases by A6,TARSKI:def 2;
suppose
A7: x = l+1;
A8: -1 < 0;
reconsider u1 = u +* (a.-->-1) as State of SCMPDS;
reconsider u1 = u +* (a.-->-1)
as Element of product the_Values_of SCMPDS by CARD_3:107;
reconsider u2 = u1 +* (DataLoc(u1.a,k1).-->-1)
as Element of product the_Values_of SCMPDS by CARD_3:107;
A9: IC u2 = u1.IC SCMPDS by FUNCT_4:83,SCMPDS_2:43
.= IC u by FUNCT_4:83,SCMPDS_2:43
.= n by MEMSTR_0:def 11;
A10: u2.DataLoc(u1.a,k1) = -1 by FUNCT_7:94;
u2.DataLoc(u2.a,k1) < 0
proof
per cases;
suppose
a = DataLoc(u1.a,k1);
hence thesis by A10;
end;
suppose
a <> DataLoc(u1.a,k1);
then u2.a = u1.a by FUNCT_4:83;
hence thesis by A8,FUNCT_7:94;
end;
end;
then x = IC Exec(i,u2) by A7,A9,SCMPDS_2:57;
hence thesis by A9;
end;
suppose
A11: x = t;
reconsider u1 = u +* (a.-->-1) as State of SCMPDS;
reconsider u1 = u +* (a.-->0)
as Element of product the_Values_of SCMPDS by CARD_3:107;
reconsider u2 = u1 +* (DataLoc(u1.a,k1).-->0)
as Element of product the_Values_of SCMPDS by CARD_3:107;
A12: u2.DataLoc(u1.a,k1) = 0 by FUNCT_7:94;
A13: u2.DataLoc(u2.a,k1) >= 0
proof
per cases;
suppose
a = DataLoc(u1.a,k1);
hence thesis by A12;
end;
suppose
a <> DataLoc(u1.a,k1);
then u2.a = u1.a by FUNCT_4:83;
hence thesis by FUNCT_7:94;
end;
end;
A14: IC u2 = u1.IC SCMPDS by FUNCT_4:83,SCMPDS_2:43
.= IC u by FUNCT_4:83,SCMPDS_2:43
.= n by MEMSTR_0:def 11;
ex m1 being Element of NAT st m1 = IC u2 & ICplusConst(u2,k2) = |.
m1+k2.| by SCMPDS_2:def 18;
then x = IC Exec(i,u2) by A11,A14,A13,SCMPDS_2:57;
hence thesis by A14;
end;
end;
theorem Th17:
JUMP (return a) = {k where k is Nat: k > 1}
proof
set A = {k where k is Nat: k > 1};
set i = return a;
set X = the set of all NIC(i,l) where l is Nat;
JUMP i c= NIC(i,(0)) by AMISTD_1:19;
hence JUMP i c= A by Th4;
let x be object;
assume
A1: x in A;
now
consider k being Nat such that
A2: x = k and
A3: k > 1 by A1;
reconsider k2 = k-2 as Element of NAT by A3,Lm2;
NIC(i,(0)) in X;
hence X <> {};
a in SCM-Data-Loc by AMI_2:def 16;
then consider j being Nat such that
A4: a = [1,j] by AMI_2:23;
set t = [1,j+1];
set s = the State of SCMPDS;
let y be set;
A5: DataLoc(j,1) = [1,|.j+1.|]
.= t by ABSVALUE:def 1;
t in SCM-Data-Loc by AMI_2:24;
then reconsider t1 = t as Int_position by AMI_2:def 16;
assume y in X;
then consider l being Nat such that
A6: y = NIC(i,l);
reconsider n = l as Element of NAT by ORDINAL1:def 12;
set I = i;
reconsider u = the n-started State of SCMPDS
as Element of product the_Values_of SCMPDS by CARD_3:107;
A7: IC u = n by MEMSTR_0:def 11;
set g = (a,t1)-->(j,k2);
reconsider v = u +* g
as Element of product the_Values_of SCMPDS by CARD_3:107;
j <> j+1;
then
A8: a <> t1 by A4,XTUPLE_0:1;
then
A9: v.a = j by FUNCT_4:84;
A10: v.t1 = k2 by A8,FUNCT_4:84;
A11: dom g = {a,t1} by FUNCT_4:62;
a <> IC SCMPDS & t1 <> IC SCMPDS by SCMPDS_2:43;
then
A12: not IC SCMPDS in dom g by A11,TARSKI:def 2;
A13: IC v = l by A7,A12,FUNCT_4:11;
x = ((k2 ) + 2) by A2
.= (|.v.DataLoc(j,1).| ) + 2 by A10,A5,ABSVALUE:def 1
.= IC Exec(i,v) by A9,SCMPDS_2:58,SCMPDS_I:def 14;
hence x in y by A6,A13;
end;
hence thesis by SETFAM_1:def 1;
end;
registration
let a;
cluster JUMP (return a) -> infinite;
coherence
proof
{k where k is Nat: k > 1} is infinite by PRE_CIRC:23;
hence thesis by Th17;
end;
end;
registration
let a,k1;
cluster JUMP (saveIC(a,k1)) -> empty;
coherence
proof
for l being Element of NAT holds NIC(saveIC(a,k1),l)={
l+1} by Th5;
hence thesis by Th2;
end;
end;
registration
let a,k1;
cluster JUMP (a:=k1) -> empty;
coherence
proof
for l being Element of NAT holds NIC(a:=k1,l)={l+1}
by Th6;
hence thesis by Th2;
end;
end;
registration
let a,k1,k2;
cluster JUMP ((a,k1):=k2) -> empty;
coherence
proof
for l being Element of NAT holds NIC((a,k1):=k2,l)={
l+1 } by Th7;
hence thesis by Th2;
end;
end;
registration
let a,b,k1,k2;
cluster JUMP ((a,k1):=(b,k2)) -> empty;
coherence
proof
for l being Element of NAT holds NIC((a,k1):=(b,k2),l)
={l+1} by Th8;
hence thesis by Th2;
end;
end;
registration
let a,k1,k2;
cluster JUMP (AddTo(a,k1,k2)) -> empty;
coherence
proof
for l being Element of NAT holds NIC(AddTo(a,k1,k2),l)
={l+1} by Th9;
hence thesis by Th2;
end;
end;
registration
let a,b,k1,k2;
cluster JUMP (AddTo(a,k1,b,k2)) -> empty;
coherence
proof
for l being Element of NAT holds NIC(AddTo(a,k1,b,k2),
l)={l+1} by Th10;
hence thesis by Th2;
end;
cluster JUMP (SubFrom(a,k1,b,k2)) -> empty;
coherence
proof
for l being Element of NAT holds NIC(SubFrom(a,k1,b,k2
),l)={l+1} by Th11;
hence thesis by Th2;
end;
cluster JUMP (MultBy(a,k1,b,k2)) -> empty;
coherence
proof
for l being Element of NAT holds NIC(MultBy(a,k1,b,k2)
,l)={l+1} by Th12;
hence thesis by Th2;
end;
cluster JUMP (Divide(a,k1,b,k2)) -> empty;
coherence
proof
for l being Element of NAT holds NIC(Divide(a,k1,b,k2)
,l)={l+1} by Th13;
hence thesis by Th2;
end;
end;
Lm3: 5/3 is not integer
proof
not 3 qua Integer divides 5
proof
assume not thesis;
then
A1: 5 mod 3 = 0 by PEPIN:6;
5 = 3 * 1 + 2;
hence contradiction by A1,NAT_D:def 2;
end;
hence thesis by WSIERP_1:17;
end;
Lm4: for d being Real holds (|.d.|+(-d+|.d.|+4))+2-2+d <> -((|.d.|+(
-d+|.d.|+4)+(-d+|.d.|+4))+2-2+d)
proof
let d be Real;
set c = -d+|.d.|+4;
set xx = c+c+c;
-d+|.d.| >= 0 by ABSVALUE:27;
then (-2)*xx < (-2)*0 by XREAL_1:69;
then
A1: (-2)*xx/4 < 0/4 by XREAL_1:74;
assume (|.d.|+c)+2-2+d = -((|.d.|+c+(-d+|.d.|+4))+2-2+d);
then d + |.d.| = (-2)*xx/4;
hence contradiction by A1,ABSVALUE:26;
end;
Lm5: for b,d being Real holds b+1 <> b + ((-d+|.d.|+4) + d)
proof
let b,d be Real;
set c = -d+|.d.|+4;
|.d.| >= 0 by COMPLEX1:46;
then
A1: |.d.|+3 >= 0+3 by XREAL_1:7;
assume b+1 = b + (c + d);
hence thesis by A1;
end;
Lm6: for c,d being Real st c > 0 holds (|.d.|+c)+1 <> -((|.d.|+c)+c+d
)
proof
let c,d being Real such that
A1: c > 0;
assume
A2: (|.d.|+c)+1 = -((|.d.|+c)+c+d);
per cases;
suppose
A3: d >= 0;
then |.d.| = d by ABSVALUE:def 1;
hence contradiction by A1,A2,A3;
end;
suppose
A4: d < 0;
then |.d.| = -d by ABSVALUE:def 1;
then (-d+3*c)+1 = 0 by A2;
hence contradiction by A1,A4;
end;
end;
Lm7: for b being Real, d being Integer st d <> 5 holds (b+(-d+|.d.|+4)
+1) <> (b+d)
proof
let b be Real, d be Integer;
assume
A1: d <> 5;
assume
A2: (b+(-d+|.d.|+4)+1) = (b+d);
per cases;
suppose
d >= 0;
then |.d.| = d by ABSVALUE:def 1;
hence thesis by A1,A2;
end;
suppose
d < 0;
then |.d.| = -d by ABSVALUE:def 1;
hence thesis by A2,Lm3;
end;
end;
Lm8: for c,d being Real st c > 0 holds (|.d.|+c+c)+1 <> -((|.d.|+c)+d
)
proof
let c,d be Real;
assume
A1: c > 0;
assume
A2: (|.d.|+c+c)+1 = -((|.d.|+c)+d);
per cases;
suppose
A3: d >= 0;
then |.d.| = d by ABSVALUE:def 1;
hence contradiction by A1,A2,A3;
end;
suppose
A4: d < 0;
then |.d.| = -d by ABSVALUE:def 1;
hence contradiction by A1,A2,A4;
end;
end;
Lm9: JUMP ((a,k1)<>0_goto 5) = {}
proof
set k2 = 5;
set i = (a,k1)<>0_goto k2;
set X = the set of all NIC(i,l) where l is Nat;
hereby
set nl2 = 8;
set nl1 = 5;
let x be object;
assume
A1: x in JUMP i;
set l2 = nl2;
NIC(i,l2) in X;
then x in NIC(i,l2) by A1,SETFAM_1:def 1;
then consider s2 being Element of product the_Values_of SCMPDS
such that
A2: x = IC Exec(i,s2) and
A3: IC s2 = l2;
set l1 = nl1;
NIC(i,l1) in X;
then x in NIC(i,l1) by A1,SETFAM_1:def 1;
then consider s1 being Element of product the_Values_of SCMPDS
such that
A4: x = IC Exec(i,s1) and
A5: IC s1 = l1;
consider m2 being Element of NAT such that
A6: m2 = IC s2 and
A7: ICplusConst(s2,k2) = |.m2+k2.| by SCMPDS_2:def 18;
consider m1 being Element of NAT such that
A8: m1 = IC s1 and
A9: ICplusConst(s1,k2) = |.m1+k2.| by SCMPDS_2:def 18;
per cases;
suppose that
A10: s1.DataLoc(s1.a,k1) <> 0 and
A11: s2.DataLoc(s2.a,k1) <> 0;
A12: x = |.m2+k2.| by A2,A7,A11,SCMPDS_2:55;
x = |.m1+k2.| by A4,A9,A10,SCMPDS_2:55;
then nl1+k2 = nl2+k2 or nl1+k2 = -(nl2+k2) by A5,A8,A3,A6,A12,ABSVALUE:28
;
hence x in {};
end;
suppose that
A13: s1.DataLoc(s1.a,k1) = 0 and
A14: s2.DataLoc(s2.a,k1) = 0;
A15: x = l2+1 by A2,A3,A14,SCMPDS_2:55;
x = l1+1 by A4,A5,A13,SCMPDS_2:55;
hence x in {} by A15;
end;
suppose that
A16: s1.DataLoc(s1.a,k1) = 0 and
A17: s2.DataLoc(s2.a,k1) <> 0;
reconsider n1 = l1 as Element of NAT;
set w1 = n1;
A18: x = |.m2+k2.| by A2,A7,A17,SCMPDS_2:55;
x = n1+1 by A4,A5,A16,SCMPDS_2:55
.= n1 + 1;
then w1+1 = m2+k2 or w1+1 = -(m2+k2) by A18,ABSVALUE:1;
hence x in {} by A3,A6;
end;
suppose that
A19: s1.DataLoc(s1.a,k1) <> 0 and
A20: s2.DataLoc(s2.a,k1) = 0;
reconsider n2 = l2 as Element of NAT;
A21: x = n2+1 by A2,A3,A20,SCMPDS_2:55
.= n2 + 1;
set w2 = n2;
x = |.m1+k2.| by A4,A9,A19,SCMPDS_2:55;
then w2+1 = m1+k2 or w2+1 = -(m1+k2) by A21,ABSVALUE:1;
hence x in {} by A5,A8;
end;
end;
thus thesis;
end;
Lm10: k2 <> 5 implies JUMP ((a,k1)<>0_goto k2) = {}
proof
set i = (a,k1)<>0_goto k2;
set X = the set of all NIC(i,l) where l is Nat;
assume
A1: k2 <> 5;
hereby
set x1 = -k2+|.k2.|+4;
let x be object;
assume
A2: x in JUMP i;
A3: x1 > -k2+|.k2.|+0 by XREAL_1:6;
then
A4: x1 > 0 by ABSVALUE:27;
then reconsider x1 as Element of NAT by INT_1:3;
set nl1 = |.k2.|+x1;
set nl2 = nl1+x1;
set l1 = nl1;
set l2 = nl2;
NIC(i,l1) in X;
then x in NIC(i,l1) by A2,SETFAM_1:def 1;
then consider s1 being Element of product the_Values_of SCMPDS
such that
A5: x = IC Exec(i,s1) and
A6: IC s1 = l1;
consider m1 being Element of NAT such that
A7: m1 = IC s1 and
A8: ICplusConst(s1,k2) = |.m1+k2.| by SCMPDS_2:def 18;
NIC(i,l2) in X;
then x in NIC(i,l2) by A2,SETFAM_1:def 1;
then consider s2 being Element of product the_Values_of SCMPDS
such that
A9: x = IC Exec(i,s2) and
A10: IC s2 = l2;
consider m2 being Element of NAT such that
A11: m2 = IC s2 and
A12: ICplusConst(s2,k2) = |.m2+k2.| by SCMPDS_2:def 18;
per cases;
suppose that
A13: s1.DataLoc(s1.a,k1) <> 0 and
A14: s2.DataLoc(s2.a,k1) <> 0;
A15: x = |.m2+k2.| by A9,A12,A14,SCMPDS_2:55;
A16: x = |.m1+k2.| by A5,A8,A13,SCMPDS_2:55;
thus x in {}
proof
per cases by A6,A7,A10,A11,A16,A15,ABSVALUE:28;
suppose
nl1+2-2+k2 = nl2+2-2+k2;
hence thesis by A3,ABSVALUE:27;
end;
suppose
nl1+2-2+k2 = -(nl2+2-2+k2);
hence thesis by Lm4;
end;
end;
end;
suppose that
A17: s1.DataLoc(s1.a,k1) = 0 and
A18: s2.DataLoc(s2.a,k1) = 0;
A19: x = l2+1 by A9,A10,A18,SCMPDS_2:55;
x = l1+1 by A5,A6,A17,SCMPDS_2:55;
hence x in {} by A3,A19,ABSVALUE:27;
end;
suppose that
A20: s1.DataLoc(s1.a,k1) = 0 and
A21: s2.DataLoc(s2.a,k1) <> 0;
reconsider n1 = l1 as Element of NAT;
set w1 = n1;
A22: x = |.m2+k2.| by A9,A12,A21,SCMPDS_2:55;
A23: x = n1+1 by A5,A6,A20,SCMPDS_2:55
.= n1 + 1;
thus x in {}
proof
per cases by A23,A22,ABSVALUE:1;
suppose
w1+1 = m2+k2;
then nl1+1 = nl1 + (x1 + k2) by A10,A11;
hence thesis by Lm5;
end;
suppose
w1+1 = -(m2+k2);
hence thesis by A4,A10,A11,Lm6;
end;
end;
end;
suppose that
A24: s1.DataLoc(s1.a,k1) <> 0 and
A25: s2.DataLoc(s2.a,k1) = 0;
reconsider n2 = l2 as Element of NAT;
A26: x = n2+1 by A9,A10,A25,SCMPDS_2:55
.= n2 + 1;
set w2 = n2;
A27: x = |.m1+k2.| by A5,A8,A24,SCMPDS_2:55;
thus x in {}
proof
per cases by A27,A26,ABSVALUE:1;
suppose
w2+1 = m1+k2;
hence thesis by A1,A6,A7,Lm7;
end;
suppose
w2+1 = -(m1+k2);
hence thesis by A4,A6,A7,Lm8;
end;
end;
end;
end;
thus thesis;
end;
Lm11: JUMP ((a,k1)<=0_goto 5) = {}
proof
set k2 = 5;
set i = (a,k1)<=0_goto k2;
set X = the set of all NIC(i,l) where l is Nat;
hereby
set nl2 = 8;
set nl1 = 5;
let x be object;
assume
A1: x in JUMP i;
set l2 = nl2;
NIC(i,l2) in X;
then x in NIC(i,l2) by A1,SETFAM_1:def 1;
then consider s2 being Element of product the_Values_of SCMPDS
such that
A2: x = IC Exec(i,s2) and
A3: IC s2 = l2;
set l1 = nl1;
NIC(i,l1) in X;
then x in NIC(i,l1) by A1,SETFAM_1:def 1;
then consider s1 being Element of product the_Values_of SCMPDS
such that
A4: x = IC Exec(i,s1) and
A5: IC s1 = l1;
consider m2 being Element of NAT such that
A6: m2 = IC s2 and
A7: ICplusConst(s2,k2) = |.m2+k2.| by SCMPDS_2:def 18;
consider m1 being Element of NAT such that
A8: m1 = IC s1 and
A9: ICplusConst(s1,k2) = |.m1+k2.| by SCMPDS_2:def 18;
per cases;
suppose that
A10: s1.DataLoc(s1.a,k1) <= 0 and
A11: s2.DataLoc(s2.a,k1) <= 0;
A12: x = |.m2+k2.| by A2,A7,A11,SCMPDS_2:56;
x = |.m1+k2.| by A4,A9,A10,SCMPDS_2:56;
then nl1+k2 = nl2+k2 or nl1+k2 = -(nl2+k2) by A5,A8,A3,A6,A12,ABSVALUE:28
;
hence x in {};
end;
suppose that
A13: s1.DataLoc(s1.a,k1) > 0 and
A14: s2.DataLoc(s2.a,k1) > 0;
A15: x = l2+1 by A2,A3,A14,SCMPDS_2:56;
x = l1+1 by A4,A5,A13,SCMPDS_2:56;
hence x in {} by A15;
end;
suppose that
A16: s1.DataLoc(s1.a,k1) > 0 and
A17: s2.DataLoc(s2.a,k1) <= 0;
reconsider n1 = l1 as Element of NAT;
set w1 = n1;
A18: x = |.m2+k2.| by A2,A7,A17,SCMPDS_2:56;
x = n1+1 by A4,A5,A16,SCMPDS_2:56
.= n1 + 1;
then w1+1 = m2+k2 or w1+1 = -(m2+k2) by A18,ABSVALUE:1;
hence x in {} by A3,A6;
end;
suppose that
A19: s1.DataLoc(s1.a,k1) <= 0 and
A20: s2.DataLoc(s2.a,k1) > 0;
reconsider n2 = l2 as Element of NAT;
A21: x = n2+1 by A2,A3,A20,SCMPDS_2:56
.= n2 + 1;
set w2 = n2;
x = |.m1+k2.| by A4,A9,A19,SCMPDS_2:56;
then w2+1 = m1+k2 or w2+1 = -(m1+k2) by A21,ABSVALUE:1;
hence x in {} by A5,A8;
end;
end;
thus thesis;
end;
Lm12: k2 <> 5 implies JUMP ((a,k1)<=0_goto k2) = {}
proof
set i = (a,k1)<=0_goto k2;
set X = the set of all NIC(i,l) where l is Nat;
assume
A1: k2 <> 5;
hereby
set x1 = -k2+|.k2.|+4;
let x be object;
assume
A2: x in JUMP i;
A3: x1 > -k2+|.k2.|+0 by XREAL_1:6;
then
A4: x1 > 0 by ABSVALUE:27;
then reconsider x1 as Element of NAT by INT_1:3;
set nl1 = |.k2.|+x1;
set nl2 = nl1+x1;
set l1 = nl1;
set l2 = nl2;
NIC(i,l1) in X;
then x in NIC(i,l1) by A2,SETFAM_1:def 1;
then consider s1 being Element of product the_Values_of SCMPDS
such that
A5: x = IC Exec(i,s1) and
A6: IC s1 = l1;
consider m1 being Element of NAT such that
A7: m1 = IC s1 and
A8: ICplusConst(s1,k2) = |.m1+k2.| by SCMPDS_2:def 18;
NIC(i,l2) in X;
then x in NIC(i,l2) by A2,SETFAM_1:def 1;
then consider s2 being Element of product the_Values_of SCMPDS
such that
A9: x = IC Exec(i,s2) and
A10: IC s2 = l2;
consider m2 being Element of NAT such that
A11: m2 = IC s2 and
A12: ICplusConst(s2,k2) = |.m2+k2.| by SCMPDS_2:def 18;
per cases;
suppose that
A13: s1.DataLoc(s1.a,k1) <= 0 and
A14: s2.DataLoc(s2.a,k1) <= 0;
A15: x = |.m2+k2.| by A9,A12,A14,SCMPDS_2:56;
A16: x = |.m1+k2.| by A5,A8,A13,SCMPDS_2:56;
thus x in {}
proof
per cases by A6,A7,A10,A11,A16,A15,ABSVALUE:28;
suppose
nl1+k2 = nl2+k2;
hence thesis by A3,ABSVALUE:27;
end;
suppose
nl1+2-2+k2 = -(nl2+2-2+k2);
hence thesis by Lm4;
end;
end;
end;
suppose that
A17: s1.DataLoc(s1.a,k1) > 0 and
A18: s2.DataLoc(s2.a,k1) > 0;
A19: x = l2+1 by A9,A10,A18,SCMPDS_2:56;
x = l1+1 by A5,A6,A17,SCMPDS_2:56;
hence x in {} by A3,A19,ABSVALUE:27;
end;
suppose that
A20: s1.DataLoc(s1.a,k1) > 0 and
A21: s2.DataLoc(s2.a,k1) <= 0;
reconsider n1 = l1 as Element of NAT;
set w1 = n1;
A22: x = |.m2+k2.| by A9,A12,A21,SCMPDS_2:56;
A23: x = n1+1 by A5,A6,A20,SCMPDS_2:56
.= n1 + 1;
thus x in {}
proof
per cases by A23,A22,ABSVALUE:1;
suppose
w1+1 = m2+k2;
then nl1+1 = nl1 + (x1 + k2) by A10,A11;
hence thesis by Lm5;
end;
suppose
w1+1 = -(m2+k2);
hence thesis by A4,A10,A11,Lm6;
end;
end;
end;
suppose that
A24: s1.DataLoc(s1.a,k1) <= 0 and
A25: s2.DataLoc(s2.a,k1) > 0;
reconsider n2 = l2 as Element of NAT;
A26: x = n2+1 by A9,A10,A25,SCMPDS_2:56
.= n2 + 1;
set w2 = n2;
A27: x = |.m1+k2.| by A5,A8,A24,SCMPDS_2:56;
thus x in {}
proof
per cases by A27,A26,ABSVALUE:1;
suppose
w2+1 = m1+k2;
hence thesis by A1,A6,A7,Lm7;
end;
suppose
w2+1 = -(m1+k2);
hence thesis by A4,A6,A7,Lm8;
end;
end;
end;
end;
thus thesis;
end;
Lm13: JUMP ((a,k1)>=0_goto 5) = {}
proof
set k2 = 5;
set i = (a,k1)>=0_goto k2;
set X = the set of all NIC(i,l) where l is Nat;
hereby
set nl2 = 8;
set nl1 = 5;
let x be object;
assume
A1: x in JUMP i;
set l2 = nl2;
NIC(i,l2) in X;
then x in NIC(i,l2) by A1,SETFAM_1:def 1;
then consider s2 being Element of product the_Values_of SCMPDS
such that
A2: x = IC Exec(i,s2) and
A3: IC s2 = l2;
set l1 = nl1;
NIC(i,l1) in X;
then x in NIC(i,l1) by A1,SETFAM_1:def 1;
then consider s1 being Element of product the_Values_of SCMPDS
such that
A4: x = IC Exec(i,s1) and
A5: IC s1 = l1;
consider m2 being Element of NAT such that
A6: m2 = IC s2 and
A7: ICplusConst(s2,k2) = |.m2+k2.| by SCMPDS_2:def 18;
consider m1 being Element of NAT such that
A8: m1 = IC s1 and
A9: ICplusConst(s1,k2) = |.m1+k2.| by SCMPDS_2:def 18;
per cases;
suppose that
A10: s1.DataLoc(s1.a,k1) >= 0 and
A11: s2.DataLoc(s2.a,k1) >= 0;
A12: x = |.m2+k2.| by A2,A7,A11,SCMPDS_2:57;
x = |.m1+k2.| by A4,A9,A10,SCMPDS_2:57;
then
nl1+2-2+k2 = nl2+2-2+k2 or nl1+2-2+k2 = -(nl2+2-2+k2) by A5,A8,A3,A6,A12,
ABSVALUE:28;
hence x in {};
end;
suppose that
A13: s1.DataLoc(s1.a,k1) < 0 and
A14: s2.DataLoc(s2.a,k1) < 0;
A15: x = l2+1 by A2,A3,A14,SCMPDS_2:57;
x = l1+1 by A4,A5,A13,SCMPDS_2:57;
hence x in {} by A15;
end;
suppose that
A16: s1.DataLoc(s1.a,k1) < 0 and
A17: s2.DataLoc(s2.a,k1) >= 0;
reconsider n1 = l1 as Element of NAT;
set w1 = n1;
A18: x = |.m2+k2.| by A2,A7,A17,SCMPDS_2:57;
x = n1+1 by A4,A5,A16,SCMPDS_2:57
.= n1 + 1;
then w1+1 = m2+k2 or w1+1 = -(m2+k2) by A18,ABSVALUE:1;
hence x in {} by A3,A6;
end;
suppose that
A19: s1.DataLoc(s1.a,k1) >= 0 and
A20: s2.DataLoc(s2.a,k1) < 0;
reconsider n2 = l2 as Element of NAT;
A21: x = n2+1 by A2,A3,A20,SCMPDS_2:57
.= n2 + 1;
set w2 = n2;
x = |.m1+k2.| by A4,A9,A19,SCMPDS_2:57;
then w2+1 = m1+k2 or w2+1 = -(m1+k2) by A21,ABSVALUE:1;
hence x in {} by A5,A8;
end;
end;
thus thesis;
end;
Lm14: k2 <> 5 implies JUMP ((a,k1)>=0_goto k2) = {}
proof
set i = (a,k1)>=0_goto k2;
set X = the set of all NIC(i,l) where l is Nat;
assume
A1: k2 <> 5;
hereby
set x1 = -k2+|.k2.|+4;
let x be object;
assume
A2: x in JUMP i;
A3: x1 > -k2+|.k2.|+0 by XREAL_1:6;
then
A4: x1 > 0 by ABSVALUE:27;
then reconsider x1 as Element of NAT by INT_1:3;
set nl1 = |.k2.|+x1;
set nl2 = nl1+x1;
set l1 = nl1;
set l2 = nl2;
NIC(i,l1) in X;
then x in NIC(i,l1) by A2,SETFAM_1:def 1;
then consider s1 being Element of product the_Values_of SCMPDS
such that
A5: x = IC Exec(i,s1) and
A6: IC s1 = l1;
consider m1 being Element of NAT such that
A7: m1 = IC s1 and
A8: ICplusConst(s1,k2) = |.m1+k2.| by SCMPDS_2:def 18;
NIC(i,l2) in X;
then x in NIC(i,l2) by A2,SETFAM_1:def 1;
then consider s2 being Element of product the_Values_of SCMPDS
such that
A9: x = IC Exec(i,s2) and
A10: IC s2 = l2;
consider m2 being Element of NAT such that
A11: m2 = IC s2 and
A12: ICplusConst(s2,k2) = |.m2+k2.| by SCMPDS_2:def 18;
per cases;
suppose that
A13: s1.DataLoc(s1.a,k1) >= 0 and
A14: s2.DataLoc(s2.a,k1) >= 0;
A15: x = |.m2+k2.| by A9,A12,A14,SCMPDS_2:57;
A16: x = |.m1+k2.| by A5,A8,A13,SCMPDS_2:57;
thus x in {}
proof
per cases by A6,A7,A10,A11,A16,A15,ABSVALUE:28;
suppose
nl1+2-2+k2 = nl2+2-2+k2;
hence thesis by A3,ABSVALUE:27;
end;
suppose
nl1+2-2+k2 = -(nl2+2-2+k2);
hence thesis by Lm4;
end;
end;
end;
suppose that
A17: s1.DataLoc(s1.a,k1) < 0 and
A18: s2.DataLoc(s2.a,k1) < 0;
A19: x = l2+1 by A9,A10,A18,SCMPDS_2:57;
x = l1+1 by A5,A6,A17,SCMPDS_2:57;
hence x in {} by A3,A19,ABSVALUE:27;
end;
suppose that
A20: s1.DataLoc(s1.a,k1) < 0 and
A21: s2.DataLoc(s2.a,k1) >= 0;
reconsider n1 = l1 as Element of NAT;
set w1 = n1;
A22: x = |.m2+k2.| by A9,A12,A21,SCMPDS_2:57;
A23: x = n1+1 by A5,A6,A20,SCMPDS_2:57
.= n1 + 1;
thus x in {}
proof
per cases by A23,A22,ABSVALUE:1;
suppose
w1+1 = m2+k2;
then nl1+1 = nl1 + (x1 + k2) by A10,A11;
hence thesis by Lm5;
end;
suppose
w1+1 = -(m2+k2);
hence thesis by A4,A10,A11,Lm6;
end;
end;
end;
suppose that
A24: s1.DataLoc(s1.a,k1) >= 0 and
A25: s2.DataLoc(s2.a,k1) < 0;
reconsider n2 = l2 as Element of NAT;
A26: x = n2+1 by A9,A10,A25,SCMPDS_2:57
.= n2 + 1;
set w2 = n2;
A27: x = |.m1+k2.| by A5,A8,A24,SCMPDS_2:57;
thus x in {}
proof
per cases by A27,A26,ABSVALUE:1;
suppose
w2+1 = m1+k2;
hence thesis by A1,A6,A7,Lm7;
end;
suppose
w2+1 = -(m1+k2);
hence thesis by A4,A6,A7,Lm8;
end;
end;
end;
end;
thus thesis;
end;
registration
let a,k1,k2;
cluster JUMP ((a,k1)<>0_goto k2) -> empty;
coherence
proof
k2 = 5 or k2 <> 5;
hence thesis by Lm9,Lm10;
end;
cluster JUMP ((a,k1)<=0_goto k2) -> empty;
coherence
proof
k2 = 5 or k2 <> 5;
hence thesis by Lm11,Lm12;
end;
cluster JUMP ((a,k1)>=0_goto k2) -> empty;
coherence
proof
k2 = 5 or k2 <> 5;
hence thesis by Lm13,Lm14;
end;
end;
theorem Th18:
SUCC(l,SCMPDS) = NAT
proof
thus SUCC(l,SCMPDS) c= NAT;
let x be object;
set X = the set of all
NIC(i,l) \ JUMP i where i is Element of the InstructionsF of SCMPDS;
assume x in NAT;
then reconsider x as Element of NAT;
reconsider xx=x as Element of NAT;
set i = goto ( xx - l);
NIC(i,l) = { |. xx - l + l.| } by Th3
.= {x} by ABSVALUE:def 1;
then
A1: x in NIC(i,l) \ JUMP i by TARSKI:def 1;
NIC(i,l) \ JUMP i in X;
hence thesis by A1,TARSKI:def 4;
end;
registration
cluster SCMPDS -> non InsLoc-antisymmetric;
coherence
proof
SUCC( 2,SCMPDS) = NAT by Th18;
then
A1: (2) <= (1), SCMPDS by AMI_WSTD:33;
SUCC( 1,SCMPDS) = NAT by Th18;
then
A2: (1) <= (2), SCMPDS by AMI_WSTD:33;
assume SCMPDS is InsLoc-antisymmetric;
hence thesis by A2,A1,AMI_WSTD:def 2;
end;
end;
registration
cluster SCMPDS -> non weakly_standard;
coherence by AMI_WSTD:10;
end;