Copyright (c) 1992 Association of Mizar Users
environ
vocabulary INT_1, BOOLE, FUNCT_2, FUNCT_1, RELAT_1, FUNCOP_1, CAT_1, FUNCT_4,
CARD_3, TARSKI, FRAENKEL, FUNCT_3, PARTFUN1, FINSET_1, AMI_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, CARD_3,
RELAT_1, FUNCT_1, FUNCT_2, FINSET_1, NAT_1, CQC_LANG, FRAENKEL, FUNCOP_1,
FUNCT_4, FINSEQ_1, FUNCT_3, PARTFUN1, STRUCT_0;
constructors CARD_3, NAT_1, CQC_LANG, CAT_2, INT_2, PARTFUN1, STRUCT_0,
MEMBERED, XBOOLE_0;
clusters SUBSET_1, FUNCT_1, INT_1, FRAENKEL, RELAT_1, FINSET_1, RELSET_1,
FINSEQ_1, FUNCOP_1, FUNCT_4, CQC_LANG, STRUCT_0, XBOOLE_0, FUNCT_2,
MEMBERED, ZFMISC_1, ORDINAL2;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, FRAENKEL, STRUCT_0, XBOOLE_0;
theorems ZFMISC_1, FUNCT_2, TARSKI, NAT_1, CQC_LANG, CARD_3, CARD_5, FINSEQ_1,
FUNCT_4, FUNCOP_1, FRAENKEL, FINSET_1, PARTFUN1, FUNCT_1, GRFUNC_1,
FUNCT_3, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, NUMBERS;
schemes NAT_1, RECDEF_1, FRAENKEL, XBOOLE_0;
begin :: Preliminaries
reserve x for set;
theorem
NAT <> INT by NUMBERS:27;
theorem Th2:
for a,b being set holds 1 <> [a,b]
proof let a,b be set;
A1: 1 = { {} } & [a,b] = {{a,b},{a}} by CARD_5:1,TARSKI:def 5;
assume 1 = [a,b];
hence contradiction by A1,ZFMISC_1:8;
end;
theorem
for a,b being set holds 2 <> [a,b]
proof let a,b be set;
A1: 2 = { {}, {{}} } & [a,b] = {{a,b},{a}} by CARD_5:1,TARSKI:def 5;
assume 2 = [a,b];
hence contradiction by A1,ZFMISC_1:10;
end;
canceled;
theorem Th5:
for a,b,c,d being set st a <> b holds
product (a,b) --> ({c},{d}) = { (a,b) --> (c,d) }
proof let a,b,c,d be set such that
A1: a <> b;
set X = { (a,b) --> (c,d) },
f = (a,b) --> ({c},{d});
A2: dom f = {a,b} by FUNCT_4:65;
now let x;
thus x in X implies ex g being Function st x = g & dom g = dom f &
for x st x in dom f holds g.x in f.x
proof assume
A3: x in X;
take g = (a,b) --> (c,d);
thus x = g by A3,TARSKI:def 1;
thus dom g = dom f by A2,FUNCT_4:65;
let x;
assume x in dom f;
then A4: x = a or x = b by A2,TARSKI:def 2;
g.a = c & f.a = {c} & g.b = d & f.b = {d} by A1,FUNCT_4:66;
hence g.x in f.x by A4,TARSKI:def 1;
end;
given g being Function such that
A5: x = g and
A6: dom g = dom f and
A7: for x st x in dom f holds g.x in f.x;
a in dom f & b in dom f by A2,TARSKI:def 2;
then g.a in f.a & g.b in f.b & f.a = {c} & f.b = {d} by A1,A7,FUNCT_4:66;
then g.a = c & g.b = d by TARSKI:def 1;
then g = (a,b) --> (c,d) by A2,A6,FUNCT_4:69;
hence x in X by A5,TARSKI:def 1;
end;
hence product (a,b) --> ({c},{d}) = { (a,b) --> (c,d) } by CARD_3:def 5;
end;
definition let IT be set;
attr IT is with_non-empty_elements means
:Def1: not {} in IT;
end;
definition
cluster non empty with_non-empty_elements set;
existence
proof
take {{{}}};
thus {{{}}} is non empty;
assume {} in {{{}}};
hence contradiction by TARSKI:def 1;
end;
end;
definition
let A be non empty set;
cluster { A } -> with_non-empty_elements;
coherence
proof
{ A } is with_non-empty_elements
proof
assume {} in { A };
hence contradiction by TARSKI:def 1;
end;
hence thesis;
end;
let B be non empty set;
cluster { A, B } -> with_non-empty_elements;
coherence
proof
{ A, B } is with_non-empty_elements
proof
assume {} in { A,B };
hence contradiction by TARSKI:def 2;
end;
hence thesis;
end;
end;
definition let A,B be with_non-empty_elements set;
cluster A \/ B -> with_non-empty_elements;
coherence
proof
A \/ B is with_non-empty_elements
proof
not {} in A & not {} in B by Def1;
hence not {} in A \/ B by XBOOLE_0:def 2;
end;
hence thesis;
end;
end;
begin :: General concepts
reserve N for with_non-empty_elements set;
definition let N be set;
struct (1-sorted) AMI-Struct over N
(# carrier -> set,
Instruction-Counter -> Element of the carrier,
Instruction-Locations -> Subset of the carrier,
Instruction-Codes -> non empty set,
Instructions -> non empty Subset of
[: the Instruction-Codes, ((union N) \/ the carrier)* :],
Object-Kind ->
Function of the carrier,
N \/ { the Instructions, the Instruction-Locations },
Execution ->
Function of the Instructions,
Funcs(product the Object-Kind, product the Object-Kind)
#);
end;
definition let N be set;
func Trivial-AMI N -> strict AMI-Struct over N means
:Def2:
the carrier of it = {0,1} &
the Instruction-Counter of it = 0 &
the Instruction-Locations of it = {1} &
the Instruction-Codes of it = {0} &
the Instructions of it = {[0,{}]} &
the Object-Kind of it = (0,1) --> ({1},{[0,{}]}) &
the Execution of it = {[0,{}]} --> id product (0,1) --> ({1},{[0,{}]});
existence
proof
reconsider y = 0 as Element of {0,1}by TARSKI:def 2;
0 in {0} & {} in (union N \/ {0,1})* by FINSEQ_1:66,TARSKI:def 1;
then [0,{}] in [: {0}, (union N \/ {0,1})* :] by ZFMISC_1:106;
then reconsider I = {[0,{}]} as non empty Subset of
[: {0}, (union(N) \/ {0,1})* :] by ZFMISC_1:37;
reconsider S = {1} as non empty Subset of {0,1} by ZFMISC_1:12;
set f = (0,1) --> (S,I);
rng f c= { I,S} & { I,S } c= N \/ {I, S} by FUNCT_4:65,XBOOLE_1:7;
then dom f = {0,1} & rng f c= N \/ {I, S} by FUNCT_4:65,XBOOLE_1:1;
then reconsider f as Function of {0,1}, N \/ {I, S} by FUNCT_2:def 1,
RELSET_1:11;
id product f in Funcs(product f, product f) by FUNCT_2:12;
then reconsider E = I --> id product f as
Function of I,Funcs(product f, product f) by FUNCOP_1:57;
take AMI-Struct(#{0,1},y,S,{0},I,f,E #);
thus thesis;
end;
uniqueness;
end;
definition let N be set; let S be AMI-Struct over N;
attr S is void means
:Def3: the Instruction-Locations of S is empty;
end;
definition let N be set;
cluster Trivial-AMI N -> non empty non void;
coherence
proof
thus the carrier of Trivial-AMI N is non empty by Def2;
thus the Instruction-Locations of Trivial-AMI N is non empty by Def2;
end;
end;
definition let N be set;
cluster non empty non void AMI-Struct over N;
existence
proof
take Trivial-AMI N;
thus thesis;
end;
end;
definition let N be set; let S be non empty AMI-Struct over N;
cluster the carrier of S -> non empty;
coherence;
end;
definition let N be set; let S be non void AMI-Struct over N;
cluster the Instruction-Locations of S -> non empty;
coherence by Def3;
end;
definition let N be set; let S be non empty AMI-Struct over N;
mode Object of S is Element of S;
end;
definition let N be set; let S be non empty non void AMI-Struct over N;
mode Instruction-Location of S is Element of the Instruction-Locations of S;
end;
definition let N be set; let S be AMI-Struct over N;
mode Instruction of S is Element of the Instructions of S;
canceled;
end;
definition let N be set; let S be non empty AMI-Struct over N;
func IC S -> Object of S equals
:Def5: the Instruction-Counter of S;
correctness;
end;
definition let N be set; let S be non empty AMI-Struct over N;
let o be Object of S;
func ObjectKind o ->
Element of N \/ { the Instructions of S, the Instruction-Locations of S }
equals
:Def6: (the Object-Kind of S).o;
correctness;
end;
definition let f be Function;
cluster product f -> functional;
coherence
proof
set d = product f;
let x be set; assume x in d;
then ex g being Function
st x = g & dom g= dom f & for x being set st x in dom f holds g.x in f.x
by CARD_3:def 5;
hence x is Function;
end;
end;
definition let A be set; let B be with_non-empty_elements set;
let f be Function of A,B;
cluster product f -> non empty;
coherence
proof
rng f c= B by RELSET_1:12;
then not {} in rng f by Def1;
hence thesis by CARD_3:37;
end;
end;
definition let N be set; let S be AMI-Struct over N;
mode State of S is Element of product the Object-Kind of S;
end;
definition let N be with_non-empty_elements set;
let S be non void AMI-Struct over N;
let I be Instruction of S, s be State of S;
func Exec(I,s) -> State of S equals
((the Execution of S).I).s;
coherence
proof
consider f being Function such that
A1: (the Execution of S).I = f &
dom f = product the Object-Kind of S &
rng f c= product the Object-Kind of S by FUNCT_2:def 2;
(the Execution of S).I.s in rng f by A1,FUNCT_1:def 5;
hence thesis by A1;
end;
end;
definition let N; let S be non void AMI-Struct over N;
let I be Instruction of S;
attr I is halting means
:Def8: for s being State of S holds Exec(I,s) = s;
end;
definition let N; let S be non void AMI-Struct over N;
attr S is halting means
:Def9: ex I being Instruction of S st I is halting &
for J being Instruction of S st J is halting holds I = J;
end;
reserve E for set;
theorem Th6:
Trivial-AMI N is halting
proof
set T = Trivial-AMI N;
A1:{[0,{}]} = the Instructions of T by Def2;
then reconsider I = [0,{}] as Instruction of T by TARSKI:def 1;
take I;
thus I is halting
proof
let s be State of T;
A2: product the Object-Kind of T
= product (0,1) --> ({1},{[0,{}]}) by Def2
.= { (0,1) --> (1,[0,{}]) } by Th5;
hence Exec(I,s) = (0,1) --> (1,[0,{}]) by TARSKI:def 1
.= s by A2,TARSKI:def 1;
end;
let J be Instruction of T such that J is halting;
thus I = J by A1,TARSKI:def 1;
end;
definition let N;
cluster Trivial-AMI N -> halting;
coherence by Th6;
end;
definition let N;
cluster halting (non void AMI-Struct over N);
existence
proof
take Trivial-AMI N;
thus thesis;
end;
end;
definition let N; let S be halting (non void AMI-Struct over N);
func halt S -> Instruction of S means
:Def10: ex I being Instruction of S st I is halting & it = I;
existence
proof
consider I being Instruction of S such that
A1: I is halting and
for J being Instruction of S st J is halting holds I = J by Def9;
take I;
thus thesis by A1;
end;
uniqueness
proof
let I1, I2 be Instruction of S such that
A2: ex I being Instruction of S st I is halting & I1 = I and
A3: ex I being Instruction of S st I is halting & I2 = I;
consider Ia being Instruction of S such that
A4: Ia is halting & I1 = Ia by A2;
consider Ib being Instruction of S such that
A5: Ib is halting & I2 = Ib by A3;
consider I being Instruction of S such that
A6: I is halting &
for J being Instruction of S st J is halting holds I = J by Def9;
I = Ia by A4,A6;
hence thesis by A4,A5,A6;
end;
end;
Lm1:
now let N; let S be halting (non void AMI-Struct over N);
thus halt S is halting
proof
ex I being Instruction of S st I is halting & halt S = I by Def10;
hence thesis;
end;
end;
definition let N; let S be halting (non void AMI-Struct over N);
cluster halt S -> halting;
coherence by Lm1;
end;
definition let N be set; let IT be non empty AMI-Struct over N;
attr IT is IC-Ins-separated means
:Def11: ObjectKind IC IT = the Instruction-Locations of IT;
end;
definition let N be set; let IT be AMI-Struct over N;
attr IT is data-oriented means
(the Object-Kind of IT)"{ the Instructions of IT }
c= the Instruction-Locations of IT;
end;
definition let N be with_non-empty_elements set;
let IT be non empty non void AMI-Struct over N;
attr IT is steady-programmed means
:Def13: for s being State of IT, i being Instruction of IT,
l being Instruction-Location of IT
holds Exec(i,s).l = s.l;
end;
definition let N be set; let IT be non empty non void AMI-Struct over N;
attr IT is definite means
:Def14: for l being Instruction-Location of IT holds
ObjectKind l = the Instructions of IT;
end;
theorem Th7:
Trivial-AMI E is IC-Ins-separated
proof
A1: IC Trivial-AMI E = the Instruction-Counter of Trivial-AMI E by Def5
.= 0 by Def2;
thus ObjectKind IC Trivial-AMI E
= (the Object-Kind of Trivial-AMI E).IC Trivial-AMI E by Def6
.= (0,1) --> ({1},{[0,{}]}).0 by A1,Def2
.= {1} by FUNCT_4:66
.= the Instruction-Locations of Trivial-AMI E by Def2;
end;
theorem Th8:
Trivial-AMI E is data-oriented
proof let x be set;
A1: 1 <> [0,{}] by Th2;
assume
A2: x in (the Object-Kind of Trivial-AMI E)"
{ the Instructions of Trivial-AMI E };
then x in the carrier of Trivial-AMI E &
(the Object-Kind of Trivial-AMI E).x in
{ the Instructions of Trivial-AMI E } by FUNCT_2:46;
then A3: (the Object-Kind of Trivial-AMI E).x =
the Instructions of Trivial-AMI E by TARSKI:def 1
.= {[0,{}]} by Def2;
A4: (the Object-Kind of Trivial-AMI E).0 =
(0,1) --> ({1},{[0,{}]}).0 by Def2
.= {1} by FUNCT_4:66;
the carrier of Trivial-AMI E = {0,1} by Def2;
then x = 0 or x = 1 by A2,TARSKI:def 2;
then x in {1} by A1,A3,A4,TARSKI:def 1,ZFMISC_1:6;
hence x in the Instruction-Locations of Trivial-AMI E by Def2;
end;
theorem Th9:
for s1, s2 being State of Trivial-AMI E holds s1=s2
proof let s1,s2 be State of Trivial-AMI E;
A1: product the Object-Kind of Trivial-AMI E
= product (0,1) --> ({1},{[0,{}]}) by Def2
.= { (0,1) --> (1,[0,{}]) } by Th5;
hence s1 = (0,1) --> (1,[0,{}]) by TARSKI:def 1
.= s2 by A1,TARSKI:def 1;
end;
theorem Th10:
Trivial-AMI N is steady-programmed
proof
let s be State of Trivial-AMI N, i be Instruction of Trivial-AMI N,
l be Instruction-Location of Trivial-AMI N;
thus Exec(i,s).l = s.l by Th9;
end;
theorem Th11:
Trivial-AMI E is definite
proof let l be Instruction-Location of Trivial-AMI E;
l in the Instruction-Locations of Trivial-AMI E;
then l in {1} by Def2;
then A1: l = 1 by TARSKI:def 1;
thus ObjectKind l
= (the Object-Kind of Trivial-AMI E).l by Def6
.= (0,1) --> ({1},{[0,{}]}).1 by A1,Def2
.= {[0,{}]} by FUNCT_4:66
.= the Instructions of Trivial-AMI E by Def2;
end;
definition let E be set;
cluster Trivial-AMI E -> data-oriented;
coherence by Th8;
end;
definition let E be set;
cluster Trivial-AMI E -> IC-Ins-separated definite;
coherence by Th7,Th11;
end;
definition let N be with_non-empty_elements set;
cluster Trivial-AMI N -> steady-programmed;
coherence by Th10;
end;
definition let E be set;
cluster data-oriented strict AMI-Struct over E;
existence
proof
take Trivial-AMI E;
thus thesis;
end;
end;
definition let M be set;
cluster IC-Ins-separated data-oriented definite strict
(non empty non void AMI-Struct over M);
existence
proof
take Trivial-AMI M;
thus thesis;
end;
end;
definition let N;
cluster IC-Ins-separated data-oriented halting steady-programmed definite
strict (non empty non void AMI-Struct over N);
existence
proof
take Trivial-AMI N;
thus thesis;
end;
end;
definition let N be with_non-empty_elements set;
let S be IC-Ins-separated (non empty non void AMI-Struct over N);
let s be State of S;
func IC s -> Instruction-Location of S equals
:Def15: s.IC S;
coherence
proof
dom the Object-Kind of S = the carrier of S by FUNCT_2:def 1;
then pi(product the Object-Kind of S,IC S) = (the Object-Kind of S).IC S
by CARD_3:22
.= ObjectKind IC S by Def6
.= the Instruction-Locations of S by Def11;
hence thesis by CARD_3:def 6;
end;
end;
begin :: Preliminaries
reserve x,y,z,A,B for set,
f,g,h for Function,
i,j,k for Nat;
canceled;
theorem Th13:
for f being Function holds pr1(dom f,rng f).:f = dom f
proof let f be Function;
now let y be set;
thus y in dom f implies
ex x being set st x in dom pr1(dom f,rng f) & x in f &
y = pr1(dom f,rng f).x
proof assume
A1: y in dom f;
then A2: f.y in rng f by FUNCT_1:def 5;
take [y,f.y];
[y,f.y] in [:dom f,rng f:] by A1,A2,ZFMISC_1:106;
hence [y,f.y] in dom pr1(dom f,rng f) by FUNCT_3:def 5;
thus [y,f.y] in f by A1,FUNCT_1:def 4;
thus y = pr1(dom f,rng f).[y,f.y] by A1,A2,FUNCT_3:def 5;
end;
given x being set such that
A3: x in dom pr1(dom f,rng f) and
x in f and
A4: y = pr1(dom f,rng f).x;
dom pr1(dom f,rng f) = [:dom f, rng f:] by FUNCT_3:def 5;
then consider x1,x2 being set such that
A5: x1 in dom f and
A6: x2 in rng f and
A7: x = [x1,x2] by A3,ZFMISC_1:103;
thus y in dom f by A4,A5,A6,A7,FUNCT_3:def 5;
end;
hence pr1(dom f,rng f).:f = dom f by FUNCT_1:def 12;
end;
theorem Th14:
f tolerates g & [x,y] in f & [x,z] in g implies y = z
proof assume f tolerates g;
then consider h such that
A1: h = f \/ g by PARTFUN1:130;
assume [x,y] in f & [x,z] in g;
then [x,y] in h & [x,z] in h by A1,XBOOLE_0:def 2;
hence y = z by FUNCT_1:def 1;
end;
theorem Th15:
(for x st x in A holds x is Function) &
(for f,g being Function st f in A & g in A holds f tolerates g)
implies union A is Function
proof assume that
A1: for x st x in A holds x is Function and
A2: for f,g being Function st f in A & g in A holds f tolerates g;
A3: now let z;
assume z in union A;
then consider p being set such that
A4: z in p & p in A by TARSKI:def 4;
reconsider p as Function by A1,A4;
p = p;
hence ex x,y st [x,y] = z by A4,RELAT_1:def 1;
end;
now let x,y,z; assume
A5: [x,y] in union A & [x,z] in union A;
then consider p being set such that
A6: [x,y] in p & p in A by TARSKI:def 4;
consider q being set such that
A7: [x,z] in q & q in A by A5,TARSKI:def 4;
reconsider p,q as Function by A1,A6,A7;
p tolerates q by A2,A6,A7;
hence y = z by A6,A7,Th14;
end;
hence union A is Function by A3,FUNCT_1:def 1,RELAT_1:def 1;
end;
theorem Th16:
dom f c= A \/ B implies f|A +* f|B = f
proof
A1:dom(f|A) = dom f /\ A & dom(f|B) = dom f /\ B by RELAT_1:90;
assume dom f c= A \/ B;
then A2: dom f = dom f /\ (A \/ B) by XBOOLE_1:28
.= dom(f|A) \/ dom(f|B) by A1,XBOOLE_1:23;
x in dom(f|A) \/ dom(f|B) implies
(x in dom(f|B) implies f.x = f|B.x) &
(not x in dom(f|B) implies f.x = f|A.x)
proof
assume
A3: x in dom(f|A) \/ dom(f|B);
thus x in dom(f|B) implies f.x = f|B.x by FUNCT_1:70;
assume not x in dom(f|B);
then x in dom(f|A) by A3,XBOOLE_0:def 2;
hence f.x = f|A.x by FUNCT_1:70;
end;
hence f|A +* f|B = f by A2,FUNCT_4:def 1;
end;
canceled;
theorem Th18:
for x1,x2,y1,y2 being set holds
(x1,x2)-->(y1,y2) = (x1 .--> y1) +* (x2 .--> y2)
proof let x1,x2,y1,y2 be set;
(x1 .--> y1) = {x1} --> y1 & (x2 .--> y2) = {x2} --> y2 by CQC_LANG:def 2;
hence (x1,x2)-->(y1,y2) = (x1 .--> y1) +* (x2 .--> y2) by FUNCT_4:def 4;
end;
theorem Th19:
for x,y holds x .--> y = {[x,y]}
proof let x,y;
thus x .--> y = ({x} --> y) by CQC_LANG:def 2
.= [:{x},{y}:] by FUNCOP_1:def 2
.= {[x,y]} by ZFMISC_1:35;
end;
theorem Th20:
for a,b,c being set holds (a,a) --> (b,c) = a .--> c
proof let a,b,c be set;
A1: dom({a} -->c) = {a} by FUNCOP_1:19
.= dom({a} -->b) by FUNCOP_1:19;
thus (a,a) --> (b,c) = ({a} --> b) +* ({a} -->c) by FUNCT_4:def 4
.= {a} -->c by A1,FUNCT_4:20
.= a .--> c by CQC_LANG:def 2;
end;
theorem Th21:
for f being Function holds dom f is finite iff f is finite
proof let f be Function;
thus dom f is finite implies f is finite
proof assume
A1: dom f is finite;
then rng f is finite by FINSET_1:26;
then A2: [:dom f, rng f:] is finite by A1,FINSET_1:19;
f c= [:dom f, rng f:] by RELAT_1:21;
hence f is finite by A2,FINSET_1:13;
end;
pr1(dom f,rng f).:f = dom f by Th13;
hence thesis by FINSET_1:17;
end;
theorem
x in product f implies x is Function
proof assume x in product f;
then ex g st x = g & dom g = dom f &
for x st x in dom f holds g.x in f.x by CARD_3:def 5;
hence x is Function;
end;
begin :: Superproducts
definition let f be Function;
func sproduct f -> set means
:Def16: x in it iff ex g st x = g & dom g c= dom f &
for x st x in dom g holds g.x in f.x;
existence
proof
defpred _P[set] means ex g st $1 = g & dom g c= dom f &
for x st x in dom g holds g.x in f.x;
consider A being set such that
A1:x in A iff x in
PFuncs(dom f, union rng f) & _P[x] from Separation;
now let x;
thus x in A implies ex g st x = g & dom g c= dom f &
for x st x in dom g holds g.x in f.x by A1;
given g such that
A2: x = g & dom g c= dom f &
for x st x in dom g holds g.x in f.x;
rng g c= union rng f
proof let y be set;
assume y in rng g;
then consider z being set such that
A3: z in dom g & y = g.z by FUNCT_1:def 5;
A4: g.z in f.z by A2,A3;
f.z in rng f by A2,A3,FUNCT_1:def 5;
hence y in union rng f by A3,A4,TARSKI:def 4;
end;
then x in PFuncs(dom f, union rng f) by A2,PARTFUN1:def 5;
hence x in A by A1,A2;
end;
hence thesis;
end;
uniqueness
proof defpred _P[set] means ex g st $1 = g & dom g c= dom f &
for x st x in dom g holds g.x in f.x;
let A,B be set such that
A5: x in A iff _P[x] and A6: x in B iff _P[x];
thus thesis from Extensionality(A5,A6);
end;
end;
definition let f be Function;
cluster sproduct f -> functional non empty;
coherence
proof
defpred _P[set] means ex g st $1 = g & dom g c= dom f &
for x st x in dom g holds g.x in f.x;
consider A being set such that
A1:x in A iff x in PFuncs(dom f, union rng f) & _P[x] from Separation;
{} is PartFunc of dom f, union rng f by PARTFUN1:56;
then A2:{} in PFuncs(dom f, union rng f) by PARTFUN1:119;
dom {} c= dom f & for x st x in dom {} holds {} .x in f.x by XBOOLE_1:2;
then reconsider A as non empty set by A1,A2;
now let x be set;
assume x in A;
then ex g st x = g & dom g c= dom f &
for x st x in dom g holds g.x in f.x by A1;
hence x is Function;
end;
then reconsider A as functional non empty set by FRAENKEL:def 1;
now let x;
thus x in A implies ex g st x = g & dom g c= dom f &
for x st x in dom g holds g.x in f.x by A1;
given g such that
A3: x = g & dom g c= dom f &
for x st x in dom g holds g.x in f.x;
rng g c= union rng f
proof let y be set;
assume y in rng g;
then consider z being set such that
A4: z in dom g & y = g.z by FUNCT_1:def 5;
A5: g.z in f.z by A3,A4;
f.z in rng f by A3,A4,FUNCT_1:def 5;
hence y in union rng f by A4,A5,TARSKI:def 4;
end;
then x in PFuncs(dom f, union rng f) by A3,PARTFUN1:def 5;
hence x in A by A1,A3;
end;
hence thesis by Def16;
end;
end;
canceled 2;
theorem Th25:
g in sproduct f implies dom g c= dom f &
for x st x in dom g holds g.x in f.x
proof assume g in sproduct f;
then ex h st g = h & dom h c= dom f &
for x st x in dom h holds h.x in f.x by Def16;
hence thesis;
end;
theorem Th26:
{} in sproduct f
proof
dom {} c= dom f & for x st x in dom {} holds {} .x in f.x by XBOOLE_1:2;
hence {} in sproduct f by Def16;
end;
theorem Th27:
product f c= sproduct f
proof let x;
assume x in product f;
then ex g st x = g & dom g = dom f &
for x st x in dom f holds g.x in f.x by CARD_3:def 5;
hence x in sproduct f by Def16;
end;
theorem Th28:
x in sproduct f implies x is PartFunc of dom f, union rng f
proof assume x in sproduct f;
then consider g such that
A1: x = g & dom g c= dom f &
for x st x in dom g holds g.x in f.x by Def16;
rng g c= union rng f
proof let y be set;
assume y in rng g;
then consider z being set such that
A2: z in dom g & y = g.z by FUNCT_1:def 5;
A3: g.z in f.z by A1,A2;
f.z in rng f by A1,A2,FUNCT_1:def 5;
hence y in union rng f by A2,A3,TARSKI:def 4;
end;
hence x is PartFunc of dom f, union rng f by A1,RELSET_1:11;
end;
theorem Th29:
g in product f & h in sproduct f implies g +* h in product f
proof assume A1: g in product f;
then A2: dom g = dom f & for x st x in dom f holds g.x in f.x by CARD_3:18;
assume A3: h in sproduct f;
then dom h c= dom f & for x st x in dom h holds h.x in f.x by Th25;
then A4: dom g \/ dom h = dom f by A2,XBOOLE_1:12;
then A5: dom(g +* h) = dom f by FUNCT_4:def 1;
now let x;
assume
A6: x in dom f;
A7: (dom g \ dom h) \/ dom h = dom f by A4,XBOOLE_1:39;
now per cases by A6,A7,XBOOLE_0:def 2;
case
A8: x in dom g \ dom h;
then not x in dom h by XBOOLE_0:def 4;
hence x in dom f & (g +* h).x = g.x by A7,A8,FUNCT_4:12,XBOOLE_0:def 2;
case x in dom h;
hence (g +* h).x = h.x by FUNCT_4:14;
end;
hence (g +* h).x in f.x by A1,A3,Th25,CARD_3:18;
end;
hence g +* h in product f by A5,CARD_3:18;
end;
theorem Th30:
product f <> {} implies
(g in sproduct f iff ex h st h in product f & g <= h)
proof assume
A1: product f <> {};
thus g in sproduct f implies ex h st h in product f & g <= h
proof assume
A2: g in sproduct f;
consider k being Element of product f;
reconsider k as Function;
take k +* g;
thus k +* g in product f by A1,A2,Th29;
thus g <= k +* g by FUNCT_4:26;
end;
given h such that
A3: h in product f & g <= h;
A4: dom h = dom f & for x st x in dom f holds h.x in f.x by A3,CARD_3:18;
A5: dom g c= dom h by A3,RELAT_1:25;
now let x;
assume
A6: x in dom g;
then g.x = h.x by A3,GRFUNC_1:8;
hence g.x in f.x by A4,A5,A6;
end;
hence g in sproduct f by A4,A5,Def16;
end;
theorem Th31:
sproduct f c= PFuncs(dom f,union rng f)
proof let x;
assume x in sproduct f;
then x is PartFunc of dom f, union rng f by Th28;
hence x in PFuncs(dom f,union rng f) by PARTFUN1:119;
end;
theorem Th32:
f c= g implies sproduct f c= sproduct g
proof
assume A1: f c= g;
then A2: dom f c= dom g by GRFUNC_1:8;
let y;
assume y in sproduct f;
then consider h such that
A3: y = h & dom h c= dom f and
A4: for x st x in dom h holds h.x in f.x by Def16;
A5: dom h c= dom g by A2,A3,XBOOLE_1:1;
now let x;
assume
A6: x in dom h;
then f.x = g.x by A1,A3,GRFUNC_1:8;
hence h.x in g.x by A4,A6;
end;
hence y in sproduct g by A3,A5,Def16;
end;
theorem Th33:
sproduct {} = {{}}
proof
sproduct {} c= PFuncs({},{}) by Th31,RELAT_1:60,ZFMISC_1:2;
hence sproduct {} c= {{}} by PARTFUN1:122;
let x be set;
assume x in {{}};
then x = {} by TARSKI:def 1;
hence x in sproduct {} by Th26;
end;
theorem
PFuncs(A,B) = sproduct (A --> B)
proof
now per cases;
case
A1: A = {};
hence sproduct (A --> B) = { {} } by Th33,FUNCT_4:3
.= PFuncs(A,B) by A1,PARTFUN1:122;
case
A <> {};
then rng (A --> B) = { B } by FUNCOP_1:14;
then A2: dom(A --> B) = A & B = union rng (A --> B)
by FUNCOP_1:19,ZFMISC_1:31;
thus PFuncs(A,B) c= sproduct (A --> B)
proof let x;
assume x in PFuncs(A,B);
then consider f being Function such that
A3: x = f & dom f c= A & rng f c= B by PARTFUN1:def 5;
A4: dom f c= dom (A --> B) by A3,FUNCOP_1:19;
now let x;
assume
A5: x in dom f;
then f.x in rng f by FUNCT_1:def 5;
then f.x in B by A3;
hence f.x in (A --> B).x by A3,A5,FUNCOP_1:13;
end;
hence x in sproduct (A --> B) by A3,A4,Def16;
end;
thus sproduct (A --> B) c= PFuncs(A,B) by A2,Th31;
end;
hence thesis by XBOOLE_0:def 10;
end;
theorem
for A, B being non empty set
for f being Function of A,B
holds sproduct f = sproduct(f|{x where x is Element of A: f.x <> {} })
proof let A, B be non empty set;
let f be Function of A,B;
set X = {x where x is Element of A: f.x <> {} };
thus sproduct f c= sproduct(f|X)
proof let x;
assume x in sproduct f;
then consider g such that
A1: x = g & dom g c= dom f &
for x st x in dom g holds g.x in f.x by Def16;
A2: now let x;
assume
A3: x in dom g;
then reconsider a = x as Element of A by A1,FUNCT_2:def 1;
f.a <> {} by A1,A3;
hence x in X;
end;
A4: now let x;
assume A5: x in dom g;
then x in X by A2;
hence x in (dom f)/\ X by A1,A5,XBOOLE_0:def 3;
end;
A6: dom g c= dom(f|X)
proof let x;
assume x in dom g;
then x in (dom f)/\ X by A4;
hence x in dom(f|X) by RELAT_1:90;
end;
now let x;
assume x in dom g;
then x in (dom f)/\ X & g.x in f.x by A1,A4;
hence g.x in (f|X).x by FUNCT_1:71;
end;
hence x in sproduct(f|X) by A1,A6,Def16;
end;
f|X c= f by RELAT_1:88;
hence thesis by Th32;
end;
theorem Th36:
x in dom f & y in f.x implies x .--> y in sproduct f
proof assume that
A1: x in dom f and
A2: y in f.x;
A3: dom(x .--> y) = {x} by CQC_LANG:5;
then A4: dom(x .--> y) c= dom f by A1,ZFMISC_1:37;
now let z;
assume z in dom(x .--> y);
then z = x by A3,TARSKI:def 1;
hence (x .--> y).z in f.z by A2,CQC_LANG:6;
end;
hence x .--> y in sproduct f by A4,Def16;
end;
theorem
sproduct f = {{}} iff for x st x in dom f holds f.x = {}
proof
thus sproduct f = {{}} implies for x st x in dom f holds f.x = {}
proof assume
A1: sproduct f = {{}};
let x; assume
A2: x in dom f;
assume
A3: f.x <> {};
consider y being Element of f.x;
x .--> y in sproduct f by A2,A3,Th36;
then x .--> y = {} by A1,TARSKI:def 1;
then {[x,y]} = {} by Th19;
hence contradiction;
end;
assume
A4: for x st x in dom f holds f.x = {};
now let x;
thus x in sproduct f implies x = {}
proof assume x in sproduct f;
then consider g such that
A5: x = g and
A6: dom g c= dom f and
A7: for y st y in dom g holds g.y in f.y by Def16;
assume x <> {};
then A8: dom g <> {} by A5,RELAT_1:64;
consider y being Element of dom g;
f.y <> {} & y in dom f by A6,A7,A8,TARSKI:def 3;
hence contradiction by A4;
end;
thus x = {} implies x in sproduct f by Th26;
end;
hence sproduct f = {{}} by TARSKI:def 1;
end;
theorem Th38:
A c= sproduct f &
(for h1,h2 being Function st h1 in A & h2 in A holds h1 tolerates h2)
implies union A in sproduct f
proof assume that
A1: A c= sproduct f and
A2: for h1,h2 being Function st h1 in A & h2 in A holds h1 tolerates h2;
for x be set st x in A holds x is Function by A1,FRAENKEL:def 1;
then reconsider g = union A as Function by A2,Th15;
A3: dom g c= dom f
proof let x;
assume x in dom g;
then consider y such that
A4: [x,y] in g by RELAT_1:def 4;
consider h being set such that
A5: [x,y] in h and
A6: h in A by A4,TARSKI:def 4;
reconsider h as Function by A1,A6,FRAENKEL:def 1;
A7: x in dom h by A5,RELAT_1:def 4;
dom h c= dom f by A1,A6,Th25;
hence x in dom f by A7;
end;
now let x;
assume x in dom g;
then consider y such that
A8: [x,y] in g by RELAT_1:def 4;
consider h being set such that
A9: [x,y] in h and
A10: h in A by A8,TARSKI:def 4;
reconsider h as Function by A1,A10,FRAENKEL:def 1;
A11: x in dom h by A9,RELAT_1:def 4;
h.x = y by A9,FUNCT_1:8 .= g.x by A8,FUNCT_1:8;
hence g.x in f.x by A1,A10,A11,Th25;
end;
hence union A in sproduct f by A3,Def16;
end;
theorem
g tolerates h & g in sproduct f & h in sproduct f
implies g \/ h in sproduct f
proof assume that
A1: g tolerates h and
A2: g in sproduct f & h in sproduct f;
A3: {g,h} c= sproduct f by A2,ZFMISC_1:38;
A4: now let h1,h2 be Function;
assume h1 in {g,h} & h2 in {g,h};
then (h1 = g or h1 = h) & (h2 = g or h2 = h) by TARSKI:def 2;
hence h1 tolerates h2 by A1;
end;
union {g,h} = g \/ h by ZFMISC_1:93;
hence g \/ h in sproduct f by A3,A4,Th38;
end;
theorem Th40:
g c= h & h in sproduct f implies g in sproduct f
proof assume that
A1: g c= h and
A2: h in sproduct f;
A3: dom g c= dom h by A1,GRFUNC_1:8;
dom h c= dom f by A2,Th25;
then A4: dom g c= dom f by A3,XBOOLE_1:1;
now let x;
assume
A5: x in dom g;
then h.x in f.x by A2,A3,Th25;
hence g.x in f.x by A1,A5,GRFUNC_1:8;
end;
hence g in sproduct f by A4,Def16;
end;
theorem Th41:
g in sproduct f implies g|A in sproduct f
proof
g|A c= g by RELAT_1:88;
hence thesis by Th40;
end;
theorem Th42:
g in sproduct f implies g|A in sproduct f|A
proof
A1: dom(g|A) = dom g /\ A & dom(f|A) = dom f /\ A by RELAT_1:90;
assume
A2: g in sproduct f;
then dom g c= dom f by Th25;
then A3: dom(g|A) c= dom(f|A) by A1,XBOOLE_1:26;
now let x;
assume
A4: x in dom(g|A);
then A5: (g|A).x = g.x & (f|A).x = f.x by A3,FUNCT_1:70;
x in dom g by A1,A4,XBOOLE_0:def 3;
hence (g|A).x in (f|A).x by A2,A5,Th25;
end;
hence g|A in sproduct f|A by A3,Def16;
end;
theorem
h in sproduct(f+*g) implies
ex f',g' being Function st f' in sproduct f & g' in sproduct g & h = f'+*g'
proof
assume
A1: h in sproduct(f+*g);
take h|(dom f \ dom g), h|dom g;
A2: h|(dom f \ dom g) in sproduct (f +* g)|(dom f \ dom g) by A1,Th42;
(f +* g)|(dom f \ dom g) c= f by FUNCT_4:25;
then sproduct (f +* g)|(dom f \ dom g) c= sproduct f by Th32;
hence h|(dom f \ dom g) in sproduct f by A2;
(f +* g)|dom g = g by FUNCT_4:24;
hence h|dom g in sproduct g by A1,Th42;
dom h c= dom(f+*g) by A1,Th25;
then dom h c= dom f \/ dom g by FUNCT_4:def 1;
then dom h c= (dom f \ dom g) \/ dom g by XBOOLE_1:39;
hence h = h|(dom f \ dom g) +* h|dom g by Th16;
end;
theorem Th44:
for f',g' being Function st dom g misses dom f' \ dom g' &
f' in sproduct f & g' in sproduct g
holds f'+*g' in sproduct(f+*g)
proof
let f',g' be Function such that
A1: dom g misses dom f' \ dom g' and
A2: f' in sproduct f & g' in sproduct g;
set h = f'+*g';
A3: dom f' c= dom f & dom g' c= dom g by A2,Th25;
then A4:dom f' \/ dom g' c= dom f \/ dom g by XBOOLE_1:13;
A5: dom h = dom f' \/ dom g' by FUNCT_4:def 1;
then A6: dom h c= dom(f+*g) by A4,FUNCT_4:def 1;
x in dom h implies h.x in (f+*g).x
proof assume
A7: x in dom h;
then x in dom(f+*g) by A6;
then A8: x in dom f \/ dom g by FUNCT_4:def 1;
x in dom f' \ dom g' \/ dom g' by A5,A7,XBOOLE_1:39;
then A9: x in dom f' \ dom g' or x in dom g' by XBOOLE_0:def 2;
now per cases;
case
A10: x in dom g;
then h.x = g'.x by A1,A5,A7,A9,FUNCT_4:def 1,XBOOLE_0:3;
hence h.x in g.x by A1,A2,A9,A10,Th25,XBOOLE_0:3;
case not x in dom g;
then A11: not x in dom g' by A3;
then A12: h.x = f'.x by A5,A7,FUNCT_4:def 1;
x in dom f' by A5,A7,A11,XBOOLE_0:def 2;
hence h.x in f.x by A2,A12,Th25;
end;
hence h.x in (f+*g).x by A8,FUNCT_4:def 1;
end;
hence h in sproduct(f+*g) by A6,Def16;
end;
theorem
for f',g' being Function st dom f' misses dom g \ dom g' &
f' in sproduct f & g' in sproduct g
holds f'+*g' in sproduct(f+*g)
proof let f',g' be Function;
assume dom f' misses dom g \ dom g';
then dom g misses dom f' \ dom g' by XBOOLE_1:81;
hence thesis by Th44;
end;
theorem Th46:
g in sproduct f & h in sproduct f
implies g +* h in sproduct f
proof
assume
A1: g in sproduct f & h in sproduct f;
then dom g c= dom f & dom h c= dom f by Th25;
then dom g \/ dom h c= dom f by XBOOLE_1:8;
then A2: dom(g+*h) c= dom f by FUNCT_4:def 1;
now let x;
assume x in dom(g+*h);
then x in dom g \/ dom h by FUNCT_4:def 1;
then A3: x in (dom g \ dom h \/ dom h) by XBOOLE_1:39;
now per cases by A3,XBOOLE_0:def 2;
suppose
A4: x in dom h;
then h.x in f.x by A1,Th25;
hence (g+*h).x in f.x by A4,FUNCT_4:14;
suppose
A5: x in dom g \ dom h;
then x in dom g by XBOOLE_0:def 4;
then A6: g.x in f.x by A1,Th25;
not x in dom h by A5,XBOOLE_0:def 4;
hence (g+*h).x in f.x by A6,FUNCT_4:12;
end;
hence (g+*h).x in f.x;
end;
hence thesis by A2,Def16;
end;
theorem
for x1,x2,y1,y2 being set holds
x1 in dom f & y1 in f.x1 & x2 in dom f & y2 in f.x2
implies (x1,x2)-->(y1,y2) in sproduct f
proof let x1,x2,y1,y2 be set;
assume x1 in dom f & y1 in f.x1;
then A1: x1 .--> y1 in sproduct f by Th36;
assume x2 in dom f & y2 in f.x2;
then A2: x2 .--> y2 in sproduct f by Th36;
(x1,x2)-->(y1,y2) = (x1 .--> y1) +* (x2 .--> y2) by Th18;
hence (x1,x2)-->(y1,y2) in sproduct f by A1,A2,Th46;
end;
begin :: General theory
definition let N;
let S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
let s be State of S;
func CurInstr s -> Instruction of S equals
:Def17: s.IC s;
coherence
proof
dom the Object-Kind of S = the carrier of S by FUNCT_2:def 1;
then pi(product the Object-Kind of S,IC s) = (the Object-Kind of S).IC s
by CARD_3:22
.= ObjectKind IC s by Def6
.= the Instructions of S by Def14;
hence thesis by CARD_3:def 6;
end;
end;
definition let N;
let S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
let s be State of S;
func Following s -> State of S equals
:Def18: Exec(CurInstr s,s);
correctness;
end;
definition let N;
let S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
let s be State of S;
func Computation s -> Function of NAT, product the Object-Kind of S
means
:Def19:
it.0 = s &
for i holds it.(i+1) = Following(it.i);
existence
proof
deffunc F(set, Element of product the Object-Kind of S) = Following $2;
consider f being Function of NAT, product the Object-Kind of S
such that
A1: f.0 = s & for n being Element of NAT holds f.(n+1) = F(n,f.n)
from LambdaRecExD;
take f;
thus thesis by A1;
end;
uniqueness
proof let F1,F2 be Function of NAT, product the Object-Kind of S such that
A2: F1.0 = s &
for i holds F1.(i+1) = Following(F1.i) and
A3: F2.0 = s &
for i holds F2.(i+1) = Following(F2.i);
deffunc F(set, Element of product the Object-Kind of S) = Following $2;
A4: F1.0 = s & for i holds F1.(i+1) = F(i,F1.i) by A2;
A5: F2.0 = s & for i holds F2.(i+1) = F(i,F2.i) by A3;
thus F1 = F2 from LambdaRecUnD(A4,A5);
end;
end;
definition let N; let S be non void AMI-Struct over N;
let f be Function of NAT, product the Object-Kind of S;
let k;
redefine func f.k -> State of S;
coherence by FUNCT_2:7;
end;
definition let N;
let S be halting IC-Ins-separated definite
(non empty non void AMI-Struct over N);
let IT be State of S;
attr IT is halting means
:Def20: ex k st CurInstr((Computation IT).k) = halt S;
end;
definition let N be set; let IT be AMI-Struct over N;
attr IT is realistic means
:Def21: the Instructions of IT <> the Instruction-Locations of IT;
end;
theorem Th48:
for S being IC-Ins-separated definite (non empty non void AMI-Struct over E)
st S is realistic holds
not ex l being Instruction-Location of S st IC S = l
proof
let S be IC-Ins-separated definite (non empty non void AMI-Struct over E)
such that
A1: S is realistic;
given l being Instruction-Location of S such that
A2: IC S = l;
ObjectKind IC S = the Instruction-Locations of S &
ObjectKind l = the Instructions of S by Def11,Def14;
hence contradiction by A1,A2,Def21;
end;
reserve
S for IC-Ins-separated definite (non empty non void AMI-Struct over N),
s for State of S;
canceled 2;
theorem Th51:
for k holds
(Computation s).(i+k) = (Computation (Computation s).i).k
proof
defpred _P[Nat] means
(Computation s).(i+$1) = (Computation (Computation s).i).$1;
A1: _P[0] by Def19;
A2: now let k; assume
A3: _P[k];
(Computation s).(i+(k+1)) = (Computation s).(i+k+1) by XCMPLX_1:1
.= Following (Computation s).(i+k) by Def19
.= (Computation (Computation s).i).(k+1) by A3,Def19;
hence _P[k+1];
end;
thus for k holds _P[k] from Ind(A1,A2);
end;
theorem Th52:
i <= j implies
for N for S being
halting IC-Ins-separated definite (non empty non void AMI-Struct over N)
for s being State of S st CurInstr((Computation s).i) = halt S
holds (Computation s).j = (Computation s).i
proof assume i <= j;
then consider k such that
A1: j = i + k by NAT_1:28;
let N;
let S be halting IC-Ins-separated definite
(non empty non void AMI-Struct over N);
let s be State of S such that
A2: CurInstr((Computation s).i) = halt S;
defpred _P[Nat] means
(Computation s).(i+$1) = (Computation s).i;
A3: _P[0];
A4: now let k; assume
A5: _P[k];
(Computation s).(i+(k+1)) = (Computation s).(i+k+1) by XCMPLX_1:1
.= Following (Computation s).(i+k) by Def19
.= Exec(halt S,(Computation s).i) by A2,A5,Def18
.= (Computation s).i by Def8;
hence _P[k+1];
end;
for k holds _P[k] from Ind(A3,A4);
hence (Computation s).j = (Computation s).i by A1;
end;
definition let N;
let S be halting IC-Ins-separated definite
(non empty non void AMI-Struct over N);
let s be State of S such that
A1: s is halting;
func Result s -> State of S means
:Def22: ex k st it = (Computation s).k & CurInstr(it) = halt S;
uniqueness
proof let s1,s2 be State of S;
given k1 being Nat such that
A2: s1 = (Computation s).k1 & CurInstr(s1) = halt S;
given k2 being Nat such that
A3: s2 = (Computation s).k2 & CurInstr(s2) = halt S;
k1 <= k2 or k2 <= k1;
hence s1 = s2 by A2,A3,Th52;
end;
correctness
proof
ex k st CurInstr((Computation s).k) = halt S by A1,Def20;
hence thesis;
end;
end;
theorem
for S being steady-programmed
IC-Ins-separated definite (non empty non void AMI-Struct over N)
for s being State of S, i be Instruction-Location of S
holds s.i = (Following s).i
proof
let S be steady-programmed
IC-Ins-separated definite (non empty non void AMI-Struct over N);
let s be State of S, i be Instruction-Location of S;
thus s.i = Exec(CurInstr s,s).i by Def13
.= (Following s).i by Def18;
end;
definition let N; let S be definite (non empty non void AMI-Struct over N);
let s be State of S, l be Instruction-Location of S;
redefine func s.l -> Instruction of S;
coherence
proof
dom the Object-Kind of S = the carrier of S by FUNCT_2:def 1;
then pi(product the Object-Kind of S,l) = (the Object-Kind of S).l
by CARD_3:22
.= ObjectKind l by Def6
.= the Instructions of S by Def14;
hence s.l is Instruction of S by CARD_3:def 6;
end;
end;
theorem Th54:
for S being steady-programmed IC-Ins-separated definite
(non empty non void AMI-Struct over N)
for s being State of S, i be Instruction-Location of S, k
holds s.i = (Computation s).k.i
proof
let S be steady-programmed
IC-Ins-separated definite (non empty non void AMI-Struct over N);
let s be State of S, i be Instruction-Location of S;
defpred _P[Nat] means s.i = (Computation s).$1.i;
A1: _P[0] by Def19;
A2: now let k;
assume _P[k];
then s.i = Exec(CurInstr (Computation s).k,(Computation s).k).i by Def13
.= (Following (Computation s).k).i by Def18
.= (Computation s).(k+1).i by Def19;
hence _P[k+1];
end;
thus for k holds _P[k] from Ind(A1,A2);
end;
theorem
for S being steady-programmed IC-Ins-separated definite
(non empty non void AMI-Struct over N)
for s being State of S
holds (Computation s).(k+1)
= Exec(s.(IC (Computation s).k),(Computation s).k)
proof
let S be steady-programmed
IC-Ins-separated definite (non empty non void AMI-Struct over N);
let s be State of S;
thus (Computation s).(k+1)
= Following (Computation s).k by Def19
.= Exec(CurInstr (Computation s).k,(Computation s).k) by Def18
.= Exec((Computation s).k.(IC (Computation s).k),(Computation s).k) by Def17
.= Exec(s.(IC (Computation s).k),(Computation s).k) by Th54;
end;
theorem Th56:
for S being steady-programmed IC-Ins-separated
halting definite (non empty non void AMI-Struct over N)
for s being State of S, k st s.IC (Computation s).k = halt S
holds Result s = (Computation s).k
proof
let S be steady-programmed IC-Ins-separated
halting definite (non empty non void AMI-Struct over N);
let s be State of S, k such that
A1: s.IC (Computation s).k = halt S;
A2:CurInstr((Computation s).k)
= (Computation s).k.IC (Computation s).k by Def17
.= halt S by A1,Th54;
then s is halting by Def20;
hence Result s = (Computation s).k by A2,Def22;
end;
theorem
for S being steady-programmed IC-Ins-separated
halting definite (non empty non void AMI-Struct over N)
for s being State of S st
ex k st s.IC (Computation s).k = halt S
for i holds Result s = Result (Computation s).i
proof
let S be steady-programmed IC-Ins-separated
halting definite (non empty non void AMI-Struct over N);
let s be State of S;
given k such that
A1: s.IC (Computation s).k = halt S;
set s' = (Computation s).k;
A2: CurInstr s' = s'.IC s' by Def17
.= halt S by A1,Th54;
let i;
now per cases;
suppose i <= k;
then consider j such that
A3: k = i + j by NAT_1:28;
A4: (Computation s).k = (Computation (Computation s).i).j by A3,Th51;
then A5: (Computation s).i is halting by A2,Def20;
thus Result s = s' by A1,Th56
.= Result (Computation s).i by A2,A4,A5,Def22;
suppose i >= k;
then A6: (Computation s).i = s' by A2,Th52;
A7: (Computation (Computation s).k).0 = (Computation s).k by Def19;
then A8: (Computation s).i is halting by A2,A6,Def20;
thus Result s = s' by A1,Th56
.= Result (Computation s).i by A2,A6,A7,A8,Def22;
end;
hence Result s = Result (Computation s).i;
end;
definition let N;
let S be non empty non void AMI-Struct over N, o be Object of S;
cluster ObjectKind o -> non empty;
coherence by Def1;
end;
begin :: Finite substates
definition let N be set; let S be AMI-Struct over N;
func FinPartSt S -> Subset of sproduct the Object-Kind of S equals
{ p where p is Element of sproduct the Object-Kind of S: p is finite };
coherence
proof defpred _P[set] means $1 is finite;
{ p where p is Element of sproduct the Object-Kind of S: _P[p] } c=
sproduct the Object-Kind of S from Fr_Set0;
hence thesis;
end;
end;
definition let N be set; let S be AMI-Struct over N;
mode FinPartState of S -> Element of sproduct the Object-Kind of S means
:Def24: it is finite;
existence
proof
{} in sproduct the Object-Kind of S & {} is finite by Th26;
hence thesis;
end;
end;
definition let N;
let S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
let IT be FinPartState of S;
attr IT is autonomic means
:Def25: for s1,s2 being State of S st IT c= s1 & IT c= s2
for i holds (Computation s1).i|dom IT = (Computation s2).i|dom IT;
end;
definition let N;
let S be halting IC-Ins-separated definite
(non empty non void AMI-Struct over N);
let IT be FinPartState of S;
attr IT is halting means
:Def26: for s being State of S st IT c= s holds s is halting;
end;
definition let N;
let IT be IC-Ins-separated definite (non empty non void AMI-Struct over N);
attr IT is programmable means
:Def27: ex s being FinPartState of IT st s is non empty autonomic;
end;
theorem Th58:
for S being IC-Ins-separated definite (non empty non void AMI-Struct over N)
for A,B being set, la,lb being Object of S st
ObjectKind la = A & ObjectKind lb = B
for a being Element of A, b being Element of B holds
(la,lb) --> (a,b) is FinPartState of S
proof
let S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
let A,B be set, la,lb be Object of S such that
A1: ObjectKind la = A & ObjectKind lb = B;
let a be Element of A, b be Element of B;
set p = (la,lb) --> (a,b);
A2:dom p = {la,lb} by FUNCT_4:65;
A3: dom the Object-Kind of S = the carrier of S by FUNCT_2:def 1;
now let x be set such that
A4: x in dom p;
now per cases by A2,A4,TARSKI:def 2;
suppose
A5: la <> lb & x = la;
then p.x = a by FUNCT_4:66;
then p.x in ObjectKind la by A1;
hence p.x in (the Object-Kind of S).x by A5,Def6;
suppose
A6: la <> lb & x = lb;
then p.x = b by FUNCT_4:66;
then p.x in ObjectKind lb by A1;
hence p.x in (the Object-Kind of S).x by A6,Def6;
suppose
A7: la = lb & x = la;
then p = la .--> b by Th20;
then p.x = b by A7,CQC_LANG:6;
then p.x in ObjectKind lb by A1;
hence p.x in (the Object-Kind of S).x by A7,Def6;
end;
hence p.x in (the Object-Kind of S).x;
end;
then reconsider p as Element of sproduct the Object-Kind of S by A2,A3,Def16;
p is FinPartState of S
proof
dom p = {la,lb} by FUNCT_4:65;
hence p is finite by Th21;
end;
hence thesis;
end;
theorem Th59:
for S being IC-Ins-separated definite (non empty non void AMI-Struct over N)
for A being set, la being Object of S st ObjectKind la = A
for a being Element of A holds la .--> a is FinPartState of S
proof let S be IC-Ins-separated definite
(non empty non void AMI-Struct over N);
let A be set, la be Object of S such that
A1: ObjectKind la = A;
let a be Element of A;
set p = la .--> a;
A2:dom p = {la} by CQC_LANG:5;
A3:dom the Object-Kind of S = the carrier of S by FUNCT_2:def 1;
now let x be set;
assume x in dom p;
then A4: x = la by A2,TARSKI:def 1;
then p.x = a by CQC_LANG:6;
then p.x in ObjectKind la by A1;
hence p.x in (the Object-Kind of S).x by A4,Def6;
end;
then reconsider p as Element of sproduct the Object-Kind of S by A2,A3,Def16;
p is FinPartState of S
proof
dom p = {la} by CQC_LANG:5;
hence p is finite by Th21;
end;
hence thesis;
end;
definition let N;
let S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
let la be Object of S;
let a be Element of ObjectKind la;
redefine func la .--> a -> FinPartState of S;
coherence by Th59;
end;
definition let N;
let S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
let la,lb be Object of S;
let a be Element of ObjectKind la,
b be Element of ObjectKind lb;
redefine func (la,lb) --> (a,b) -> FinPartState of S;
coherence by Th58;
end;
theorem Th60:
Trivial-AMI E is realistic
proof
A1: the Instructions of Trivial-AMI E = {[0,{}]} &
the Instruction-Locations of Trivial-AMI E = {1} by Def2;
assume the Instructions of Trivial-AMI E
= the Instruction-Locations of Trivial-AMI E;
then [0,{}] = 1 by A1,ZFMISC_1:6;
hence contradiction by Th2;
end;
theorem Th61:
Trivial-AMI N is programmable
proof
reconsider la = 0 as Object of Trivial-AMI N by Def2;
ObjectKind la = (the Object-Kind of Trivial-AMI N).la by Def6
.= ((0,1) --> ({1},{[0,{}]})).0 by Def2
.= {1} by FUNCT_4:66;
then reconsider a = 1 as Element of ObjectKind la by TARSKI:def 1;
take la .--> a;
0 .--> 1 = ({0} --> 1) by CQC_LANG:def 2
.= [:{0},{1}:] by FUNCOP_1:def 2;
hence la .--> a is non empty;
let s1,s2 be State of Trivial-AMI N such that
la .--> a c= s1 & la .--> a c= s2;
let i;
thus (Computation s1).i|dom(la .--> a) = (Computation s2).i|dom(la .--> a)
by Th9;
end;
definition let E;
cluster Trivial-AMI E -> realistic;
coherence by Th60;
end;
definition let N;
cluster Trivial-AMI N -> programmable;
coherence by Th61;
end;
definition let E;
cluster data-oriented realistic strict AMI-Struct over E;
existence
proof
take Trivial-AMI E;
thus thesis;
end;
end;
definition let M be set;
cluster data-oriented realistic strict IC-Ins-separated
definite (non empty non void AMI-Struct over M);
existence
proof
take Trivial-AMI M;
thus thesis;
end;
end;
definition let N;
cluster data-oriented halting steady-programmed realistic programmable
strict (IC-Ins-separated definite
(non empty non void AMI-Struct over N));
existence
proof
take Trivial-AMI N;
thus thesis;
end;
end;
theorem Th62:
for S being non void AMI-Struct over N,
s being State of S, p being FinPartState of S
holds s|dom p is FinPartState of S
proof let S be non void AMI-Struct over N,
s be State of S, p be FinPartState of S;
product the Object-Kind of S c= sproduct the Object-Kind of S
& s in product the Object-Kind of S by Th27;
then A1:s|dom p in sproduct the Object-Kind of S by Th41;
A2: dom(s|dom p) = dom s /\ dom p by RELAT_1:90;
p is finite by Def24;
then dom p is finite by Th21;
then dom(s|dom p) is finite by A2,FINSET_1:15;
then s|dom p is finite by Th21;
hence s|dom p is FinPartState of S by A1,Def24;
end;
theorem Th63:
for N being set for S being AMI-Struct over N holds {} is FinPartState of S
proof let N be set, S be AMI-Struct over N;
{} is Element of sproduct the Object-Kind of S
& {} is finite by Th26;
hence {} is FinPartState of S by Def24;
end;
definition let N;
let S be programmable
(IC-Ins-separated definite (non empty non void AMI-Struct over N));
cluster non empty autonomic FinPartState of S;
existence by Def27;
end;
definition let N be set;
let S be AMI-Struct over N;
let f,g be FinPartState of S;
redefine func f +* g -> FinPartState of S;
coherence
proof
A1: f +* g is Element of sproduct the Object-Kind of S by Th46;
f is finite & g is finite by Def24;
then A2: dom f is finite & dom g is finite by Th21;
dom(f +* g) = dom f \/ dom g by FUNCT_4:def 1;
then dom(f +* g) is finite by A2,FINSET_1:14;
then f +* g is finite by Th21;
hence thesis by A1,Def24;
end;
end;
begin :: Preprograms
theorem Th64:
for S being halting realistic IC-Ins-separated definite
(non empty non void AMI-Struct over N)
for loc being Instruction-Location of S
for l being Element of ObjectKind IC S st l = loc
for h being Element of ObjectKind loc st h = halt S
for s being State of S st (IC S,loc) --> (l, h) c= s
holds CurInstr s = halt S
proof
let S be halting realistic
IC-Ins-separated definite (non empty non void AMI-Struct over N);
let loc be Instruction-Location of S;
let l be Element of ObjectKind IC S such that
A1: l = loc;
let h be Element of ObjectKind loc such that
A2: h = halt S;
let s be State of S such that
A3: (IC S,loc) --> (l, h) c= s;
A4: IC S <> loc by Th48;
dom((IC S,loc) --> (l, h)) = {IC S,loc} by FUNCT_4:65;
then A5: IC S in dom((IC S,loc) --> (l, h)) & loc in dom((IC S,loc) --> (l, h))
by TARSKI:def 2;
then A6: ((IC S,loc) --> (l, h)).IC S in dom((IC S,loc) --> (l, h))
by A1,A4,FUNCT_4:66;
thus CurInstr s = s.IC s by Def17
.= s.(s.IC S) by Def15
.= s.(((IC S,loc) --> (l, h)).IC S) by A3,A5,GRFUNC_1:8
.= ((IC S,loc) --> (l, h)).(((IC S,loc) --> (l, h)).IC S)
by A3,A6,GRFUNC_1:8
.= ((IC S,loc) --> (l, h)).loc by A1,A4,FUNCT_4:66
.= halt S by A2,A4,FUNCT_4:66;
end;
theorem Th65:
for S being halting realistic IC-Ins-separated definite
(non empty non void AMI-Struct over N)
for loc being Instruction-Location of S
for l being Element of ObjectKind IC S st l = loc
for h being Element of ObjectKind loc st h = halt S
holds (IC S,loc) --> (l, h) is halting
proof
let S be halting realistic
IC-Ins-separated definite (non empty non void AMI-Struct over N);
let loc be Instruction-Location of S;
let l be Element of ObjectKind IC S such that
A1: l = loc;
let h be Element of ObjectKind loc such that
A2: h = halt S;
thus (IC S,loc) --> (l, h) is halting
proof let s be State of S such that
A3: (IC S,loc) --> (l, h) c= s;
take 0;
thus CurInstr((Computation s).0)
= CurInstr s by Def19
.= halt S by A1,A2,A3,Th64;
end;
end;
theorem Th66:
for S being realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N)
for loc being Instruction-Location of S
for l being Element of ObjectKind IC S st l = loc
for h being Element of ObjectKind loc st h = halt S
for s being State of S st (IC S,loc) --> (l, h) c= s
for i holds (Computation s).i = s
proof
let S be realistic halting
IC-Ins-separated definite (non empty non void AMI-Struct over N);
let loc be Instruction-Location of S;
let l be Element of ObjectKind IC S such that
A1: l = loc;
let h be Element of ObjectKind loc such that
A2: h = halt S;
let s be State of S such that
A3: (IC S,loc) --> (l, h) c= s;
defpred _P[Nat] means (Computation s).$1 = s;
A4: _P[0] by Def19;
A5: now let i;
assume
A6: _P[i];
(Computation s).(i+1) = Following (Computation s).i by Def19
.= Exec(CurInstr s,s) by A6,Def18 .= Exec(halt S,s) by A1,A2,A3,Th64
.= s by Def8;
hence _P[i+1];
end;
thus for i holds _P[i] from Ind(A4,A5);
end;
theorem Th67:
for S be realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N)
for loc being Instruction-Location of S
for l being Element of ObjectKind IC S st l = loc
for h being Element of ObjectKind loc st h = halt S
holds (IC S,loc) --> (l, h) is autonomic
proof
let S be realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N);
let loc be Instruction-Location of S;
let l be Element of ObjectKind IC S such that
A1: l = loc;
let h be Element of ObjectKind loc such that
A2: h = halt S;
thus (IC S,loc) --> (l, h) is autonomic
proof let s1,s2 be State of S;
assume
A3: (IC S,loc) --> (l, h) c= s1 & (IC S,loc) --> (l, h) c= s2;
then A4: s1|dom((IC S,loc) --> (l, h)) = (IC S,loc) --> (l, h) &
s2|dom((IC S,loc) --> (l, h)) = (IC S,loc) --> (l, h) by GRFUNC_1:64;
let i;
(Computation s1).i = s1 & (Computation s2).i = s2 by A1,A2,A3,Th66;
hence thesis by A4;
end;
end;
definition let N;
let S be realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N);
cluster autonomic halting FinPartState of S;
existence
proof
consider loc being Instruction-Location of S;
reconsider l = loc as Element of ObjectKind IC S by Def11;
reconsider h = halt S as Element of ObjectKind loc by Def14;
(IC S,loc) --> (l, h) is autonomic halting by Th65,Th67;
hence thesis;
end;
end;
definition let N;
let S be realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N);
mode pre-program of S is autonomic halting FinPartState of S;
end;
definition let N;
let S be realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N);
let s be FinPartState of S;
assume
A1: s is pre-program of S;
func Result(s) -> FinPartState of S means
for s' being State of S st s c= s' holds it = (Result s')|dom s;
existence
proof
sproduct the Object-Kind of S <> {};
then consider h being Function such that
A2: h in product the Object-Kind of S and
A3: s <= h by Th30;
reconsider h as State of S by A2;
reconsider R = (Result h)|dom s as FinPartState of S by Th62;
take R;
let s' be State of S such that
A4: s c= s';
h is halting by A1,A3,Def26;
then consider k1 being Nat such that
A5: Result h = (Computation h).k1 & CurInstr(Result h) = halt S by Def22;
s' is halting by A1,A4,Def26;
then consider k2 being Nat such that
A6: Result s' = (Computation s').k2 & CurInstr(Result s') = halt S by Def22;
now per cases;
suppose k1 <= k2;
then Result h = (Computation h).k2 by A5,Th52;
hence R = (Result s')|dom s by A1,A3,A4,A6,Def25;
suppose k1 >= k2;
then Result s' = (Computation s').k1 by A6,Th52;
hence R = (Result s')|dom s by A1,A3,A4,A5,Def25;
end;
hence R = (Result s')|dom s;
end;
correctness
proof let p1,p2 be FinPartState of S such that
A7: for s' being State of S st s c= s' holds p1 = (Result s')|dom s and
A8: for s' being State of S st s c= s' holds p2 = (Result s')|dom s;
sproduct the Object-Kind of S <> {};
then consider h being Function such that
A9: h in product the Object-Kind of S and
A10: s <= h by Th30;
reconsider h as State of S by A9;
thus p1 = (Result h)|dom s by A7,A10 .= p2 by A8,A10;
end;
end;
begin :: Computability
definition let N;
let S be realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N);
let p be FinPartState of S, F be Function;
pred p computes F means
:Def29:
for x being set st x in dom F ex s being FinPartState of S st x = s &
p +* s is pre-program of S & F.s c= Result(p +* s);
antonym p does_not_compute F;
end;
theorem Th68:
for S being realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N)
for p being FinPartState of S
holds p computes {}
proof
let S be realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N);
let p be FinPartState of S;
let x be set;
assume
A1: x in dom {};
then reconsider x as FinPartState of S;
take x;
thus thesis by A1;
end;
theorem Th69:
for S being realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N)
for p being FinPartState of S
holds p is pre-program of S iff p computes {} .--> Result(p)
proof
let S be realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N);
let p be FinPartState of S;
thus p is pre-program of S implies p computes {} .--> Result(p)
proof assume
A1: p is pre-program of S;
let x be set such that
A2: x in dom({} .--> Result(p));
dom({} .--> Result(p)) = {{}} by CQC_LANG:5;
then A3: x = {} by A2,TARSKI:def 1;
then reconsider s = x as FinPartState of S by Th63;
take s;
thus x = s;
thus p +* s is pre-program of S by A1,A3,FUNCT_4:22;
({} .--> Result(p)).s = Result(p) by A3,CQC_LANG:6;
hence ({} .--> Result(p)).s c= Result(p +* s) by A3,FUNCT_4:22;
end;
dom({} .--> Result(p)) = {{}} by CQC_LANG:5;
then A4: {} in dom({} .--> Result(p)) by TARSKI:def 1;
assume p computes {} .--> Result(p);
then consider s being FinPartState of S such that
A5: s = {} and
A6: p +* s is pre-program of S and
({} .--> Result(p)).s c= Result(p +* s) by A4,Def29;
thus thesis by A5,A6,FUNCT_4:22;
end;
theorem Th70:
for S being realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N)
for p being FinPartState of S
holds p is pre-program of S iff p computes {} .--> {}
proof
let S be realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N);
let p be FinPartState of S;
thus p is pre-program of S implies p computes {} .--> {}
proof assume
A1: p is pre-program of S;
let x be set such that
A2: x in dom({} .--> {});
dom({} .--> {}) = {{}} by CQC_LANG:5;
then A3: x = {} by A2,TARSKI:def 1;
then reconsider s = x as FinPartState of S by Th63;
take s;
thus x = s;
thus p +* s is pre-program of S by A1,A3,FUNCT_4:22;
({} .--> {}).s = {} by A3,CQC_LANG:6;
hence ({} .--> {}).s c= Result(p +* s) by XBOOLE_1:2;
end;
dom({} .--> {}) = {{}} by CQC_LANG:5;
then A4: {} in dom({} .--> {}) by TARSKI:def 1;
assume p computes {} .--> {};
then consider s being FinPartState of S such that
A5: s = {} and
A6: p +* s is pre-program of S and
({} .--> {}).s c= Result(p +* s) by A4,Def29;
thus thesis by A5,A6,FUNCT_4:22;
end;
definition let N;
let S be realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N);
let IT be PartFunc of FinPartSt S, FinPartSt S;
attr IT is computable means
:Def30: ex p being FinPartState of S st p computes IT;
end;
theorem Th71:
for S being realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N)
for F being PartFunc of FinPartSt S, FinPartSt S st F = {}
holds F is computable
proof
let S be realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N);
let F be PartFunc of FinPartSt S, FinPartSt S;
consider p being FinPartState of S;
assume
A1: F = {};
take p;
thus thesis by A1,Th68;
end;
theorem Th72:
for S being realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N)
for F being PartFunc of FinPartSt S, FinPartSt S st F = {} .--> {}
holds F is computable
proof
let S be realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N);
let F be PartFunc of FinPartSt S, FinPartSt S;
consider p being pre-program of S;
assume
A1: F = {} .--> {};
take p;
thus thesis by A1,Th70;
end;
theorem Th73:
for S being realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N)
for p being pre-program of S
for F being PartFunc of FinPartSt S, FinPartSt S st F = {} .--> Result(p)
holds F is computable
proof
let S be realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N);
let p be pre-program of S;
let F be PartFunc of FinPartSt S, FinPartSt S;
assume
A1: F = {} .--> Result(p);
take p;
thus thesis by A1,Th69;
end;
definition let N;
let S be realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N);
let F be PartFunc of FinPartSt S, FinPartSt S such that
A1: F is computable;
mode Program of F -> FinPartState of S means it computes F;
existence by A1,Def30;
end;
definition
let N be set, S be AMI-Struct over N;
mode InsType of S is Element of the Instruction-Codes of S;
canceled;
end;
theorem
for S being realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N)
for F being PartFunc of FinPartSt S, FinPartSt S st F = {}
for p being FinPartState of S
holds p is Program of F
proof
let S be realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N);
let F be PartFunc of FinPartSt S, FinPartSt S such that
A1: F = {};
let p be FinPartState of S;
thus F is computable by A1,Th71;
thus p computes F by A1,Th68;
end;
theorem
for S being realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N)
for F being PartFunc of FinPartSt S, FinPartSt S st F = {} .--> {}
for p being pre-program of S holds p is Program of F
proof
let S be realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N);
let F be PartFunc of FinPartSt S, FinPartSt S such that
A1: F = {} .--> {};
let p be pre-program of S;
thus F is computable by A1,Th72;
thus p computes F by A1,Th70;
end;
theorem
for S being realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N)
for p being pre-program of S
for F being PartFunc of FinPartSt S, FinPartSt S st F = {} .--> Result p
holds p is Program of F
proof
let S be realistic halting IC-Ins-separated definite
(non empty non void AMI-Struct over N);
let p be pre-program of S;
let F be PartFunc of FinPartSt S, FinPartSt S; assume
A1: F = {} .--> Result p;
hence F is computable by Th73;
thus p computes F by A1,Th69;
end;