:: Weakly Standard Ordering of Instruction Locations
:: by Andrzej Trybulec , Piotr Rudnicki and Artur Korni{\l}owicz
::
:: Received April 22, 2010
:: Copyright (c) 2010-2019 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, XBOOLE_0, SUBSET_1, AMI_1, FSM_1, FUNCT_4, FUNCOP_1,
RELAT_1, TARSKI, FUNCT_1, CARD_3, ZFMISC_1, CIRCUIT2, NAT_1, GLIB_000,
XXREAL_0, PARTFUN1, FINSEQ_1, ARYTM_3, GRAPH_2, CARD_1, FUNCT_2,
FINSEQ_4, ARYTM_1, FINSET_1, FRECHET, WAYBEL_0, MEMBERED, AMISTD_1,
EXTPRO_1, AMI_WSTD, STRUCT_0, COMPOS_1, QUANTAL1, GOBRD13, MEMSTR_0,
FUNCT_7, ORDINAL1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, ORDINAL1,
CARD_1, XXREAL_0, NUMBERS, XCMPLX_0, NAT_1, MEMBERED, FUNCT_1, RELSET_1,
PARTFUN1, DOMAIN_1, CARD_3, FINSEQ_1, FINSEQ_4, FUNCOP_1, FINSET_1,
FUNCT_4, FUNCT_7, MEASURE6, STRUCT_0, GRAPH_2, NAT_D, XXREAL_2, MEMSTR_0,
COMPOS_0, FINSEQ_6, COMPOS_1, EXTPRO_1, FUNCT_2, AMISTD_1;
constructors WELLORD2, REAL_1, FINSEQ_4, REALSET1, NAT_D, XXREAL_2, RELSET_1,
PRE_POLY, GRAPH_2, AMISTD_1, FUNCT_7, FUNCT_4, PBOOLE,
FINSEQ_6, XTUPLE_0;
registrations RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1,
XREAL_0, NAT_1, MEMBERED, FINSEQ_1, CARD_3, FUNCT_7, JORDAN1J, CARD_1,
XXREAL_2, RELSET_1, FUNCT_4, AMISTD_1, EXTPRO_1, PRE_POLY, MEMSTR_0,
MEASURE6, COMPOS_0, XTUPLE_0, ORDINAL1, FINSEQ_6;
requirements NUMERALS, BOOLE, REAL, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, AMISTD_1;
equalities STRUCT_0, EXTPRO_1, XBOOLE_0, FUNCOP_1, NAT_1, AMISTD_1, MEMSTR_0,
CARD_1, ORDINAL1;
expansions XBOOLE_0;
theorems TARSKI, FINSEQ_4, FINSEQ_1, GRAPH_2, NAT_1, FUNCT_4, FUNCT_1,
FUNCT_2, ZFMISC_1, CARD_1, FUNCOP_1, ORDINAL1, GRFUNC_1, FINSEQ_3, INT_1,
REVROT_1, FUNCT_7, XBOOLE_0, MEMBERED, XREAL_1, XXREAL_0, FINSEQ_6,
PARTFUN1, XXREAL_2, XREAL_0, NAT_D, PBOOLE, AMISTD_1,
MEMSTR_0, CARD_3;
schemes NAT_1, FUNCT_7, FINSEQ_2, FRAENKEL, DOMAIN_1, FINSEQ_4;
begin :: Ami-Struct
reserve x for set,
D for non empty set,
k, n for Element of NAT,
z for Nat;
reserve N for with_zero set,
S for
IC-Ins-separated non empty with_non-empty_values AMI-Struct over N,
i for Element of the InstructionsF of S,
l, l1, l2, l3 for Element of NAT,
s for State of S;
reserve ss for Element of product the_Values_of S;
begin :: Ordering of Instruction Locations
definition
let N,S; let l1,l2 be Nat;
pred l1 <= l2, S means
ex f being non empty FinSequence of NAT st f/.1
= l1 & f/.len f = l2 & for n st 1 <= n & n < len f
holds f/.(n+1) in SUCC(f/.n,S);
end;
theorem
for N,S for l1,l2 being Nat holds
l1 <= l2,S & l2 <= l3, S implies l1 <= l3, S
proof let N,S; let l1,l2 be Nat;
given f1 being non empty FinSequence of NAT such that
A1: f1/.1 = l1 and
A2: f1/.len f1 = l2 and
A3: for n st 1 <= n & n < len f1 holds f1/.(n+1) in SUCC(f1/.n,S);
given f2 being non empty FinSequence of NAT such that
A4: f2/.1 = l2 and
A5: f2/.len f2 = l3 and
A6: for n st 1 <= n & n < len f2 holds f2/.(n+1) in SUCC(f2/.n,S);
take f1^'f2;
thus (f1^'f2)/.1 = l1 by A1,FINSEQ_6:155;
now
per cases;
suppose
f2 is trivial;
then
A7: ex x being Element of NAT st f2 = <*x*> by FINSEQ_6:107;
then f1^'f2 = f1 by FINSEQ_6:158;
hence (f1^'f2)/.len(f1^'f2) = l3 by A2,A4,A5,A7,FINSEQ_1:39;
end;
suppose
f2 is not trivial;
hence (f1^'f2)/.len(f1^'f2) = l3 by A5,FINSEQ_6:156;
end;
end;
hence (f1^'f2)/.len(f1^'f2) = l3;
let n such that
A8: 1 <= n and
A9: n < len(f1^'f2);
A10: len (f1^'f2) +1 = len f1 + len f2 by FINSEQ_6:139;
per cases by XXREAL_0:1;
suppose
A11: n < len f1;
then n+1 <= len f1 by NAT_1:13;
then
A12: (f1^'f2)/.(n+1) = f1/.(n+1) by FINSEQ_6:159,NAT_1:11;
(f1^'f2)/.n = f1/.n by A8,A11,FINSEQ_6:159;
hence thesis by A3,A8,A11,A12;
end;
suppose
A13: n = len f1;
then
A14: (f1^'f2)/.n = f2/.1 by A2,A4,A8,FINSEQ_6:159;
n+1 < len (f1^'f2) +1 by A9,XREAL_1:6;
then
A15: 1 < len f2 by A10,A13,XREAL_1:6;
then (f1^'f2)/.(n+1) = f2/.(1+1) by A13,FINSEQ_6:160;
hence thesis by A6,A14,A15;
end;
suppose
A16: n > len f1;
then consider m being Nat such that
A17: len f1 + m = n by NAT_1:10;
reconsider m as Element of NAT by ORDINAL1:def 12;
A18: len f1 + m > len f1 + 0 by A16,A17;
len f1 + m+1 < len f1 + len f2 by A9,A10,A17,XREAL_1:6;
then len f1 + (m+1) < len f1 + len f2;
then
A19: m+1 < len f2 by XREAL_1:6;
A20: (f1^'f2)/.(n+1) = (f1^'f2)/.(len f1 + (m+1)) by A17
.= f2/.(m+1+1) by A19,FINSEQ_6:160,NAT_1:11;
m <= m+1 by NAT_1:11;
then m < len f2 by A19,XXREAL_0:2;
then (f1^'f2)/.n = f2/.(m+1) by A17,A18,FINSEQ_6:160,NAT_1:14;
hence thesis by A6,A19,A20,NAT_1:11;
end;
end;
definition
let N, S;
attr S is InsLoc-antisymmetric means
for l1, l2 st l1 <= l2, S & l2 <= l1, S holds
l1 = l2;
end;
definition
let N, S;
attr S is weakly_standard means
:Def3:
ex f being sequence of NAT st f is
bijective & for m, n being Element of NAT holds m <= n iff f.m <= f.n, S;
end;
theorem Th2:
for f1, f2 being sequence of NAT st f1 is bijective & (for
m, n being Element of NAT holds m <= n iff f1.m <= f1.n,S) & f2 is bijective &
(for m, n being Element of NAT holds m <= n iff f2.m <= f2.n, S) holds f1 = f2
proof
let f1, f2 be sequence of NAT such that
A1: f1 is bijective and
A2: for m, n being Element of NAT holds m <= n iff f1.m <= f1.n,S and
A3: f2 is bijective and
A4: for m, n being Element of NAT holds m <= n iff f2.m <= f2.n,S;
A5: dom f1 = NAT by FUNCT_2:def 1;
A6: dom f2 = NAT by FUNCT_2:def 1;
defpred P[Nat] means f1.$1 <> f2.$1;
assume f1 <> f2;
then ex c being Element of NAT st P[c] by FUNCT_2:63;
then
A7: ex c being Nat st P[c];
consider d being Nat such that
A8: P[d] and
A9: for n being Nat st P[n] holds d <= n from NAT_1:sch 5(A7);
reconsider d as Element of NAT by ORDINAL1:def 12;
A10: rng f1 = NAT by A1,FUNCT_2:def 3;
A11: rng f2 = NAT by A3,FUNCT_2:def 3;
consider d1 being object such that
A12: d1 in dom f1 and
A13: f2.d = f1.d1 by A10,FUNCT_1:def 3;
reconsider d1 as Element of NAT by A12;
consider d2 being object such that
A14: d2 in dom f2 and
A15: f1.d = f2.d2 by A11,FUNCT_1:def 3;
reconsider d2 as Element of NAT by A14;
per cases;
suppose
A16: d1 <= d & d2 <= d;
then f2.d2 <= f2.d, S by A4;
then d <= d1 by A2,A15,A13;
hence contradiction by A8,A13,A16,XXREAL_0:1;
end;
suppose
A17: d <= d1 & d2 <= d;
f2.d2 = f1.d2
proof
assume not thesis;
then d <= d2 by A9;
hence contradiction by A8,A15,A17,XXREAL_0:1;
end;
hence contradiction by A1,A8,A15,A5,FUNCT_1:def 4;
end;
suppose
A18: d1 <= d & d <= d2;
f1.d1 = f2.d1
proof
assume not thesis;
then d <= d1 by A9;
hence contradiction by A8,A13,A18,XXREAL_0:1;
end;
hence contradiction by A3,A8,A13,A6,FUNCT_1:def 4;
end;
suppose
A19: d <= d1 & d <= d2;
then f2.d <= f2.d2,S by A4;
then d1 <= d by A2,A15,A13;
hence contradiction by A8,A13,A19,XXREAL_0:1;
end;
end;
Lm1: k <= k, S
proof
reconsider l=k as Element of NAT;
reconsider f = <*l*> as non empty FinSequence of NAT;
take f;
thus f/.1 = k by FINSEQ_4:16;
hence thesis by FINSEQ_1:39;
end;
theorem Th3:
for f being sequence of NAT st f is bijective holds
(for m, n being Element of NAT holds m <= n iff f.m <= f.n, S)
iff for k being Element of NAT holds f.(k+1) in SUCC(f.k,S) &
for j being Element of NAT st f.j in SUCC(f.k,S) holds k <= j
proof
let f be sequence of NAT;
assume
A1: f is bijective;
hereby
assume
A2: for m, n being Element of NAT holds m <= n iff f.m <= f.n, S;
let k be Element of NAT;
k <= k+1 by NAT_1:11;
then f.k <= f.(k+1), S by A2;
then consider F being non empty FinSequence of NAT such that
A3: F/.1 = f.k and
A4: F/.len F = f.(k+1) and
A5: for n st 1 <= n & n < len F holds F/.(n+1) in SUCC(F/.n,S);
set F1 = F -| f.(k+1);
set x = (f.(k+1))..F;
A6: f.(k+1) in rng F by A4,FINSEQ_6:168;
then
A7: len F1 = x-1 by FINSEQ_4:34;
then
A8: len F1+1 = x;
A9: x in dom F by A6,FINSEQ_4:20;
then
A10: F/.(len F1+1) = F.x by A7,PARTFUN1:def 6
.= f.(k+1) by A6,FINSEQ_4:19;
x <= len F by A9,FINSEQ_3:25;
then
A11: len F1 < len F by A8,NAT_1:13;
1 <= len F by NAT_1:14;
then
A12: 1 in dom F by FINSEQ_3:25;
then
A13: F/.1 = F.1 by PARTFUN1:def 6;
A14: F.x = f.(k+1) by A6,FINSEQ_4:19;
A15: dom f = NAT by FUNCT_2:def 1;
A16: f.k <> f.(k+1)
proof
assume not thesis;
then 0+k = k+1 by A1,A15,FUNCT_1:def 4;
hence contradiction;
end;
then
A17: len F1 <> 0 by A3,A14,A12,A7,PARTFUN1:def 6;
1 <= x by A9,FINSEQ_3:25;
then 1 < x by A3,A16,A14,A13,XXREAL_0:1;
then
A18: 1 <= len F1 by A8,NAT_1:13;
reconsider F1 as non empty FinSequence of NAT by A17,A6,FINSEQ_4:41;
rng f = NAT by A1,FUNCT_2:def 3;
then consider m being object such that
A19: m in dom f and
A20: f.m = F/.len F1 by FUNCT_1:def 3;
reconsider m as Element of NAT by A19;
A21: len F1 in dom F by A18,A11,FINSEQ_3:25;
A22: len F1 in dom F1 by A18,FINSEQ_3:25;
then
A23: F1/.len F1 = F1.len F1 by PARTFUN1:def 6
.= F.len F1 by A6,A22,FINSEQ_4:36
.= F/.len F1 by A21,PARTFUN1:def 6;
A24: now
(rng F1) misses {f.(k+1)} by A6,FINSEQ_4:38;
then rng F1 /\ {f.(k+1)} = {};
then
A25: not f.(k+1) in rng F1 or not f.(k+1) in {f.(k+1)} by XBOOLE_0:def 4;
assume
A26: m = k+1;
A27: len F1 in dom F1 by A18,FINSEQ_3:25;
then F1/.len F1 = F1.len F1 by PARTFUN1:def 6;
hence contradiction by A20,A23,A26,A25,A27,FUNCT_1:def 3,TARSKI:def 1;
end;
reconsider F2 = <*F/.len F1, F/.x*> as non empty FinSequence of NAT;
A28: len F2 = 2 by FINSEQ_1:44;
then
A29: 2 in dom F2 by FINSEQ_3:25;
then
A30: F2/.len F2 = F2.2 by A28,PARTFUN1:def 6
.= F/.x by FINSEQ_1:44
.= f.(k+1) by A14,A9,PARTFUN1:def 6;
A31: 1 in dom F2 by A28,FINSEQ_3:25;
A32: now
let n;
assume 1 <= n & n < len F2;
then n <> 0 & n < 1+1 by FINSEQ_1:44;
then n <> 0 & n <= 1 by NAT_1:13;
then
A33: n = 1 by NAT_1:25;
then
A34: F2/.n = F2.1 by A31,PARTFUN1:def 6
.= F/.len F1 by FINSEQ_1:44;
F2/.(n+1) = F2.2 by A29,A33,PARTFUN1:def 6
.= F/.(len F1+1) by A7,FINSEQ_1:44;
hence F2/.(n+1) in SUCC(F2/.n,S) by A5,A18,A11,A34;
end;
A35: now
let n;
assume that
A36: 1 <= n and
A37: n < len F1;
A38: 1 <= n+1 by A36,NAT_1:13;
A39: n+1 <= len F1 by A37,NAT_1:13;
then n+1 <= len F by A11,XXREAL_0:2;
then
A40: n+1 in dom F by A38,FINSEQ_3:25;
n <= len F by A11,A37,XXREAL_0:2;
then
A41: n in dom F by A36,FINSEQ_3:25;
A42: n in dom F1 by A36,A37,FINSEQ_3:25;
then
A43: F1/.n = F1.n by PARTFUN1:def 6
.= F.n by A6,A42,FINSEQ_4:36
.= F/.n by A41,PARTFUN1:def 6;
A44: n < len F by A11,A37,XXREAL_0:2;
A45: n+1 in dom F1 by A38,A39,FINSEQ_3:25;
then F1/.(n+1) = F1.(n+1) by PARTFUN1:def 6
.= F.(n+1) by A6,A45,FINSEQ_4:36
.= F/.(n+1) by A40,PARTFUN1:def 6;
hence F1/.(n+1) in SUCC(F1/.n,S) by A5,A36,A43,A44;
end;
F2/.1 = F2.1 by A31,PARTFUN1:def 6
.= f.m by A20,FINSEQ_1:44;
then f.m <= f.(k+1), S by A30,A32;
then
A46: m <= k+1 by A2;
A47: 1 in dom F1 by A18,FINSEQ_3:25;
then F1/.1 = F1.1 by PARTFUN1:def 6
.= F.1 by A6,A47,FINSEQ_4:36
.= f.k by A3,A12,PARTFUN1:def 6;
then f.k <= f.m, S by A20,A23,A35;
then k <= m by A2;
then m = k or m = k+1 by A46,NAT_1:9;
hence f.(k+1) in SUCC(f.k,S) by A5,A18,A11,A10,A20,A24;
let j be Element of NAT;
reconsider fk=f.k, fj=f.j as Element of NAT;
reconsider F = <*fk, fj*> as non empty FinSequence of NAT;
A48: len F = 2 by FINSEQ_1:44;
then
A49: 2 in dom F by FINSEQ_3:25;
A50: 1 in dom F by A48,FINSEQ_3:25;
then
A51: F/.1 = F.1 by PARTFUN1:def 6
.= f.k by FINSEQ_1:44;
assume
A52: f.j in SUCC(f.k,S);
A53: now
let n be Element of NAT;
assume 1 <= n & n < len F;
then n <> 0 & n < 1+1 by FINSEQ_1:44;
then n <> 0 & n <= 1 by NAT_1:13;
then
A54: n = 1 by NAT_1:25;
then
A55: F/.n = F.1 by A50,PARTFUN1:def 6
.= f.k by FINSEQ_1:44;
F/.(n+1) = F.2 by A49,A54,PARTFUN1:def 6
.= f.j by FINSEQ_1:44;
hence F/.(n+1) in SUCC(F/.n,S) by A52,A55;
end;
F/.len F = F.2 by A48,A49,PARTFUN1:def 6
.= f.j by FINSEQ_1:44;
then f.k <= f.j, S by A51,A53;
hence k <= j by A2;
end;
assume
A56: for k being Element of NAT holds f.(k+1) in SUCC(f.k,S) & for j
being Element of NAT st f.j in SUCC(f.k,S) holds k <= j;
let m, n be Element of NAT;
hereby
assume
A57: m <= n;
per cases by A57,XXREAL_0:1;
suppose
m = n;
hence f.m <= f.n, S by Lm1;
end;
suppose
A58: m < n;
thus f.m <= f.n, S
proof
reconsider f9=f as sequence of NAT;
set mn = n -' m;
deffunc F(Nat) = f9.(m+$1-'1);
consider F being FinSequence of NAT such that
A59: len F = mn+1 and
A60: for j being Nat st j in dom F holds F.j = F(j) from FINSEQ_2:
sch 1;
reconsider F as non empty FinSequence of NAT by A59;
take F;
A61: 1 <= mn+1 by NAT_1:11;
then
A62: 1 in dom F by A59,FINSEQ_3:25;
hence F/.1 = F.1 by PARTFUN1:def 6
.= f.(m+1-'1) by A60,A62
.= f.m by NAT_D:34;
m+1 <= n by A58,INT_1:7;
then 1 <= n-m by XREAL_1:19;
then 0 <= n-m;
then
A63: mn = n - m by XREAL_0:def 2;
A64: len F in dom F by A59,A61,FINSEQ_3:25;
hence F/.len F = F.len F by PARTFUN1:def 6
.= f.(m+(mn+1)-'1) by A59,A60,A64
.= f.(m+mn+1-'1)
.= f.n by A63,NAT_D:34;
let p be Element of NAT;
assume that
A65: 1 <= p and
A66: p < len F;
A67: p in dom F by A65,A66,FINSEQ_3:25;
then
A68: F/.p = F.p by PARTFUN1:def 6
.= f.(m+p-'1) by A60,A67;
A69: p <= m+p by NAT_1:11;
1 <= p+1 & p+1 <= len F by A65,A66,NAT_1:13;
then
A70: p+1 in dom F by FINSEQ_3:25;
then F/.(p+1) = F.(p+1) by PARTFUN1:def 6
.= f.(m+(p+1)-'1) by A60,A70
.= f.(m+p+1-'1)
.= f.(m+p-'1+1) by A65,A69,NAT_D:38,XXREAL_0:2;
hence thesis by A56,A68;
end;
end;
end;
assume f.m <= f.n, S;
then consider F being non empty FinSequence of NAT such that
A71: F/.1 = f.m and
A72: F/.len F = f.n and
A73: for n being Element of NAT st 1 <= n & n < len F holds F/.(n+1) in
SUCC(F/.n,S);
defpred P[Nat] means
1 <= $1 & $1 <= len F implies ex l being
Element of NAT st F/.$1 = f.l & m <= l;
A74: now
let k be Nat such that
A75: P[k];
now
assume that
1 <= k+1 and
A76: k+1 <= len F;
per cases;
suppose
k = 0;
hence ex l being Element of NAT st F/.(k+1) = f.l & m <= l by A71;
end;
suppose
A77: k > 0;
rng f = NAT by A1,FUNCT_2:def 3;
then consider l1 being object such that
A78: l1 in dom f and
A79: f.l1 = F/.(k+1) by FUNCT_1:def 3;
consider l being Element of NAT such that
A80: F/.k = f.l and
A81: m <= l by A75,A76,A77,NAT_1:13,14;
reconsider l1 as Element of NAT by A78;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
k < len F by A76,NAT_1:13;
then F/.(kk+1) in SUCC(F/.kk,S) by A73,A77,NAT_1:14;
then l <= l1 by A56,A80,A79;
hence
ex l being Element of NAT st F/.(k+1) = f.l & m <= l by A81,A79,
XXREAL_0:2;
end;
end;
hence P[k+1];
end;
A82: 1 <= len F by NAT_1:14;
A83: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A83, A74);
then dom f = NAT & ex l being Element of NAT st F/.len F = f.l & m <= l by
A82,FUNCT_2:def 1;
hence thesis by A1,A72,FUNCT_1:def 4;
end;
theorem Th4:
S is weakly_standard iff ex f being sequence of NAT st f is
bijective & for k being Element of NAT holds f.(k+1) in SUCC(f.k,S) & for j
being Element of NAT st f.j in SUCC(f.k,S) holds k <= j
proof
hereby
assume S is weakly_standard;
then consider f being sequence of NAT such that
A1: f is bijective and
A2: for m, n being Element of NAT holds m <= n iff f.m <= f.n, S;
thus ex f being sequence of NAT st f is bijective & for k being
Element of NAT holds f.(k+1) in SUCC(f.k,S) & for j being Element of NAT st f.j
in SUCC(f.k,S) holds k <= j
proof
take f;
thus f is bijective by A1;
thus thesis by A1,A2,Th3;
end;
end;
given f be sequence of NAT such that
A3: f is bijective and
A4: for k being Element of NAT holds f.(k+1) in SUCC(f.k,S) & for j being
Element of NAT st f.j in SUCC(f.k,S) holds k <= j;
take f;
thus f is bijective by A3;
thus thesis by A3,A4,Th3;
end;
set III = {[1,0,0],[0,0,0]};
begin :: Standard trivial computer
Lm2: for i being Instruction of STC N, s being State of STC N st InsCode i = 1
holds IC Exec(i,s) = IC s + 1
proof
let i be Instruction of STC N, s be State of STC N;
set M = STC N;
assume
A1: InsCode i = 1;
A2: now
assume i in {[0,0,0]};
then i = [0,0,0] by TARSKI:def 1;
hence contradiction by A1;
end;
the InstructionsF of M = III by AMISTD_1:def 7;
then i = [1,0,0] or i = [0,0,0] by TARSKI:def 2;
then
A3: i in {[1,0,0]} by A1,TARSKI:def 1;
A4: 0 in {0} by TARSKI:def 1;
then
A5: 0 in dom (0 .-->(In(s.0,NAT)+1));
consider f be Function of product the_Values_of M, product
the_Values_of M such that
A6: for s being Element of product the_Values_of M holds f.s = s+*(
0 .--> (In(s.0,NAT)+1)) and
A7: the Execution of M = ([1,0,0] .--> f) +* ([0,0,0] .--> id product
the_Values_of M) by AMISTD_1:def 7;
A8: for s being State of M holds f.s = s+*(0 .-->(In(s.0,NAT)+1))
proof let s be State of M;
reconsider s as Element of product the_Values_of M by CARD_3:107;
f.s = s+*(0 .-->(In(s.0,NAT)+1)) by A6;
hence thesis;
end;
A9: IC M = 0 by AMISTD_1:def 7;
A10: s in product the_Values_of M by CARD_3:107;
dom(the_Values_of M) = the carrier of M by PARTFUN1:def 2
.= {0} by AMISTD_1:def 7;
then
A11: 0 in dom(the_Values_of M) by TARSKI:def 1;
Values IC M = NAT by MEMSTR_0:def 6;
then reconsider k = s.0 as Element of NAT by A10,A11,CARD_3:9,A9;
dom ([0,0,0] .--> id product the_Values_of M) = {[0,0,0]};
then (the Execution of M).i = ([1,0,0] .--> f).i by A7,A2,FUNCT_4:11
.= f by A3,FUNCOP_1:7;
hence IC Exec(i,s) = (s+*(0 .-->(In(s.0,NAT)+1))).0 by A9,A8
.= (0 .-->(In(k,NAT)+1)).0 by A5,FUNCT_4:13
.= IC s + 1 by A9,A4,FUNCOP_1:7;
end;
Lm3: for l being Element of NAT, i being Element of the
InstructionsF of STC N st l = z & InsCode i = 1 holds NIC(i, l) = {z+1}
proof
let l be Element of NAT, i be Element of the InstructionsF of STC N;
assume that
A1: l = z and
A2: InsCode i = 1;
set M = STC N;
set F = { IC Exec(i,ss)
where ss is Element of product the_Values_of STC N:
IC ss = l };
now
reconsider f = NAT --> i
as Instruction-Sequence of M;
reconsider l9 = l as Element of Values IC M by MEMSTR_0:def 6;
reconsider w = the l-started State of M
as Element of product the_Values_of M by CARD_3:107;
set u = (IC M).-->l9;
let y be object;
reconsider t = w+*u as Element of product the_Values_of STC N
by CARD_3:107;
hereby
assume y in F;
then ex s being Element of product the_Values_of STC N
st y = IC Exec(i,s) & IC s = l;
then y = z + 1 by A1,A2,Lm2;
hence y in {z+1} by TARSKI:def 1;
end;
assume y in {z+1};
then
A4: y = z+1 by TARSKI:def 1;
IC M in dom u by TARSKI:def 1;
then
A5: IC t = u.IC M by FUNCT_4:13
.= z by A1,FUNCOP_1:72;
then IC Exec(i,t) = z+1 by A2,Lm2;
hence y in F by A1,A4,A5;
end;
hence thesis by TARSKI:2;
end;
registration
let N be with_zero set;
cluster STC N -> weakly_standard;
coherence
proof
reconsider f = id NAT as sequence of NAT;
set M = STC N;
now
let k be Element of NAT;
reconsider fk = f.k as Element of NAT;
A1: SUCC(fk,STC N) = {k,k+1} by AMISTD_1:8;
thus f.(k+1) in SUCC(f.k,STC N) by A1,TARSKI:def 2;
let j be Element of NAT;
assume f.j in SUCC(f.k,STC N);
then f.j = k or f.j = k+1 by A1,TARSKI:def 2;
then j = k+1 or j = k;
hence k <= j by NAT_1:11;
end;
hence thesis by Th4;
end;
end;
registration
let N be with_zero set;
cluster weakly_standard halting
for IC-Ins-separated non empty with_non-empty_values AMI-Struct
over N;
existence
proof
take STC N;
thus thesis;
end;
end;
reserve T for weakly_standard
IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N;
definition
let N be with_zero set,
S be weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, k be natural Number;
func il.(S,k) -> Element of NAT means
:Def4:
ex f being
sequence of NAT st f is bijective & (for m, n being Element of NAT holds
m <= n iff f.m <= f.n, S) & it = f.k;
existence
proof
reconsider k as Element of NAT by ORDINAL1:def 12;
consider f being sequence of NAT such that
A1: f is bijective & for m, n being Element of NAT holds m <= n iff f.
m <= f.n, S by Def3;
reconsider fk = f.k as Element of NAT;
take fk;
take f;
thus thesis by A1;
end;
uniqueness by Th2;
end;
theorem Th5:
for N,T
for k1, k2 being Nat st il.(T,k1) = il.(T,k2) holds
k1 = k2
proof let N,T;
let k1, k2 be Nat;
assume
A1: il.(T,k1) = il.(T,k2);
A2: k1 is Element of NAT & k2 is Element of NAT by ORDINAL1:def 12;
consider f2 being sequence of NAT such that
A3: f2 is bijective & for m, n being Element of NAT holds m <= n iff f2.
m <= f2. n, T and
A4: il.(T,k2) = f2.k2 by Def4;
consider f1 being sequence of NAT such that
A5: f1 is bijective and
A6: for m, n being Element of NAT holds m <= n iff f1.m <= f1.n, T and
A7: il.(T,k1) = f1.k1 by Def4;
A8: dom f1 = NAT by FUNCT_2:def 1;
f1 = f2 by A5,A6,A3,Th2;
hence thesis by A1,A2,A5,A7,A4,A8,FUNCT_1:def 4;
end;
theorem Th6:
for l being Nat ex k being Nat st l = il.(T,k)
proof
let l be Nat;
consider f1 being sequence of NAT such that
A1: f1 is bijective and
A2: for m, n being Element of NAT holds m <= n iff f1.m <= f1.n, T and
il.(T,0) = f1.0 by Def4;
l in NAT & rng f1 = NAT by A1,FUNCT_2:def 3,ORDINAL1:def 12;
then consider k being object such that
A3: k in dom f1 and
A4: f1.k = l by FUNCT_1:def 3;
reconsider k as Nat by A3;
take k;
reconsider l as Element of NAT by ORDINAL1:def 12;
l = il.(T,k) by A1,A2,A4,Def4;
hence thesis;
end;
definition
let N be with_zero set,
S be weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, l be Nat;
func locnum(l,S) -> Nat means
:Def5:
il.(S,it) = l;
existence by Th6;
uniqueness by Th5;
end;
definition
let N be with_zero set,
S be weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, l be Nat;
redefine func locnum(l,S) -> Element of NAT;
coherence by ORDINAL1:def 12;
end;
theorem Th7:
for l1, l2 being Element of NAT holds locnum(l1,T) =
locnum(l2,T) implies l1 = l2
proof
let l1, l2 be Element of NAT;
assume
A1: locnum(l1,T) = locnum(l2,T);
il.(T,locnum(l1,T)) = l1 by Def5;
hence thesis by A1,Def5;
end;
theorem Th8:
for N,T
for k1, k2 being natural Number holds
il.(T,k1) <= il.(T,k2), T iff k1 <= k2
proof let N,T;
let k1, k2 be natural Number;
A1: k1 is Element of NAT & k2 is Element of NAT by ORDINAL1:def 12;
consider f2 being sequence of NAT such that
A2: f2 is bijective & for m, n being Element of NAT holds m <= n iff f2.
m <= f2. n, T and
A3: il.(T,k2) = f2.k2 by Def4;
consider f1 being sequence of NAT such that
A4: f1 is bijective and
A5: for m, n being Element of NAT holds m <= n iff f1.m <= f1.n, T and
A6: il.(T,k1) = f1.k1 by Def4;
f1 = f2 by A4,A5,A2,Th2;
hence thesis by A1,A5,A6,A3;
end;
theorem Th9:
for N,T
for l1, l2 being Element of NAT holds locnum(l1,T) <=
locnum(l2,T) iff l1 <= l2, T
proof let N,T;
let l1, l2 be Element of NAT;
il.(T,locnum(l1,T)) = l1 & il.(T,locnum(l2,T)) = l2 by Def5;
hence thesis by Th8;
end;
theorem Th10:
for N,T holds T is InsLoc-antisymmetric
proof let N,T;
let l1, l2 be Element of NAT;
assume
A1: l1 <= l2, T & l2 <= l1, T;
reconsider T as weakly_standard IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N;
reconsider l1, l2 as Element of NAT;
locnum(l1,T) <= locnum(l2,T) & locnum(l2,T) <= locnum(l1,T) by A1,Th9;
hence thesis by Th7,XXREAL_0:1;
end;
registration
let N;
cluster weakly_standard -> InsLoc-antisymmetric
for IC-Ins-separated non
empty with_non-empty_values AMI-Struct over N;
coherence by Th10;
end;
definition
let N be with_zero set,
S be weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, f be
Element of NAT, k be Nat;
func f +(k,S) -> Element of NAT equals
il.(S,locnum(f,S) + k);
coherence;
end;
theorem
for f being Element of NAT holds f + (0,T) = f by Def5;
theorem
for f, g being Element of NAT st f + (z,T) = g + (z,T)
holds f = g
proof
let f, g be Element of NAT;
assume f + (z,T) = g + (z,T);
then locnum(f,T) + z = locnum(g,T) + z by Th5;
hence thesis by Th7;
end;
theorem
for f being Element of NAT
holds locnum(f,T) + z = locnum(f+(z,T),T) by Def5;
definition
let N be with_zero set,
S be weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, f be
Element of NAT;
func NextLoc(f,S) -> Element of NAT equals
f + (1,S);
coherence;
end;
theorem
for f being Element of NAT
holds NextLoc(f,T) = il.(T,locnum(f,T)+ 1);
theorem Th15:
for f being Element of NAT holds f <> NextLoc(f,T)
proof
let f be Element of NAT;
assume f = NextLoc(f,T);
then locnum(f,T) = locnum(f,T) + 1 by Def5;
hence thesis;
end;
theorem
for f, g being Element of NAT st NextLoc(f,T) = NextLoc(g,T)
holds f = g
proof
let f, g be Element of NAT such that
A1: NextLoc(f,T) = NextLoc(g,T);
set m = locnum(g,T);
set k = locnum(f,T);
k+0 = k+1-1
.= m+1-1 by A1,Th5
.= m+0;
hence thesis by Th7;
end;
theorem Th17:
il.(STC N, z) = z
proof
set M = STC N;
reconsider f2 = id NAT as sequence of NAT;
consider f being sequence of NAT such that
A1: f is bijective & for m, n being Element of NAT holds m <= n iff f.m
<= f.n, STC N and
A2: il.(M,z) = f.z by Def4;
now
let k be Element of NAT;
reconsider fk = f2.k as Element of NAT;
A3: SUCC(fk,STC N) = {k,k+1} by AMISTD_1:8;
thus f2.(k+1) in SUCC(f2.k,STC N) by A3,TARSKI:def 2;
let j be Element of NAT;
assume f2.j in SUCC(f2.k,STC N);
then j = k or j = k+1 by A3,TARSKI:def 2;
hence k <= j by NAT_1:11;
end;
then for m, n being Element of NAT holds m <= n iff f2.m <= f2.n, M by Th3;
then z is Element of NAT & f = f2 by A1,Th2,ORDINAL1:def 12;
hence thesis by A2;
end;
theorem
for i being Instruction of STC N, s being State of STC N st InsCode i
= 1 holds IC Exec(i,s) = NextLoc(IC s,STC N)
proof
let i be Instruction of STC N, s be State of STC N;
set M = STC N;
set k = locnum(IC s,STC N);
reconsider K = IC s as Element of NAT;
assume InsCode i = 1;
then
A1: IC Exec(i,s) = IC s + 1 by Lm2
.= K+1;
il.(M,k) = k & il.(M,k+1) = k+1 by Th17;
hence thesis by A1,Def5;
end;
theorem
for l being Element of NAT, i being Element of the
InstructionsF of STC N st InsCode i = 1 holds NIC(i, l) = {NextLoc(l,STC N)}
proof
let l be Element of NAT, i be Element of the InstructionsF of
STC N;
assume
A1: InsCode i = 1;
set M = STC N;
consider k being Nat such that
A2: l = il.(M,k) by Th6;
k = locnum(l,M) by A2,Def5;
then NextLoc(l,STC N) = k+1 by Th17;
hence thesis by A1,A2,Lm3,Th17;
end;
theorem
for l being Element of NAT holds SUCC(l,STC N) = {l, NextLoc(l,STC N)}
proof
let l be Element of NAT;
set M = STC N;
consider k being Nat such that
A1: l = il.(M,k) by Th6;
A2: k = locnum(l,M) by A1,Def5;
thus SUCC(l,STC N) = {k,k+1} by A1,Th17,AMISTD_1:8
.= {k,il.(M,k+1)} by Th17
.= {l, NextLoc(l,STC N)} by A1,A2,Th17;
end;
definition
let N be with_zero set,
S be weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, i be Instruction of
S;
attr i is sequential means
for s being State of S holds Exec(i, s).IC S = NextLoc(IC s,S);
end;
theorem Th21:
for S being weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, il being Element of NAT,
i being Instruction of S st i is sequential holds NIC(i,il)
= {NextLoc(il,S)}
proof
let S be weakly_standard IC-Ins-separated
non empty
with_non-empty_values AMI-Struct over N, il be Element of NAT, i be
Instruction of S such that
A1: for s being State of S holds Exec(i, s).IC S = NextLoc(IC s,S);
now
let x be object;
A2: now
reconsider il1 = il as Element of Values IC S by MEMSTR_0:def 6;
set I = i;
set t = the State of S,
P = the Instruction-Sequence of S;
assume
A3: x = NextLoc(il,S);
reconsider u = t+*(IC S,il1) as
Element of product the_Values_of S by CARD_3:107;
il in NAT;
then
A4: il in dom P by PARTFUN1:def 2;
A5: (P+*(il,i))/.il = (P+*(il,i)).il by PBOOLE:143
.= i by A4,FUNCT_7:31;
IC S in dom t by MEMSTR_0:2;
then
A6: IC u = il by FUNCT_7:31;
then IC Following(P+*(il,i),u) = NextLoc(il,S) by A1,A5;
hence x in {IC Exec(i,ss)
where ss is Element of product the_Values_of S
: IC ss = il} by A3,A6,A5;
end;
now
assume x in {IC Exec(i,ss)
where ss is Element of product the_Values_of S : IC ss = il};
then ex s being Element of product the_Values_of S
st x = IC Exec(i,s) & IC s = il;
hence x = NextLoc(il,S) by A1;
end;
hence
x in {NextLoc(il,S)} iff x in {IC Exec(i,ss)
where ss is Element of product the_Values_of S
: IC ss = il } by A2,TARSKI:def 1;
end;
hence thesis by TARSKI:2;
end;
theorem Th22:
for S being weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
i being Instruction of S st i is sequential
holds i is non halting
proof
let S be weakly_standard IC-Ins-separated
non empty
with_non-empty_values AMI-Struct over N, i be Instruction of S such that
A1: i is sequential;
set s = the State of S;
NIC(i,IC s) = {NextLoc(IC s,S)} by A1,Th21;
then NIC(i,IC s) <> {IC s} by Th15,ZFMISC_1:3;
hence thesis by AMISTD_1:2;
end;
registration
let N;
let S be weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
cluster sequential -> non halting for Instruction of S;
coherence by Th22;
cluster halting -> non sequential for Instruction of S;
coherence;
end;
begin :: Closedness of finite partial states
definition
let N be with_zero set;
let S be weakly_standard IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N;
let F be NAT-defined (the InstructionsF of S)-valued Function;
attr F is para-closed means
for s being State of S st IC s = il.(S,0)
for k being Element of NAT holds IC Comput(F,s,k) in dom F;
end;
theorem Th23:
for S being weakly_standard IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N,
F being NAT-defined (the InstructionsF of S)-valued
finite Function st F is really-closed & il.(S,0) in dom F holds F is
para-closed
by AMISTD_1:14;
theorem Th24:
for S being weakly_standard halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N holds il.(S,0) .-->
halt S qua NAT-defined (the InstructionsF of S)-valued
finite Function is really-closed
proof
let S be weakly_standard halting IC-Ins-separated
non empty
with_non-empty_values AMI-Struct over N;
reconsider F = il.(S,0) .--> halt S as
NAT-defined (the InstructionsF of S)-valued finite Function;
let l be Nat;
assume
A1: l in dom(il.(S,0) .--> halt S);
A3: l = il.(S,0) by A1,TARSKI:def 1;
F/.l = F.l by A1,PARTFUN1:def 6
.= halt S by A3,FUNCOP_1:72;
hence thesis by A3,AMISTD_1:2;
end;
definition
let N be with_zero set;
let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over
N;
let F be (the InstructionsF of S)-valued NAT-defined finite Function;
attr F is lower means
:Def10:
for l being Element of NAT st l in
dom F holds for m being Element of NAT st m <= l, S
holds m in dom F;
end;
registration
let N be with_zero set,
S be IC-Ins-separated non
empty with_non-empty_values AMI-Struct over N;
cluster empty -> lower
for finite (the InstructionsF of S)-valued NAT-defined Function;
coherence;
end;
theorem Th25:
for i being Element of the InstructionsF of T
holds il.(T,0) .--> i is lower
proof
let i be Element of the InstructionsF of T;
set F = il.(T,0).--> i;
let l be Element of NAT such that
A1: l in dom F;
let m be Element of NAT such that
A2: m <= l, T;
consider k being Nat such that
A3: m = il.(T,k) by Th6;
A4: l = il.(T,0) by A1,TARSKI:def 1;
then 0 <= k & k <= 0 by A2,A3,Th8;
hence thesis by A1,A4,A3,XXREAL_0:1;
end;
registration
let N be with_zero set;
let S be weakly_standard IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N;
cluster lower 1-element for NAT-defined
(the InstructionsF of S)-valued finite Function;
existence
proof
set i = the Instruction of S;
take il.(S,0).--> i;
thus thesis by Th25;
end;
end;
theorem Th26:
for F being lower non empty
NAT-defined (the InstructionsF of T)-valued finite Function
holds il.(T,0) in dom F
proof
let F be lower non empty
NAT-defined (the InstructionsF of T)-valued finite Function;
consider l being object such that
A1: l in dom F by XBOOLE_0:def 1;
reconsider l as Element of NAT by A1;
consider f being sequence of NAT such that
A2: f is bijective and
A3: for m, n being Element of NAT holds m <= n iff f.m <= f.n, T and
A4: il.(T,0) = f.0 by Def4;
rng f = NAT by A2,FUNCT_2:def 3;
then consider x being object such that
A5: x in dom f and
A6: l = f.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A5;
f.0 <= f.x, T by A3;
hence thesis by A1,A4,A6,Def10;
end;
theorem Th27:
for P being lower
NAT-defined (the InstructionsF of T)-valued finite Function
holds z < card P iff il.(T,z) in dom P
proof
let P be lower NAT-defined (the InstructionsF of T)-valued finite Function;
deffunc F(Element of NAT) = il.(T,$1);
defpred P[Element of NAT] means F($1) in dom P;
set A = { k : P[k]};
A1: A is Subset of NAT from DOMAIN_1:sch 7;
A2: now
let a, b be Nat;
assume a in A;
then
A3: ex l being Element of NAT st l = a & il.(T,l) in dom P;
A4: b in NAT by ORDINAL1:def 12;
assume b < a;
then il.(T,b) <= il.(T,a), T by Th8;
then il.(T,b) in dom P by A3,Def10;
hence b in A by A4;
end;
A5: now
let x be set;
assume x in dom P;
then reconsider l=x as Element of NAT;
consider n being Nat such that
A6: l = il.(T,n) by Th6;
reconsider n as Element of NAT by ORDINAL1:def 12;
take n;
thus x = F(n) by A6;
end;
reconsider A as Cardinal by A1,A2,FUNCT_7:20;
set A1 = {k : F(k) in dom P};
A7: z is Element of NAT by ORDINAL1:def 12;
A8: for k1, k2 being Element of NAT st F(k1) = F(k2) holds k1 = k2 by Th5;
A9: dom P, A1 are_equipotent from FUNCT_7:sch 3(A5,A8);
hereby
assume z < card P;
then card Segm z in card Segm card P by NAT_1:41;
then z in card dom P by CARD_1:62;
then z in card A by A9,CARD_1:5;
then ex d being Element of NAT st d = z & il.(T,d) in dom P;
hence il.(T,z) in dom P;
end;
assume il.(T,z) in dom P;
then z in card A by A7;
then z in card dom P by A9,CARD_1:5;
then card Segm z in card Segm card P by CARD_1:62;
hence thesis by NAT_1:41;
end;
definition
let N be with_zero set;
let S be weakly_standard IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N;
let F be non empty
NAT-defined (the InstructionsF of S)-valued finite Function;
func LastLoc F -> Element of NAT means
:Def11:
ex M being finite non empty natural-membered set
st M = { locnum(l,S) where l is
Element of NAT : l in dom F } & it = il.(S, max M);
existence
proof
deffunc F(Element of NAT) = locnum($1,S);
set M = { F(l) where l is Element of NAT : l in dom F };
set l = the Element of dom F;
reconsider l as Element of NAT;
A1: locnum(l,S) in M;
A2: M c= NAT
proof
let k be object;
assume k in M;
then
ex l being Element of NAT st k = locnum(l,S) & l in dom F;
hence thesis;
end;
A3: dom F is finite;
M is finite from FRAENKEL:sch 21(A3);
then reconsider M as finite non empty Subset of NAT by A1,A2;
take il.(S, max M), M;
thus thesis;
end;
uniqueness;
end;
theorem Th28:
for F being non empty
NAT-defined (the InstructionsF of T)-valued finite Function
holds LastLoc F in dom F
proof
let F be non empty
NAT-defined (the InstructionsF of T)-valued finite Function;
consider M being finite non empty natural-membered set such that
A1: M = { locnum(l,T) where l is Element of NAT : l in dom F } and
A2: LastLoc F = il.(T, max M) by Def11;
max M in M by XXREAL_2:def 8;
then
ex l being Element of NAT st max M = locnum(l,T) & l in dom F
by A1;
hence thesis by A2,Def5;
end;
theorem
for F, G being non empty
NAT-defined (the InstructionsF of T)-valued finite Function
st F c= G
holds LastLoc F <= LastLoc G, T
proof
let F, G be non empty
NAT-defined (the InstructionsF of T)-valued finite Function
such that
A1: F c= G;
consider N being finite non empty natural-membered set such that
A2: N = { locnum(l,T) where l is Element of NAT : l in dom G } and
A3: LastLoc G = il.(T, max N) by Def11;
consider M being finite non empty natural-membered set such that
A4: M = { locnum(l,T) where l is Element of NAT : l in dom F } and
A5: LastLoc F = il.(T, max M) by Def11;
reconsider MM = M, NN = N as non empty finite Subset of REAL by MEMBERED:3;
M c= N
proof
let a be object;
assume a in M;
then
A6: ex l being Element of NAT st a = locnum(l,T) & l in dom F by A4;
dom F c= dom G by A1,GRFUNC_1:2;
hence thesis by A2,A6;
end;
then max MM <= max NN by XXREAL_2:59;
hence thesis by A5,A3,Th8;
end;
theorem Th30:
for F being non empty
NAT-defined (the InstructionsF of T)-valued finite Function,
l being
Element of NAT st l in dom F holds l <= LastLoc F, T
proof
let F be non empty
NAT-defined (the InstructionsF of T)-valued finite Function,
l be Element of NAT
such that
A1: l in dom F;
consider M being finite non empty natural-membered set such that
A2: M = { locnum(w,T) where w is Element of NAT : w in dom F } and
A3: LastLoc F = il.(T, max M) by Def11;
locnum(l,T) in M by A1,A2;
then
A4: locnum(l,T) <= max M by XXREAL_2:def 8;
max M is Nat by TARSKI:1;
then locnum(LastLoc F,T) = max M by A3,Def5;
hence thesis by A4,Th9;
end;
theorem
for F being lower non empty
NAT-defined (the InstructionsF of T)-valued finite Function,
G being non empty NAT-defined
NAT-defined (the InstructionsF of T)-valued finite Function
holds F c= G & LastLoc F = LastLoc G
implies F = G
proof
let F be lower non empty
NAT-defined (the InstructionsF of T)-valued finite Function,
G be non empty
NAT-defined (the InstructionsF of T)-valued finite Function
such that
A1: F c= G and
A2: LastLoc F = LastLoc G;
dom F = dom G
proof
thus dom F c= dom G by A1,GRFUNC_1:2;
let x be object;
assume
A3: x in dom G;
reconsider x as Element of NAT by A3;
A4: LastLoc F in dom F by Th28;
x <= LastLoc F, T by A2,A3,Th30;
hence thesis by A4,Def10;
end;
hence thesis by A1,GRFUNC_1:3;
end;
theorem Th32:
for F being lower non empty
NAT-defined (the InstructionsF of T)-valued finite Function
holds LastLoc F = il.(T, card F -' 1)
proof
let F be lower non empty
NAT-defined (the InstructionsF of T)-valued finite Function;
consider k being Nat such that
A1: LastLoc F = il.(T,k) by Th6;
reconsider k as Element of NAT by ORDINAL1:def 12;
LastLoc F in dom F by Th28;
then k < card F by A1,Th27;
then
A2: k <= card F -' 1 by NAT_D:49;
per cases by A2,XXREAL_0:1;
suppose
k < card F -' 1;
then k+1 < card F -' 1 + 1 by XREAL_1:6;
then k+1 < card F by NAT_1:14,XREAL_1:235;
then il.(T,k+1) in dom F by Th27;
then il.(T,k+1) <= LastLoc F, T by Th30;
then
A3: k+1 <= k by A1,Th8;
k <= k+1 by NAT_1:11;
then k+0 = k+1 by A3,XXREAL_0:1;
hence thesis;
end;
suppose
k = card F -' 1;
hence thesis by A1;
end;
end;
registration
let N be with_zero set,
S be weakly_standard
IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;
cluster really-closed lower non empty -> para-closed for NAT-defined
(the InstructionsF of S)-valued finite Function;
coherence
by Th26,Th23;
end;
Lm4: now
let N;
let S be weakly_standard halting IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N;
set F = il.(S,0) .--> halt S;
A1: card dom F = 1 by CARD_1:30;
F is lower NAT-defined (the InstructionsF of S)-valued finite Function
by Th25;
then
A2: LastLoc F = il.(S,card F -' 1) by Th32
.= il.(S,card dom F -' 1) by CARD_1:62
.= il.(S,0) by A1,XREAL_1:232;
hence F.(LastLoc F) = halt S by FUNCOP_1:72;
let l be Element of NAT such that
F.l = halt S;
assume l in dom F;
hence l = LastLoc F by A2,TARSKI:def 1;
end;
definition
let N be with_zero set,
S be weakly_standard halting
IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, F
be non empty NAT-defined (the InstructionsF of S)-valued finite Function;
attr F is halt-ending means
:Def12:
F.(LastLoc F) = halt S;
attr F is unique-halt means
:Def13:
for f being Element of NAT st
F.f = halt S & f in dom F holds f = LastLoc F;
end;
registration
let N be with_zero set;
let S be weakly_standard halting IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N;
cluster halt-ending unique-halt trivial
for lower non empty
NAT-defined (the InstructionsF of S)-valued finite Function;
existence
proof
reconsider F = il.(S,0) .--> halt S as lower non empty
NAT-defined (the InstructionsF of S)-valued finite Function
by Th25;
take F;
thus F.(LastLoc F) = halt S by Lm4;
thus for f being Element of NAT st F.f = halt S & f in dom F
holds f = LastLoc F by Lm4;
thus thesis;
end;
end;
registration
let N be with_zero set;
let S be weakly_standard halting IC-Ins-separated
non empty
with_non-empty_values AMI-Struct over N;
cluster trivial really-closed lower non empty
for NAT-defined (the InstructionsF of S)-valued finite Function;
existence
proof
reconsider F = il.(S,0) .--> halt S as lower non empty
NAT-defined (the InstructionsF of S)-valued finite Function
by Th25;
take F;
thus thesis by Th24;
end;
end;
registration
let N be with_zero set;
let S be weakly_standard halting IC-Ins-separated
non empty
with_non-empty_values AMI-Struct over N;
cluster halt-ending unique-halt trivial really-closed
for lower non empty
NAT-defined (the InstructionsF of S)-valued finite Function;
existence
proof
reconsider F = il.(S,0) .--> halt S as lower non empty
NAT-defined (the InstructionsF of S)-valued finite Function
by Th25;
take F;
thus F.(LastLoc F) = halt S by Lm4;
thus for f being Element of NAT st F.f = halt S & f in dom F
holds f = LastLoc F by Lm4;
thus thesis by Th24;
end;
end;
definition
let N be with_zero set;
let S be weakly_standard halting IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N;
mode pre-Macro of S is halt-ending unique-halt
lower non empty
NAT-defined (the InstructionsF of S)-valued finite Function;
end;
registration
let N be with_zero set;
let S be weakly_standard halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
cluster really-closed for pre-Macro of S;
existence
proof
reconsider F = il.(S,0) .--> halt S as lower non empty
NAT-defined (the InstructionsF of S)-valued finite Function
by Th25;
F.(LastLoc F) = halt S & for l being Element of NAT st F.l
= halt S & l in dom F holds l = LastLoc F by Lm4;
then reconsider F as pre-Macro of S by Def12,Def13;
take F;
thus thesis by Th24;
end;
end;
theorem
for N being with_zero set,
S being IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
l1, l2 being Element of NAT st SUCC(l1,S) = NAT
holds l1 <= l2, S
proof
let N be with_zero set,
S be IC-Ins-separated non
empty with_non-empty_values AMI-Struct over N, l1, l2 be Element of NAT
such that
A1: SUCC(l1,S) = NAT;
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 NAT st P[n,d]
proof
let n be Nat;
assume
A3: n in Seg 2;
per cases by A3,FINSEQ_1:2,TARSKI:def 2;
suppose
A4: n = 1;
reconsider l1 as Element of NAT;
take l1;
thus thesis by A4;
end;
suppose
A5: n = 2;
reconsider l2 as Element of NAT;
take l2;
thus thesis by A5;
end;
end;
consider f being FinSequence of NAT such that
A6: len f = 2 and
A7: for n being Nat st n in Seg 2 holds P[n,f/.n] from FINSEQ_4:sch 1(A2);
A8: 1 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
then
A9: f/.1 = l1 by A7;
reconsider f as non empty FinSequence of NAT by A6;
take f;
2 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
hence f/.1 = l1 & f/.len f = l2 by A6,A7,A8;
let n be Element of NAT;
assume
A10: 1 <= n;
assume n < len f;
then n < 1+1 by A6;
then n <= 1 by NAT_1:13;
then n = 1 by A10,XXREAL_0:1;
hence thesis by A1,A9;
end;
:: from SCMRING4, 2008.03.13, A.T.
reserve i, j, k for Nat,
n for Element of NAT,
N for with_zero set,
S for weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
l for Element of NAT,
f for FinPartState of S;
definition
let N be with_zero set,
S be weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, loc be
Element of NAT, k be Nat;
func loc -' (k,S) -> Element of NAT equals
il.(S, (locnum(loc,S)) -' k);
coherence;
end;
theorem
l -' (0,S) = l
by NAT_D:40,Def5;
theorem
l + (k,S) -' (k,S) = l
proof
thus l + (k,S) -' (k,S) = il.(S,locnum(l,S) + k -' k) by Def5
.= il.(S,locnum(l,S)) by NAT_D:34
.= l by Def5;
end;