:: Standard Ordering of Instruction Locations
:: by Andrzej Trybulec , Piotr Rudnicki and Artur Korni{\l}owicz
::
:: Received April 14, 2000
:: Copyright (c) 2000-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, XBOOLE_0, SUBSET_1, SETFAM_1, AMI_1, FSM_1, FUNCT_4,
FUNCOP_1, RELAT_1, TARSKI, STRUCT_0, FUNCT_1, CARD_3, ZFMISC_1, CIRCUIT2,
CAT_1, NAT_1, GLIB_000, XXREAL_0, PARTFUN1, FINSEQ_1, ARYTM_3, CARD_1,
GOBOARD5, FUNCT_2, FINSEQ_4, ARYTM_1, FINSET_1, FRECHET, AMISTD_1,
EXTPRO_1, COMPOS_1, AMISTD_2, SCMFSA6B, QUANTAL1, GOBRD13, MEMSTR_0,
FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, SETFAM_1, ORDINAL1,
CARD_1, XXREAL_0, NUMBERS, XCMPLX_0, NAT_1, MEMBERED, FUNCT_1, RELSET_1,
PARTFUN1, XTUPLE_0, MCART_1, VALUED_1, DOMAIN_1, CARD_3, FINSEQ_1,
FINSEQ_4, FUNCOP_1, FINSET_1, FUNCT_4, FUNCT_7, AFINSQ_1, PBOOLE,
MEASURE6, STRUCT_0, GRAPH_2, NAT_D, XXREAL_2, MEMSTR_0, COMPOS_0,
COMPOS_1, EXTPRO_1, FUNCT_2;
constructors WELLORD2, REAL_1, FINSEQ_4, REALSET1, NAT_D, XXREAL_2, COMPOS_1,
EXTPRO_1, RELSET_1, PRE_POLY, GRAPH_2, AFINSQ_1, MCART_1, FUNCT_7,
PBOOLE, XXREAL_1, FUNCT_4, MEASURE6, MEMSTR_0, XTUPLE_0;
registrations SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSET_1,
XREAL_0, NAT_1, MEMBERED, FINSEQ_1, CARD_3, FUNCT_7, STRUCT_0, CARD_1,
RELSET_1, FUNCT_4, AFINSQ_1, COMPOS_1, EXTPRO_1, PRE_POLY, MEMSTR_0,
MEASURE6, COMPOS_0, XTUPLE_0, INT_1;
requirements NUMERALS, BOOLE, REAL, SUBSET, ARITHM;
definitions TARSKI, EXTPRO_1, XBOOLE_0, MEMSTR_0, FUNCT_1, COMPOS_0;
equalities STRUCT_0, COMPOS_1, EXTPRO_1, XBOOLE_0, MEMSTR_0, FUNCOP_1,
AFINSQ_1, COMPOS_0, ORDINAL1;
expansions XBOOLE_0, MEMSTR_0;
theorems TARSKI, FINSEQ_4, FINSEQ_1, NAT_1, FUNCT_4, FUNCT_1, FUNCT_2,
ENUMSET1, ZFMISC_1, FUNCOP_1, CARD_3, ORDINAL1, FINSEQ_3, INT_1,
SETFAM_1, REVROT_1, EXTPRO_1, RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_1,
XXREAL_0, COMPOS_1, FUNCT_7, PARTFUN1, XREAL_0, NAT_D, PBOOLE, MEMSTR_0,
GRFUNC_1, PARTFUN2, MEASURE6, RELAT_1, FINSEQ_6;
schemes NAT_1, FINSEQ_2, FUNCT_2;
begin :: AMI-Struct
reserve x for set,
D for non empty set,
k, n for 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 Nat,
s for State of S;
registration
let N be with_zero set, S be
with_non-empty_values AMI-Struct over N,
i be Element of the InstructionsF of S, s be State of S;
cluster ((the Execution of S).i).s -> Function-like Relation-like;
coherence
proof
reconsider A =(the Execution of S).i
as Function of product the_Values_of S, product the_Values_of S
by FUNCT_2:66;
reconsider s as Element of product the_Values_of S
by CARD_3:107;
A.s in product the_Values_of S;
hence thesis;
end;
end;
registration let N;
cluster non empty with_non-empty_values for AMI-Struct over N;
existence
proof
take Trivial-AMI N;
thus thesis;
end;
end;
definition
let N be with_zero set;
let S be non empty with_non-empty_values AMI-Struct over N;
let T be InsType of the InstructionsF of S;
attr T is jump-only means
for s being State of S, o being Object of S, I
being Instruction of S st InsCode I = T &
o in Data-Locations S
holds Exec(I, s).o = s.o;
end;
definition
let N be with_zero set;
let S be non empty with_non-empty_values AMI-Struct over N;
let I be Instruction of S;
attr I is jump-only means
InsCode I is jump-only;
end;
reserve ss for Element of product the_Values_of S;
definition
let N,S; let l be Nat;
let i be Element of the InstructionsF of S;
func NIC(i,l) -> Subset of NAT equals
{ IC Exec(i,ss) : IC ss = l };
coherence
proof
{ IC Exec(i,ss) : IC ss = l } c= NAT
proof
let e be object;
assume e in { IC Exec(i,ss) : IC ss = l };
then ex ss st e = IC Exec(i,ss) & IC ss = l;
hence thesis;
end;
hence thesis;
end;
end;
Lm1:
now
let N;
let S be IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
i be Element of the InstructionsF of S, l be
Nat, s be State of S,
P be Instruction-Sequence of S;
reconsider t = s+*(IC S,l) as Element of product the_Values_of S
by CARD_3:107;
l in NAT by ORDINAL1:def 12;
then
A1: l in dom P by PARTFUN1:def 2;
IC S in dom s by MEMSTR_0:2;
then
A2: IC t = l by FUNCT_7:31;
then CurInstr(P+*(l,i),t) = (P+*(l,i)).l by PBOOLE:143
.= i by A1,FUNCT_7:31;
hence IC Following(P+*(l,i),s+*(IC S,l)) in NIC(i,l) by A2;
end;
registration
let N be with_zero set,
S be IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, i be Element of the
InstructionsF of S, l be Nat;
cluster NIC(i,l) -> non empty;
coherence by Lm1;
end;
definition
let N,S,i;
func JUMP i -> Subset of NAT equals
meet the set of all NIC(i,l) ;
coherence
proof
set X = the set of all NIC(i,l) ;
X c= bool NAT
proof
let x be object;
assume x in X;
then ex l st x = NIC(i,l);
hence thesis;
end;
then reconsider X as Subset-Family of NAT;
meet X c= NAT;
hence thesis;
end;
end;
definition
let N,S; let l be Nat;
func SUCC(l,S) -> Subset of NAT equals
union the set of all NIC(i,l) \ JUMP i ;
coherence
proof
set X = the set of all NIC(i,l) \ JUMP i ;
X c= bool NAT
proof
let x be object;
assume x in X;
then ex i st x = NIC(i,l) \ JUMP i;
hence thesis;
end;
then reconsider X as Subset-Family of NAT;
union X c= NAT;
hence thesis;
end;
end;
theorem Th1:
for i being Element of the InstructionsF of S
st for l being Nat holds NIC(i,l)={l}
holds JUMP i is empty
proof
let i be Element of the InstructionsF of S;
set p = 0, q = 1;
set X = the set of all NIC(i, l) where l is Nat;
reconsider p,q as Nat;
assume
A1: for l being Nat holds NIC(i,l)={l};
assume not thesis;
then consider x being object such that
A2: x in meet X;
NIC(i,p) = {p} by A1;
then {p} in X;
then
A3: x in {p} by A2,SETFAM_1:def 1;
NIC(i,q) = {q} by A1;
then {q} in X;
then x in {q} by A2,SETFAM_1:def 1;
hence contradiction by A3,TARSKI:def 1;
end;
theorem Th2:
for S being IC-Ins-separated non empty with_non-empty_values
AMI-Struct over N,
il being Nat, i being Instruction of S st i is halting
holds NIC(i,il) = {il}
proof
let S be IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
il be Nat, i be Instruction of S
such that
A1: for s being State of S holds Exec(i,s) = s;
hereby
let n be object;
assume n in NIC(i,il);
then ex s being Element of product the_Values_of S
st n = IC Exec(i,s) & IC s = il;
then n = il by A1;
hence n in {il} by TARSKI:def 1;
end;
set s = the State of S,
P = the Instruction-Sequence of S;
let n be object;
assume
n in {il};
then
A2: n = il by TARSKI:def 1;
il in NAT by ORDINAL1:def 12;
then
A3: il in dom P by PARTFUN1:def 2;
A4: IC S in dom s by MEMSTR_0:2;
then IC(s+*(IC S,il)) = il by FUNCT_7:31;
then CurInstr(P+*(il,i),s+*(IC S,il))
= (P+*(il,i)).il by PBOOLE:143
.= i by A3,FUNCT_7:31;
then IC Following(P+*(il,i),s+*(IC S,il))
= IC(s+*(IC S,il)) by A1
.= n by A2,A4,FUNCT_7:31;
hence n in NIC(i,il) by Lm1;
end;
begin :: Ordering of Instruction Locations
definition
let N, S;
attr S is standard means
for m, n being Nat holds m <= n iff
ex f being non empty FinSequence of NAT st f/.1 = m & f/.len f = n &
for n st 1 <= n & n < len f holds f/.(n+1) in SUCC(f/.n,S);
end;
Lm2:
ex f being non empty FinSequence of NAT st f/.1
= k & f/.len f = k & for n st 1 <= n & n < len f
holds f/.(n+1) in SUCC(f/.n,S)
proof
reconsider l=k as Element of NAT by ORDINAL1:def 12;
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:
S is standard iff
for k being Nat holds k+1 in SUCC(k,S) &
for j being Nat st j in SUCC(k,S) holds k <= j
proof
hereby
assume
A1: S is standard;
let k be Nat;
k <= k+1 by NAT_1:11;
then consider F being non empty FinSequence of NAT such that
A2: F/.1 = k and
A3: F/.len F = k+1 and
A4: for n st 1 <= n & n < len F holds F/.(n+1) in SUCC(F/.n,S) by A1;
set F1 = F -| (k+1);
set x = (k+1)..F;
A5: k+1 in rng F by A3,FINSEQ_6:168;
then
A6: len F1 = x-1 by FINSEQ_4:34;
then
A7: len F1+1 = x;
A8: x in dom F by A5,FINSEQ_4:20;
then
A9: F/.(len F1+1) = F.x by A6,PARTFUN1:def 6
.= k+1 by A5,FINSEQ_4:19;
x <= len F by A8,FINSEQ_3:25;
then
A10: len F1 < len F by A7,NAT_1:13;
1 <= len F by NAT_1:14;
then
A11: 1 in dom F by FINSEQ_3:25;
then
A12: F/.1 = F.1 by PARTFUN1:def 6;
A13: F.x = k+1 by A5,FINSEQ_4:19;
A14: k <> k+1;
then
A15: len F1 <> 0 by A2,A13,A11,A6,PARTFUN1:def 6;
1 <= x by A8,FINSEQ_3:25;
then 1 < x by A2,A14,A13,A12,XXREAL_0:1;
then
A16: 1 <= len F1 by A7,NAT_1:13;
reconsider F1 as non empty FinSequence of NAT by A15,A5,FINSEQ_4:41;
set m = F/.len F1;
reconsider m as Nat;
A17: len F1 in dom F by A16,A10,FINSEQ_3:25;
A18: len F1 in dom F1 by A16,FINSEQ_3:25;
then
A19: F1/.len F1 = F1.len F1 by PARTFUN1:def 6
.= F.len F1 by A5,A18,FINSEQ_4:36
.= F/.len F1 by A17,PARTFUN1:def 6;
A20: now
(rng F1) misses {k+1} by A5,FINSEQ_4:38;
then rng F1 /\ {k+1} = {};
then
A21: not k+1 in rng F1 or not k+1 in {k+1} by XBOOLE_0:def 4;
assume
A22: m = k+1;
A23: len F1 in dom F1 by A16,FINSEQ_3:25;
then F1/.len F1 = F1.len F1 by PARTFUN1:def 6;
hence contradiction by A19,A22,A21,A23,FUNCT_1:def 3,TARSKI:def 1;
end;
reconsider F2 = <*F/.len F1, F/.x*> as non empty FinSequence of NAT;
A24: len F2 = 2 by FINSEQ_1:44;
then
A25: 2 in dom F2 by FINSEQ_3:25;
then
A26: F2/.len F2 = F2.2 by A24,PARTFUN1:def 6
.= F/.x
.= k+1 by A13,A8,PARTFUN1:def 6;
A27: 1 in dom F2 by A24,FINSEQ_3:25;
A28: 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
A29: n = 1 by NAT_1:25;
then
A30: F2/.n = F2.1 by A27,PARTFUN1:def 6
.= F/.len F1;
F2/.(n+1) = F2.2 by A25,A29,PARTFUN1:def 6
.= F/.(len F1+1) by A6;
hence F2/.(n+1) in SUCC(F2/.n,S) by A4,A16,A10,A30;
end;
A31: now
let n;
assume that
A32: 1 <= n and
A33: n < len F1;
A34: 1 <= n+1 by A32,NAT_1:13;
A35: n+1 <= len F1 by A33,NAT_1:13;
then n+1 <= len F by A10,XXREAL_0:2;
then
A36: n+1 in dom F by A34,FINSEQ_3:25;
n <= len F by A10,A33,XXREAL_0:2;
then
A37: n in dom F by A32,FINSEQ_3:25;
A38: n in dom F1 by A32,A33,FINSEQ_3:25;
then
A39: F1/.n = F1.n by PARTFUN1:def 6
.= F.n by A5,A38,FINSEQ_4:36
.= F/.n by A37,PARTFUN1:def 6;
A40: n < len F by A10,A33,XXREAL_0:2;
A41: n+1 in dom F1 by A34,A35,FINSEQ_3:25;
then F1/.(n+1) = F1.(n+1) by PARTFUN1:def 6
.= F.(n+1) by A5,A41,FINSEQ_4:36
.= F/.(n+1) by A36,PARTFUN1:def 6;
hence F1/.(n+1) in SUCC(F1/.n,S) by A4,A32,A39,A40;
end;
F2/.1 = F2.1 by A27,PARTFUN1:def 6
.= m;
then
A42: m <= k+1 by A1,A26,A28;
A43: 1 in dom F1 by A16,FINSEQ_3:25;
then F1/.1 = F1.1 by PARTFUN1:def 6
.= F.1 by A5,A43,FINSEQ_4:36
.= k by A2,A11,PARTFUN1:def 6;
then k <= m by A1,A19,A31;
then m = k or m = k+1 by A42,NAT_1:9;
hence k+1 in SUCC(k,S) by A4,A16,A10,A9,A20;
let j be Nat;
reconsider fk=k, fj=j as Element of NAT by ORDINAL1:def 12;
reconsider F = <*fk, fj*> as non empty FinSequence of NAT;
A44: len F = 2 by FINSEQ_1:44;
then
A45: 2 in dom F by FINSEQ_3:25;
A46: 1 in dom F by A44,FINSEQ_3:25;
then
A47: F/.1 = F.1 by PARTFUN1:def 6
.= k;
assume
A48: j in SUCC(k,S);
A49: now
let n be 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
A50: n = 1 by NAT_1:25;
then
A51: F/.n = F.1 by A46,PARTFUN1:def 6
.= k;
F/.(n+1) = F.2 by A45,A50,PARTFUN1:def 6
.= j;
hence F/.(n+1) in SUCC(F/.n,S) by A48,A51;
end;
F/.len F = F.2 by A44,A45,PARTFUN1:def 6
.= j;
hence k <= j by A1,A47,A49;
end;
assume
A52: for k being Nat holds k+1 in SUCC(k,S) & for j
being Nat st j in SUCC(k,S) holds k <= j;
thus S is standard
proof
let m, n be Nat;
thus m <= n implies ex f being non empty FinSequence of NAT st f/.1
= m & f/.len f = n &
for k st 1 <= k & k < len f holds f/.(k+1) in SUCC(f/.k,S)
proof
assume
A53: m <= n;
per cases by A53,XXREAL_0:1;
suppose
m = n;
hence ex f being non empty FinSequence of NAT st f/.1
= m & f/.len f = n & for n st 1 <= n & n < len f
holds f/.(n+1) in SUCC(f/.n,S) by Lm2;
end;
suppose
A54: m < n;
thus ex f being non empty FinSequence of NAT st f/.1
= m & f/.len f = n & for n st 1 <= n & n < len f
holds f/.(n+1) in SUCC(f/.n,S)
proof
set mn = n -' m;
deffunc F(Nat) = m+$1-'1;
consider F being FinSequence of NAT such that
A55: len F = mn+1 and
A56: 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 A55;
take F;
A57: 1 <= mn+1 by NAT_1:11;
then
A58: 1 in dom F by A55,FINSEQ_3:25;
hence F/.1 = F.1 by PARTFUN1:def 6
.= m+1-'1 by A56,A58
.= m by NAT_D:34;
m+1 <= n by A54,INT_1:7;
then 1 <= n-m by XREAL_1:19;
then 0 <= n-m;
then
A59: mn = n - m by XREAL_0:def 2;
A60: len F in dom F by A55,A57,FINSEQ_3:25;
hence F/.len F = F.len F by PARTFUN1:def 6
.= m+(mn+1)-'1 by A55,A56,A60
.= m+mn+1-'1
.= n by A59,NAT_D:34;
let p be Nat;
assume that
A61: 1 <= p and
A62: p < len F;
A63: p in dom F by A61,A62,FINSEQ_3:25;
then
A64: F/.p = F.p by PARTFUN1:def 6
.= m+p-'1 by A56,A63;
A65: p <= m+p by NAT_1:11;
1 <= p+1 & p+1 <= len F by A61,A62,NAT_1:13;
then
A66: p+1 in dom F by FINSEQ_3:25;
then F/.(p+1) = F.(p+1) by PARTFUN1:def 6
.= m+(p+1)-'1 by A56,A66
.= m+p+1-'1
.= m+p-'1+1 by A61,A65,NAT_D:38,XXREAL_0:2;
hence thesis by A52,A64;
end;
end;
end;
given F being non empty FinSequence of NAT such that
A67: F/.1 = m and
A68: F/.len F = n and
A69: for n being 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
Nat st F/.$1 = l & m <= l;
A70: now
let k be Nat such that
A71: P[k];
now
assume that
1 <= k+1 and
A72: k+1 <= len F;
per cases;
suppose
k = 0;
hence ex l being Nat st F/.(k+1) = l & m <= l by A67;
end;
suppose
A73: k > 0;
set l1 = F/.(k+1);
consider l being Nat such that
A74: F/.k = l and
A75: m <= l by A71,A72,A73,NAT_1:13,14;
reconsider l1 as Nat;
k < len F by A72,NAT_1:13;
then F/.(k+1) in SUCC(F/.k,S) by A69,A73,NAT_1:14;
then l <= l1 by A52,A74;
hence
ex l being Nat st F/.(k+1) = l & m <= l by A75,XXREAL_0:2;
end;
end;
hence P[k+1];
end;
A76: 1 <= len F by NAT_1:14;
A77: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A77, A70);
then ex l being Nat st F/.len F = l & m <= l by A76;
hence thesis by A68;
end;
end;
set III = {[1,{},{}],[0,{},{}]};
begin :: Standard trivial computer
definition
let N be with_zero set;
func STC N -> strict AMI-Struct over N means
:Def7:
the carrier of it = {0} & IC it = 0 &
the InstructionsF of it = {[0,0,0],[1,0,0]} &
the Object-Kind of it = (0 .--> 0) &
the ValuesF of it = N --> NAT &
ex f being Function of product the_Values_of it,
product the_Values_of it st
(for s being Element of product the_Values_of it
holds f.s = s+*(0 .-->(In(s.0,NAT) + 1))) &
the Execution of it = ([1,0,0] .--> f) +*
([0,0,0] .--> id product the_Values_of it);
existence
proof
set O = {0};
set V = N --> NAT;
reconsider IC1 = 0 as Element of O by TARSKI:def 1;
reconsider i = [0,0,0] as Element of III by TARSKI:def 2;
A1: 0 in N by MEASURE6:def 2;
then
A2: V*(0 .-->0) = 0 .--> NAT by FUNCOP_1:89;
then
A3: dom(V*(0 .-->0)) = O;
A4: dom(0 .-->0) = O;
rng(0 .-->0) = {0} by FUNCOP_1:88;
then rng(0 .-->0) c= N by A1,ZFMISC_1:31;
then reconsider Ok = 0 .-->0 as Function of O, N by A4,RELSET_1:4;
deffunc F(Element of product(V*Ok)) = $1+*(0 .-->(In($1.0,NAT) + 1));
A5: now
let s be Element of product(V*Ok);
now
thus dom (s+*(0 .-->(In(s.0,NAT)+1)))
= dom s \/ dom (0 .-->(In(s.0,NAT)+1)) by FUNCT_4:def 1
.= dom s \/ {0}
.= {0} \/ {0} by PARTFUN1:def 2
.= dom(V*Ok) by A3;
let o be object;
A6: dom (0 .-->(In(s.0,NAT)+1)) = {0};
assume
A7: o in dom(V*Ok);
A8: (V*Ok).o = NAT by A7,A2,FUNCOP_1:7;
(s+*(0 .-->(In(s.0,NAT)+1))).o
= (0 .-->(In(s.0,NAT)+1)).o by A6,A7,FUNCT_4:13
.= In(s.0,NAT)+1 by A7,FUNCOP_1:7;
hence (s+*(0 .-->(In(s.0,NAT)+1))).o in (V*Ok).o by A8;
end;
hence F(s) in product(V*Ok) by CARD_3:9;
end;
consider f being Function of product(V*Ok), product(V*Ok) such that
A9: for s being Element of product(V*Ok) holds f.s= F(s) from FUNCT_2:
sch 8 (A5);
set E = ([1,0,0] .--> f) +* ([0,0,0] .--> id product(V*Ok));
A10: dom E = dom ([1,0,0] .--> f) \/ dom ([0,0,0] .--> id product(V*Ok)) by
FUNCT_4:def 1
.= {[1,0,0]} \/ dom ([0,0,0] .--> id product(V*Ok))
.= {[1,0,0]} \/ {[0,0,0]}
.= III by ENUMSET1:1;
A11: rng ([1,0,0] .--> f) c= {f} & rng ([0,0,0] .--> id product(V*Ok)) c= {id
product(V*Ok)} by FUNCOP_1:13;
A12: rng E c= rng ([1,0,0] .--> f) \/ rng ([0,0,0] .--> id product(V*Ok)) by
FUNCT_4:17;
rng E c= Funcs(product(V*Ok), product(V*Ok))
proof
let e be object;
assume e in rng E;
then e in rng ([1,0,0] .--> f) or
e in rng ([0,0,0] .--> id product(V*Ok)) by A12,XBOOLE_0:def 3;
then e = f or e = id product(V*Ok) by A11,TARSKI:def 1;
hence thesis by FUNCT_2:9;
end;
then reconsider E as Function of III, Funcs(product(V*Ok), product(V*Ok))
by A10,FUNCT_2:def 1,RELSET_1:4;
set V = N --> NAT;
set M = AMI-Struct(# O, IC1, III, Ok, V, E#);
take M qua strict AMI-Struct over N;
thus the carrier of M = {0};
thus IC M = 0;
thus the InstructionsF of M = {[0,0,0],[1,0,0]};
thus the Object-Kind of M = (0 .-->0);
thus the ValuesF of M = N --> NAT;
reconsider f as Function of product the_Values_of M,
product the_Values_of M;
take f;
thus for s being Element of product the_Values_of M
holds f.s = s+*(0 .-->(In(s.0,NAT) + 1)) by A9;
thus thesis;
end;
uniqueness
proof
let it1, it2 be strict AMI-Struct over N such that
A13: the carrier of it1 = {0} & IC it1 = 0
& the InstructionsF of it1 = {[0,0,0],[1,0,0]}
and
A14: the Object-Kind of it1 = (0 .-->0) and
A15: the ValuesF of it1 = N --> NAT;
given f1 being Function of product the_Values_of it1,
product the_Values_of it1 such that
A16: for s being Element of product the_Values_of it1 holds f1.s
= s+* (0 .-->(In(s.0,NAT)+1)) and
A17: the Execution of it1 = ([1,0,0] .--> f1) +* ([0,0,0] .--> id product
the_Values_of it1);
assume that
A18: the carrier of it2 = {0} & IC it2 = 0
& the InstructionsF of it2 = {[0,0,0],[1,0,0]} and
A19: the Object-Kind of it2 = (0 .-->0) and
A20: the ValuesF of it2 = N --> NAT;
given f2 being Function of product the_Values_of it2, product
the_Values_of it2 such that
A21: for s being Element of product the_Values_of it2 holds f2.s
= s+* (0 .-->(In(s.0,NAT)+1)) and
A22: the Execution of it2 = ([1,0,0] .--> f2) +* ([0,0,0] .--> id product
the_Values_of it2);
A23: the_Values_of it1 = the_Values_of it2 by A14,A15,A19,A20;
now
let c be Element of product the_Values_of it1;
thus f1.c = c+*(0 .-->(In(c.0,NAT)+1)) by A16
.= f2.c by A21,A23;
end;
hence thesis by A13,A14,A17,A18,A19,A22,A15,A20,FUNCT_2:63;
end;
end;
registration
let N be with_zero set;
cluster STC N -> finite non empty;
coherence by Def7;
end;
registration
let N be with_zero set;
cluster STC N -> with_non-empty_values;
coherence
proof
let n be object;
set S = STC N, F = the_Values_of S;
assume
A1: n in dom F;
then
A2: (the Object-Kind of S).n in dom the ValuesF of S by FUNCT_1:11;
A3: the ValuesF of S = N --> NAT by Def7;
A4: (the Object-Kind of S).n in N by A2;
F.n =(the ValuesF of S).((the Object-Kind of S).n) by A1,FUNCT_1:12
.= NAT by A4,A3,FUNCOP_1:7;
hence F.n is non empty;
end;
end;
registration
let N be with_zero set;
cluster STC N -> IC-Ins-separated;
coherence
proof
set IT = STC N;
set Ok = the_Values_of IT;
A1: 0 in {0} by TARSKI:def 1;
A2: the_Values_of IT = (the ValuesF of IT)*(the Object-Kind of IT)
.= (the ValuesF of IT)*(0.-->0) by Def7
.= (N-->NAT)*(0.-->0) by Def7;
0 in N by MEASURE6:def 2;
then Ok.0 = (0 .-->NAT).0 by A2,FUNCOP_1:89
.= NAT by A1,FUNCOP_1:7;
then Values IC IT = NAT by Def7;
hence STC N is IC-Ins-separated;
end;
end;
Lm3: for i being Instruction of STC N, s being State of STC N st InsCode i = 1
holds Exec(i,s).IC STC N = 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 Def7;
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 Def7;
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 Def7;
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 Def7;
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 Exec(i,s).IC STC N = (s+*(0 .-->(In(s.0,NAT) + 1))).0 by A9,A8
.= (0 .-->(In(s.0,NAT)+1)).0 by A5,FUNCT_4:13
.= In(k,NAT)+1 by A4,FUNCOP_1:7
.= IC s + 1 by A9;
end;
theorem Th4:
for i being Instruction of STC N st InsCode i = 0 holds i is halting
proof
let i be Instruction of STC N;
set M = STC N;
the InstructionsF of M = III by Def7;
then
A1: i = [1,0,0] or i = [0,0,0] by TARSKI:def 2;
assume InsCode i = 0;
then
A2: i in {[0,0,0]} by A1,TARSKI:def 1;
let s be State of M;
reconsider s as Element of product the_Values_of M by CARD_3:107;
(ex f be Function of product the_Values_of M, product
the_Values_of M
st ( for s being Element of product the_Values_of M holds
f.s = s+*(0 .-->(In(s.0,NAT)+1)))&
the Execution of M = ([1,0,0] .--> f) +* ([0,0,0]
.--> id product the_Values_of M) )& dom ([0,0,0] .--> id product
the_Values_of M) = {[0,0,0]} by Def7;
then
(the Execution of M).i = ([0,0,0] .--> id product the_Values_of M).i
by A2,FUNCT_4:13
.= id product the_Values_of M by A2,FUNCOP_1:7;
then (the Execution of M).i.s = s;
hence thesis;
end;
theorem
for i being Instruction of STC N st InsCode i = 1 holds i is non halting
proof
let i be Instruction of STC N;
set M = STC N;
set s =the State of M;
assume InsCode i = 1;
then
A1: Exec(i,s).IC M = IC s + 1 by Lm3;
assume for s being State of M holds Exec(i,s) = s;
then Exec(i,s).IC M = IC s;
hence thesis by A1;
end;
theorem Th6:
for i being Element of the InstructionsF of STC N
holds InsCode i = 1 or InsCode i = 0
proof
let i be Element of the InstructionsF of STC N;
the InstructionsF of STC N = III by Def7;
then i = [1,0,0] or i = [0,0,0] by TARSKI:def 2;
hence thesis;
end;
theorem
for i being Instruction of STC N holds i is jump-only
proof
let i be Instruction of STC N;
set M = STC N;
let s be State of M, o be Object of M, I be Instruction of M such that
InsCode I = InsCode i and
A1: o in Data-Locations M;
A2: IC M = 0 by Def7;
Data-Locations M = ({0}) \ ({0}) by A2,Def7
.= {} by XBOOLE_1:37;
hence thesis by A1;
end;
registration let N;
cluster -> ins-loc-free for Instruction of STC N;
coherence
proof let I be Instruction of STC N;
I in the InstructionsF of STC N;
then I in {[0,0,0],[1,0,0]} by Def7;
then I = [0,0,0] or I = [1,0,0] by TARSKI:def 2;
hence JumpPart I is empty;
end;
end;
Lm4: for l being 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 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
set f = NAT --> i;
set w =the State of M;
reconsider ll=l as Element of NAT by ORDINAL1:def 12;
reconsider l9 = ll as Element of Values IC M by MEMSTR_0:def 6;
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,Lm3;
hence y in {z+1} by TARSKI:def 1;
end;
assume y in {z+1};
then
A5: y = z+1 by TARSKI:def 1;
IC M in dom u by TARSKI:def 1;
then
A6: IC t = u.IC M by FUNCT_4:13
.= z by A1,FUNCOP_1:72;
then IC Following(f,t) = z+1 by A2,Lm3;
hence y in F by A1,A5,A6;
end;
hence thesis by TARSKI:2;
end;
Lm5: for i being Element of the InstructionsF of STC N holds JUMP i is empty
proof
let i be Element of the InstructionsF of STC N;
per cases by Th6;
suppose
A1: InsCode i = 1;
reconsider l1 = 0, l2 = 1 as Nat;
set X = the set of all NIC(i,l) where l is Nat ;
assume not thesis;
then consider x being object such that
A2: x in meet X;
NIC(i, l1) in X;
then {0+1} in X by A1,Lm4;
then x in {1} by A2,SETFAM_1:def 1;
then
A3: x = 1 by TARSKI:def 1;
NIC(i, l2) in X;
then {1+1} in X by A1,Lm4;
then x in {2} by A2,SETFAM_1:def 1;
hence contradiction by A3,TARSKI:def 1;
end;
suppose
A4: InsCode i = 0;
reconsider i as Instruction of STC N;
for l being Nat holds NIC(i,l)={l} by A4,Th2,Th4;
hence thesis by Th1;
end;
end;
theorem Th8:
for l being Nat st l = z holds SUCC(l,STC N) = {z, z+1}
proof
let l be Nat such that
A1: l = z;
set M = STC N;
set K = the set of all
NIC(i,l) \ JUMP i where i is Element of the InstructionsF of STC N;
now
let y be object;
hereby
assume y in K;
then consider ii being Element of the InstructionsF of STC N such that
A2: y = NIC(ii,l) \ JUMP ii and
not contradiction;
reconsider ii as Instruction of STC N;
now
per cases by Th6;
suppose
A3: InsCode ii = 1;
JUMP ii = {} by Lm5;
then y = {z+1} by A1,A2,A3,Lm4;
hence y in {{z},{z+1}} by TARSKI:def 2;
end;
suppose
A4: InsCode ii = 0;
JUMP ii = {} by Lm5;
then y = {z} by A1,A2,A4,Th2,Th4;
hence y in {{z},{z+1}} by TARSKI:def 2;
end;
end;
hence y in {{z},{z+1}};
end;
assume
A5: y in {{z},{z+1}};
per cases by A5,TARSKI:def 2;
suppose
A6: y = {z};
halt M = [0,{},{}];
then reconsider i = [0,0,0] as Instruction of M;
JUMP i = {} & InsCode i = 0 by Lm5;
then NIC(i,l) \ JUMP i = y by A1,A6,Th2,Th4;
hence y in K;
end;
suppose
A7: y = {z+1};
set i = [1,0,0];
i in III by TARSKI:def 2;
then reconsider i as Instruction of M by Def7;
JUMP i = {} & InsCode i = 1 by Lm5;
then NIC(i,l) \ JUMP i = y by A1,A7,Lm4;
hence y in K;
end;
end;
then K = {{z},{z+1}} by TARSKI:2;
hence thesis by ZFMISC_1:26;
end;
registration
let N be with_zero set;
cluster STC N -> standard;
coherence
proof
set M = STC N;
now
let k be Nat;
A1: SUCC(k,STC N) = {k,k+1} by Th8;
thus k+1 in SUCC(k,STC N) by A1,TARSKI:def 2;
let j be Nat;
assume j in SUCC(k,STC N);
then j = k or j = k+1 by A1,TARSKI:def 2;
hence k <= j by NAT_1:11;
end;
hence thesis by Th3;
end;
end;
registration
let N be with_zero set;
cluster STC N -> halting;
coherence
proof
set I = halt STC N;
InsCode I = 0;
hence I is halting by Th4;
end;
end;
registration
let N be with_zero set;
cluster 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 standard IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N;
theorem
for i being Instruction of STC N, s being State of STC N st InsCode i = 1
holds Exec(i,s).IC STC N = IC s + 1 by Lm3;
theorem
for l being Nat, i being Element of the
InstructionsF of STC N st InsCode i = 1 holds NIC(i, l) = {l+1} by Lm4;
theorem
for l being Nat holds SUCC(l,STC N) = {l, l + 1} by Th8;
definition
let N be with_zero set,
S be 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 = IC s + 1;
end;
theorem Th12:
for S being IC-Ins-separated non empty with_non-empty_values
AMI-Struct over N,
il being Nat, i being Instruction of S st i is sequential
holds NIC(i,il) = {il + 1}
proof
let S be IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
il be Nat, i be
Instruction of S such that
A1: for s being State of S holds Exec(i, s).IC S = IC s + 1;
now
let x be object;
A2: now
reconsider ll = il as Element of NAT by ORDINAL1:def 12;
reconsider il1 = ll 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 = il+1;
reconsider u = t+*(IC S,il1) as
Element of product the_Values_of S by CARD_3:107;
ll in NAT;
then
A4: il in dom P by PARTFUN1:def 2;
A5: (P+*(il,i))/.ll = (P+*(il,i)).ll 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) = il + 1 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 = il + 1 by A1;
end;
hence
x in {il+1} 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;
registration
let N;
let S be IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
cluster sequential -> non halting for Instruction of S;
coherence
proof
let i be Instruction of S such that
A1: i is sequential;
set s =the State of S;
A2: IC s + 1 <> IC s + 0;
NIC(i,IC s) = {IC s + 1} by A1,Th12;
then NIC(i,IC s) <> {IC s} by ZFMISC_1:3,A2;
hence thesis by Th2;
end;
cluster halting -> non sequential for Instruction of S;
coherence;
end;
theorem
for T being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N
for i being Instruction of T st JUMP i is non empty holds i is non
sequential
proof
let T be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;
let i be Instruction of T;
set X = the set of all NIC(i,l1) where l1 is Nat;
assume JUMP i is non empty;
then consider l being object such that
A1: l in JUMP i;
reconsider l as Nat by A1;
NIC(i,l) in X;
then l in NIC(i,l) by A1,SETFAM_1:def 1;
then consider s being Element of product the_Values_of T
such that
A2: l = IC Exec(i,s) & IC s = l;
take s;
thus thesis by A2;
end;
begin :: Closedness of finite partial states
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 finite preProgram of S;
attr F is really-closed means
for l being Nat st l in dom F holds NIC (F/.l, l) c= dom F;
end;
::$CD
definition
let N be with_zero set;
let S be halting 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 parahalting means
for s being 0-started State of S
for P being Instruction-Sequence of S st F c= P
holds P halts_on s;
end;
theorem Th14:
for N being with_zero set
for S being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N
for F being finite preProgram of S
holds F is really-closed iff
for s being State of S st IC s in dom F
for k being Nat holds IC Comput(F,s,k) in dom F
proof 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 finite preProgram of S;
thus F is really-closed implies
for s being State of S st IC s in dom F
for k being Nat holds IC Comput(F,s,k) in dom F
proof assume
A1: F is really-closed;
let s be State of S such that
A2: IC s in dom F;
defpred P[Nat] means IC Comput(F,s,$1) in dom F;
A3: now
let k be Nat such that
A4: P[k];
reconsider t = Comput(F,s,k)
as Element of product the_Values_of S by CARD_3:107;
set l = IC Comput(F,s,k);
A5: IC Following(F,t) in NIC(F/.l,l);
A6: Comput(F,s,k+1) = Following(F,t) by EXTPRO_1:3;
NIC(F/.l, l) c= dom F by A1,A4;
hence P[k+1] by A5,A6;
end;
A7: P[0] by A2;
thus for k being Nat holds P[k] from NAT_1:sch 2(A7,A3);
end;
assume
A8: for s being State of S st IC s in dom F
for k being Nat holds IC Comput(F,s,k) in dom F;
let l being Nat such that
A9: l in dom F;
let x be object;
assume x in NIC(F/.l, l);
then consider ss being Element of product the_Values_of S
such that
A10: x = IC Exec(F/.l,ss) and
A11: IC ss = l;
reconsider ss as State of S;
IC Comput(F,ss,0+1) = IC Following(F,Comput(F,ss,0)) by EXTPRO_1:3
.= IC Following(F,ss)
.= IC Exec(F/.IC ss,ss);
hence x in dom F by A10,A11,A8,A9;
end;
Lm6:
for N being with_zero set
for S being IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N
for F being finite preProgram of S
holds F is really-closed iff
for s being State of S st IC s in dom F
for P being Instruction-Sequence of S st F c= P
for k being Nat holds IC Comput(P,s,k) in dom F
proof 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 finite preProgram of S;
thus F is really-closed implies
for s being State of S st IC s in dom F
for P being Instruction-Sequence of S st F c= P
for k being Nat holds IC Comput(P,s,k) in dom F
proof assume
A1: F is really-closed;
let s be State of S such that
A2: IC s in dom F;
let P be Instruction-Sequence of S such that
A3: F c= P;
defpred P[Nat] means IC Comput(P,s,$1) in dom F;
A4: now
let k be Nat such that
A5: P[k];
reconsider t = Comput(P,s,k)
as Element of product the_Values_of S by CARD_3:107;
set l = IC Comput(P,s,k);
A6: IC Following(P,t) in NIC(P/.l,l);
A7: Comput(P,s,k+1) = Following(P,t) by EXTPRO_1:3;
P/.l = F/.l by A5,A3,PARTFUN2:61;
then NIC(P/.l, l) c= dom F by A1,A5;
hence P[k+1] by A6,A7;
end;
A8: P[0] by A2;
thus for k being Nat holds P[k] from NAT_1:sch 2(A8,A4);
end;
assume
A9: for s being State of S st IC s in dom F
for P being Instruction-Sequence of S st F c= P
for k being Nat holds IC Comput(P,s,k) in dom F;
for s being State of S st IC s in dom F
for k being Nat holds IC Comput(F,s,k) in dom F
proof let s be State of S such that
A10: IC s in dom F;
consider P being Instruction-Sequence of S such that
A11: F c= P by PBOOLE:145;
let k be Nat;
A12: IC Comput(P,s,k) in dom F by A9,A10,A11;
defpred P[Nat] means Comput(P,s,$1) = Comput(F,s,$1);
A13: P[0];
A14: for k being Nat st P[k] holds P[k+1]
proof let k be Nat;
assume
A15: P[k];
reconsider kk = k as Nat;
A16: IC Comput(P,s,kk) in dom F by A9,A10,A11;
Comput(P,s,k+1) = Following(P,Comput(F,s,k)) by A15,EXTPRO_1:3
.= Following(F,Comput(F,s,k)) by A16,A11,A15,PARTFUN2:61
.= Comput(F,s,k+1) by EXTPRO_1:3;
hence P[k+1];
end;
for k being Nat holds P[k] from NAT_1:sch 2(A13,A14);
hence IC Comput(F,s,k) in dom F by A12;
end;
hence thesis by Th14;
end;
registration let N;
let S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
cluster Stop S -> really-closed;
coherence
proof set F = Stop S;
let l be Nat;
assume
A1: l in dom F;
A3: l = 0 by A1,TARSKI:def 1;
F/.l = F.l by A1,PARTFUN1:def 6
.= halt S by A3;
hence thesis by A3,Th2;
end;
end;
::$CT 2
registration
let N be with_zero set;
let S be standard halting IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N;
cluster really-closed trivial for MacroInstruction of S;
existence
proof
take F = Stop S;
thus thesis;
end;
end;
theorem
for i being Instruction of Trivial-AMI(N) holds i is halting
proof
let i be Instruction of Trivial-AMI(N);
set M = Trivial-AMI(N);
A1: the InstructionsF of M = {[0,{},{}]} by EXTPRO_1:def 1;
let s be State of M;
reconsider s as Element of product the_Values_of M by CARD_3:107;
A2: the Object-Kind of M = 0 .--> 0 &
the ValuesF of M = N --> NAT by EXTPRO_1:def 1;
(the Execution of M).i = ([0,{},{}] .--> id product the_Values_of M).i
by A2,EXTPRO_1:def 1
.= id product the_Values_of M by A1;
then (the Execution of M).i.s = s;
hence thesis;
end;
theorem
for i being Element of the InstructionsF of Trivial-AMI N holds InsCode i = 0
proof
let i be Element of the InstructionsF of Trivial-AMI(N);
the InstructionsF of Trivial-AMI(N) = {[0,{},{}]} by EXTPRO_1:def 1;
then i = [0,{},{}] by TARSKI:def 1;
hence thesis;
end;
begin :: Addenda
:: from SCMPDS_9, 2008.03.10, A.T.
theorem
for N being with_zero set, S
being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N,
i being Instruction of S, l being Nat
holds JUMP(i) c= NIC(i,l)
proof
let N be with_zero set,
S be IC-Ins-separated non
empty with_non-empty_values AMI-Struct over N, i be Instruction of S, l be
Nat;
set X = the set of all NIC(i,k) where k is Nat;
let x be object;
A1: NIC(i,l) in X;
assume x in JUMP(i);
hence thesis by A1,SETFAM_1:def 1;
end;
theorem
for i being Instruction of STC N, s being State of STC N st InsCode i = 1
holds Exec(i,s) = IncIC(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 Def7;
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;
consider f be Function of product the_Values_of M, product
the_Values_of M such that
A4: for s being Element of product the_Values_of M
holds f.s = s+*(0 .-->(In(s.0,NAT)+1)) and
A5: the Execution of M = ([1,0,0] .--> f) +* ([0,0,0] .--> id product
the_Values_of M) by Def7;
A6: 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 A4;
hence thesis;
end;
A7: IC M = 0 by Def7;
A8: 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 Def7;
then
A9: 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 A8,A9,CARD_3:9,A7;
A10: Start-At(IC s+1,M) = 0 .-->(In(k,NAT)+1) by A7;
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 A5,A2,FUNCT_4:11
.= f by A3,FUNCOP_1:7;
hence Exec(i,s) = IncIC(s,1) by A10,A6;
end;
registration let N; let p be PartState of STC N;
cluster DataPart p -> empty;
coherence
proof
Data-Locations STC N
= (the carrier of STC N) \ ({0}) by Def7
.= ({0}) \ ({0}) by Def7
.= {} by XBOOLE_1:37;
hence thesis;
end;
end;
theorem
for N being with_zero set
for S being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N
for F being finite preProgram of S
holds F is really-closed iff
for s being State of S st IC s in dom F
for P being Instruction-Sequence of S st F c= P
for k being Nat holds IC Comput(P,s,k) in dom F by Lm6;
registration
let N be with_zero set;
let S be halting IC-Ins-separated non empty with_non-empty_values
AMI-Struct over N;
cluster parahalting
for finite non halt-free non empty
NAT-defined (the InstructionsF of S)-valued Function;
existence
proof
take Stop S;
let s be 0-started State of S;
let P be Instruction-Sequence of S such that
A1: Stop S c= P;
take 0;
A2: 0 in dom Stop S by COMPOS_1:3;
dom Stop S c= dom P by A1,RELAT_1:11;
then
A3: 0 in dom P by A2;
A4: IC s = 0 by MEMSTR_0:def 11;
hence IC Comput(P,s,0) in dom P by A3;
thus CurInstr(P,Comput(P,s,0))
= P/.0 by A4
.= P.0 by A3,PARTFUN1:def 6
.= (Stop S).0 by A1,A2,GRFUNC_1:2
.= halt S;
end;
end;