Copyright (c) 1998 Association of Mizar Users
environ
vocabulary SUBSTLAT, FUNCT_1, RELAT_1, PARTFUN1, FRAENKEL, BOOLE, FINSET_1,
FINSUB_1, FINSEQ_1, NORMFORM, TARSKI, ARYTM_1, LATTICES, FUNCT_2,
HEYTING1, BINOP_1, FDIFF_1, LATTICE2, SETWISEO, FUNCOP_1, FILTER_0,
ZF_LANG, HEYTING2;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
FUNCOP_1, BINOP_1, FINSET_1, FINSUB_1, FUNCT_2, FRAENKEL, PARTFUN1,
LATTICES, STRUCT_0, SUBSTLAT, SETWISEO, HEYTING1, LATTICE2, FILTER_0;
constructors SETWISEO, GRCAT_1, SUBSTLAT, LATTICE2, FILTER_0, HEYTING1,
MEMBERED;
clusters RELSET_1, FINSET_1, FINSUB_1, SETWISEO, SUBSTLAT, MONOID_1, STRUCT_0,
RFINSEQ, SUBSET_1, RELAT_1, FUNCT_1, WELLFND1, FRAENKEL, FINSEQ_1;
requirements SUBSET, BOOLE;
definitions TARSKI, FILTER_0, XBOOLE_0;
theorems ZFMISC_1, TARSKI, FINSUB_1, FINSET_1, PARTFUN1, BINOP_1, LATTICES,
LATTICE2, RELAT_1, FUNCT_1, GRFUNC_1, FUNCT_2, SUBSTLAT, SETWISEO, AMI_1,
FUNCOP_1, FILTER_0, HEYTING1, RELSET_1, XBOOLE_0, XBOOLE_1;
schemes FRAENKEL, BINOP_1, LATTICE3, PRE_CIRC, FUNCT_1, FUNCT_2, XBOOLE_0;
begin :: Preliminaries
reserve V, C, x, a, b for set;
reserve A, B for Element of SubstitutionSet (V, C);
definition let a, b be set;
cluster {[a, b]} -> Function-like Relation-like;
coherence
proof
set X = {[a, b]};
A1:[:{a},{b}:] = X by ZFMISC_1:35;
for x,y1,y2 be set st [x,y1] in X & [x,y2] in X holds y1 = y2
proof
let x,y1,y2 be set such that
A2: [x,y1] in X and
A3: [x,y2] in X;
y1 = b & y2 = b by A1,A2,A3,ZFMISC_1:34;
hence thesis;
end;
hence X is Function-like by FUNCT_1:def 1;
thus X is Relation-like by RELAT_1:4;
end;
end;
theorem
for V, C being non empty set ex f be Element of PFuncs (V, C) st f <> {}
proof
let V, C be non empty set;
consider a be set such that A1: a in V by XBOOLE_0:def 1;
consider b be set such that A2: b in C by XBOOLE_0:def 1;
set f = {[a,b]};
{a} c= V & {b} c= C by A1,A2,ZFMISC_1:37;
then dom f c= V & rng f c= C by RELAT_1:23;
then reconsider f as Element of PFuncs (V, C) by PARTFUN1:def 5;
f <> {};
hence thesis;
end;
theorem Th2:
for a, b being set st b in SubstitutionSet (V, C) & a in b holds
a is finite Function
proof
let a, b be set; assume
A1: b in SubstitutionSet (V, C) & a in b;
then b in { A where A is Element of Fin PFuncs (V,C) :
( for u being set st u in A holds u is finite ) &
for s1, t being Element of PFuncs (V, C) holds
( s1 in A & t in A & s1 c= t implies s1 = t ) }
by SUBSTLAT:def 1;
then consider A being Element of Fin PFuncs (V,C) such that
A2: A = b & ( for u being set st u in A holds u is finite ) &
for s, t being Element of PFuncs (V, C) holds
( s in A & t in A & s c= t implies s = t );
a is Element of PFuncs (V, C) by A1,SETWISEO:14;
hence thesis by A1,A2;
end;
theorem Th3:
for f being Element of PFuncs (V, C),
g being set st g c= f holds g in PFuncs (V, C)
proof
let f be Element of PFuncs (V, C),
g be set;
assume A1: g c= f;
consider f1 be Function such that
A2: f1 = f & dom f1 c= V & rng f1 c= C by PARTFUN1:def 5;
reconsider g' = g as Function by A1,GRFUNC_1:6;
dom g' c= dom f1 & rng g' c= rng f1 by A1,A2,RELAT_1:25;
then dom g' c= V & rng g' c= C by A2,XBOOLE_1:1;
hence thesis by PARTFUN1:def 5;
end;
Lm1:
for A, B, C be set st A = B \/ C & A c= B holds A = B
proof
let A, B, C be set; assume
A1: A = B \/ C & A c= B;
then B c= A by XBOOLE_1:7;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem Th4:
PFuncs(V,C) c= bool [:V,C:]
proof
let x be set;
assume x in PFuncs(V,C);
then consider f being Function such that
A1: x = f and
A2: dom f c= V & rng f c= C by PARTFUN1:def 5;
A3: f c= [: dom f, rng f:] by RELAT_1:21;
[:dom f, rng f:] c= [:V,C:] by A2,ZFMISC_1:119;
then f c= [:V,C:] by A3,XBOOLE_1:1;
hence x in bool [:V,C:] by A1;
end;
theorem Th5:
V is finite & C is finite implies PFuncs (V, C) is finite
proof
A1: PFuncs(V,C) c= bool [:V,C:] by Th4;
assume V is finite & C is finite;
then [:V,C:] is finite by FINSET_1:19;
then bool [:V,C:] is finite by FINSET_1:24;
hence PFuncs(V,C) is finite by A1,FINSET_1:13;
end;
definition
cluster functional finite non empty set;
existence
proof
consider A, B be finite non empty set;
take P = PFuncs(A,B);
thus P is functional;
thus P is finite by Th5;
thus thesis;
end;
end;
begin :: Some properties of sets of substitutions
theorem Th6:
for a being finite Element of PFuncs (V, C) holds
{a} in SubstitutionSet (V, C)
proof
let a be finite Element of PFuncs (V, C);
A1: for u being set st u in {a} holds u is finite by TARSKI:def 1;
for s, t being Element of PFuncs (V,C) holds
( s in { a } & t in { a } & s c= t implies s = t )
proof
let s, t be Element of PFuncs (V,C);
assume s in { a } & t in { a } & s c= t;
then s = a & t = a by TARSKI:def 1;
hence s = t;
end;
then { a } in { A where A is Element of Fin PFuncs (V,C) :
( for u being set st u in A holds u is finite ) &
for s, t being Element of PFuncs (V, C) holds
( s in A & t in A & s c= t implies s = t ) } by A1;
hence thesis by SUBSTLAT:def 1;
end;
theorem
A ^ B = A implies for a be set st a in A ex b be set st b in B & b c= a
proof
assume A1: A ^ B = A;
let a be set;
assume a in A;
then consider b,c be set such that
A2: b in A & c in B & a = b \/ c by A1,SUBSTLAT:15;
take c;
thus thesis by A2,XBOOLE_1:7;
end;
theorem Th8:
mi (A ^ B) = A implies for a be set st a in A ex b be set st b in B & b c= a
proof
assume A1: mi (A ^ B) = A;
let a be set;
A2: mi (A ^ B) c= A ^ B by SUBSTLAT:8;
assume a in A;
then consider b,c be set such that
A3: b in A & c in B & a = b \/ c by A1,A2,SUBSTLAT:15;
take c;
thus thesis by A3,XBOOLE_1:7;
end;
theorem Th9:
(for a be set st a in A ex b be set st b in
B & b c= a) implies mi (A ^ B) = A
proof
assume A1: for a be set st a in A ex b be set st b in B & b c= a;
A2: mi (A ^ B) c= A ^ B by SUBSTLAT:8;
thus mi (A ^ B) c= A
proof
let a be set; assume A3: a in mi (A ^ B);
then consider b, c be set such that
A4: b in A & c in B & a = b \/ c by A2,SUBSTLAT:15;
consider b1 be set such that
A5: b1 in B & b1 c= b by A1,A4;
B c= PFuncs (V, C) & A c= PFuncs (V, C) by FINSUB_1:def 5;
then reconsider b' = b, b1' = b1 as Element of PFuncs (V, C)
by A4,A5;
A6: b1' tolerates b' by A5,PARTFUN1:135;
b = b1 \/ b by A5,XBOOLE_1:12;
then A7: b in A ^ B by A4,A5,A6,SUBSTLAT:16;
b c= a by A4,XBOOLE_1:7;
hence thesis by A3,A4,A7,SUBSTLAT:6;
end;
thus A c= mi (A ^ B)
proof
let a be set; assume A8: a in A;
then consider b be set such that A9: b in B & b c= a by A1;
A10: a in mi A by A8,SUBSTLAT:11;
A11: a is finite by A8,Th2;
B c= PFuncs (V, C) & A c= PFuncs (V, C) by FINSUB_1:def 5;
then reconsider a' = a, b' = b as Element of PFuncs (V, C) by A8,A9;
A12: a' = a' \/ b' by A9,XBOOLE_1:12;
a' tolerates b' by A9,PARTFUN1:135;
then A13:a' in A ^ B by A8,A9,A12,SUBSTLAT:16;
for b be finite set st b in A ^ B & b c= a holds b = a
proof
let b be finite set;
assume A14: b in A ^ B & b c= a;
then consider c, d be set such that
A15: c in A & d in B & b = c \/ d by SUBSTLAT:15;
c c= b by A15,XBOOLE_1:7;
then c c= a by A14,XBOOLE_1:1;
then c = a by A10,A15,SUBSTLAT:6;
hence thesis by A14,A15,Lm1;
end;
hence thesis by A11,A13,SUBSTLAT:7;
end;
end;
definition let V be set, C be finite set;
let A be Element of Fin PFuncs (V, C);
func Involved A means :Def1:
x in it iff ex f being finite Function st f in A & x in dom f;
existence
proof
defpred P[set] means ex f being finite Function st f in A & $1 in dom f;
consider X be set such that
A1: x in X iff x in V & P[x] from Separation;
take X;
let x be set;
thus x in X implies
ex f being finite Function st f in A & x in dom f by A1;
given f being finite Function such that
A2: f in A & x in dom f;
A c= PFuncs (V, C) by FINSUB_1:def 5;
then consider f1 being Function such that
A3: f = f1 & dom f1 c= V & rng f1 c= C by A2,PARTFUN1:def 5;
thus thesis by A1,A2,A3;
end;
uniqueness
proof
defpred P[set] means
ex f being finite Function st f in A & $1 in dom f;
A4: for X1,X2 being set st
(for x being set holds x in X1 iff P[x]) &
(for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq;
let r,s be set such that
A5: x in r iff ex f being finite Function st f in A & x in dom f and
A6: x in s iff ex f being finite Function st f in A & x in dom f;
thus r=s by A4,A5,A6;
end;
end;
reserve C for finite set;
theorem Th10:
for V being set, C be finite set,
A being Element of Fin PFuncs (V, C) holds Involved A c= V
proof
let V be set, C be finite set,
A be Element of Fin PFuncs (V, C);
let a be set;
assume a in Involved A;
then consider f being finite Function such that
A1: f in A & a in dom f by Def1;
A c= PFuncs (V, C) by FINSUB_1:def 5;
then consider f1 being Function such that
A2: f = f1 & dom f1 c= V & rng f1 c= C by A1,PARTFUN1:def 5;
thus thesis by A1,A2;
end;
Lm2:
for V being set, C be finite set,
A being non empty Element of Fin PFuncs (V, C) holds
Involved A is finite
proof
let V be set, C be finite set,
A be non empty Element of Fin PFuncs (V, C);
deffunc F(Function)=dom $1;
defpred P[set] means $1 in A & $1 is finite;
defpred Q[set] means $1 in A;
set X = { F(f) where f is Element of PFuncs(V, C) : P[f]};
A1: for g being Element of PFuncs(V, C) holds P[g] implies Q[g];
A2: X c= { F(f) where f is Element of PFuncs(V, C) : Q[f]}
from Fraenkel5'(A1);
A3: A is finite;
A4: { F(f) where f is Element of PFuncs(V, C) : f in A } is finite
from FraenkelFin(A3);
x in Involved A iff ex Y be set st x in Y & Y in X
proof
hereby assume x in Involved A;
then consider f being finite Function such that
A5: f in A & x in dom f by Def1;
A c= PFuncs (V,C) by FINSUB_1:def 5;
then dom f in X by A5;
hence ex Y be set st x in Y & Y in X by A5;
end;
given Y be set such that
A6: x in Y & Y in X;
consider f1 being Element of PFuncs(V, C) such that
A7: Y = dom f1 & f1 in A & f1 is finite by A6;
thus thesis by A6,A7,Def1;
end;
then A8: Involved A = union X by TARSKI:def 4;
A9: X is finite by A2,A4,FINSET_1:13;
for x be set st x in X holds x is finite
proof
let x be set;
assume x in X;
then consider f1 being Element of PFuncs(V, C) such that
A10: x = dom f1 & f1 in A & f1 is finite;
thus thesis by A10,AMI_1:21;
end;
hence thesis by A8,A9,FINSET_1:25;
end;
theorem Th11:
for V being set, C being finite set,
A being Element of Fin PFuncs (V, C) st A = {} holds Involved A = {}
proof
let V be set, C be finite set,
A be Element of Fin PFuncs (V, C);
assume A1: A = {};
assume Involved A <> {};
then consider x be set such that
A2: x in Involved A by XBOOLE_0:def 1;
consider f being finite Function such that
A3: f in A & x in dom f by A2,Def1;
thus thesis by A1,A3;
end;
theorem Th12:
for V being set, C being finite set,
A being Element of Fin PFuncs (V, C) holds Involved A is finite
proof
let V be set, C be finite set,
A be Element of Fin PFuncs (V, C);
per cases;
suppose A is non empty;
hence thesis by Lm2;
suppose A is empty;
hence thesis by Th11;
end;
theorem
for C being finite set,
A being Element of Fin PFuncs ({}, C) holds Involved A = {}
proof
let C be finite set,
A be Element of Fin PFuncs ({}, C);
Involved A c= {} by Th10;
hence thesis by XBOOLE_1:3;
end;
definition let V be set, C be finite set;
let A be Element of Fin PFuncs (V, C);
func -A -> Element of Fin PFuncs (V, C) equals :Def2:
{ f where f is Element of PFuncs (Involved A, C) :
for g be Element of PFuncs (V, C) st g in A holds not f tolerates g };
coherence
proof
set M = { f where f is Element of PFuncs (Involved A, C) :
for g be Element of PFuncs (V, C) st g in A holds not f tolerates g };
defpred P[Element of PFuncs (Involved A, C)] means
for h be Element of PFuncs (V, C) st h in A holds not $1 tolerates h;
defpred Q[set] means not contradiction;
A1: for v being Element of PFuncs (Involved A, C) holds P[v]
implies Q[v];
deffunc F(set)=$1;
A2: { F(f) where f is Element of PFuncs (Involved A, C) : P[f] } c=
{ F(f) where f is Element of PFuncs (Involved A, C) : Q[f] }
from Fraenkel5'(A1);
Involved A is finite by Th12;
then A3: PFuncs (Involved A, C) is finite by Th5;
{ f where f is Element of PFuncs (Involved A, C) : not contradiction } c=
PFuncs (Involved A, C)
proof
let a be set;
assume a in { f where f is Element of PFuncs (Involved A, C) :
not contradiction };
then consider f1 be Element of PFuncs (Involved A, C) such that
A4: f1 = a & not contradiction;
thus thesis by A4;
end;
then { f where f is Element of PFuncs (Involved A, C) : not contradiction }
is finite by A3,FINSET_1:13;
then A5: M is finite by A2,FINSET_1:13;
M c= PFuncs (V, C)
proof
let a be set; assume a in M;
then consider f1 be Element of PFuncs (Involved A, C) such that A6: f1 = a
&
for g be Element of PFuncs (V, C) st g in A holds not f1 tolerates g;
Involved A c= V by Th10;
then A7: PFuncs (Involved A, C) c= PFuncs (V, C) by PARTFUN1:125;
a in PFuncs (Involved A, C) by A6;
hence thesis by A7;
end;
hence thesis by A5,FINSUB_1:def 5;
end;
end;
theorem Th14:
A ^ -A = {}
proof
assume A ^ -A <> {};
then consider x be set such that
A1: x in A ^ -A by XBOOLE_0:def 1;
x in { s \/ t where s, t is Element of PFuncs (V,C) :
s in A & t in -A & s tolerates t } by A1,SUBSTLAT:def 3;
then consider s1, t1 be Element of PFuncs (V,C) such that
A2: x = s1 \/ t1 & s1 in A & t1 in -A & s1 tolerates t1;
t1 in { f where f is Element of PFuncs (Involved A, C) :
for g be Element of PFuncs (V, C) st g in A holds not f tolerates g }
by A2,Def2;
then consider f1 be Element of PFuncs (Involved A, C) such that A3: f1 = t1 &
for g be Element of PFuncs (V, C) st g in A holds not f1 tolerates g;
thus thesis by A2,A3;
end;
theorem Th15:
A = {} implies -A = { {} }
proof
assume A1: A = {};
A2:-A = { f where f is Element of PFuncs (Involved A, C) :
for g be Element of PFuncs (V, C) st g in A holds not f tolerates g }
by Def2;
defpred P[Element of PFuncs (Involved A, C)] means
for g be Element of PFuncs (V, C) st g in A holds not $1 tolerates g;
{ xx where xx is Element of PFuncs (Involved A, C) : P[xx]}
c= PFuncs (Involved A, C) from Fr_Set0;
then -A c= PFuncs ({}, C) by A1,A2,Th11;
then A3: -A c= { {} } by PARTFUN1:122;
{} in -A
proof
{} in { {} } by TARSKI:def 1;
then {} in PFuncs ({}, C) by PARTFUN1:122;
then A4: {} in PFuncs (Involved A, C) by A1,Th11;
for g be Element of PFuncs (V, C) st g in A holds not {} tolerates g by
A1
;
hence thesis by A2,A4;
end;
then { {} } c= -A by ZFMISC_1:37;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem
A = { {} } implies -A = {}
proof
assume A = {{}};
then A1:-A = { f where f is Element of PFuncs (Involved A, C) :
for g be Element of PFuncs (V, C) st g in {{}} holds not f tolerates g }
by Def2;
assume -A <> {};
then consider x1 be set such that
A2: x1 in -A by XBOOLE_0:def 1;
consider f1 being Element of PFuncs (Involved A, C) such that
A3: x1 = f1 &
for g be Element of PFuncs (V, C) st g in {{}} holds not f1 tolerates g
by A1,A2;
{} is PartFunc of V, C by PARTFUN1:56;
then A4: {} in PFuncs (V, C) by PARTFUN1:119;
A5: {} in {{}} by TARSKI:def 1;
f1 tolerates {} by PARTFUN1:141;
hence thesis by A3,A4,A5;
end;
theorem Th17:
for V being set, C being finite set
for A being Element of SubstitutionSet (V, C) holds
mi (A ^ -A) = Bottom SubstLatt (V,C)
proof
let V be set, C be finite set,
A be Element of SubstitutionSet (V, C);
A ^ -A = {} by Th14;
then mi (A ^ -A) = {} by SUBSTLAT:9
.= Bottom SubstLatt (V,C) by SUBSTLAT:26;
hence thesis;
end;
theorem
for V being non empty set, C being finite non empty set
for A being Element of SubstitutionSet (V, C) st A = {} holds
mi -A = Top SubstLatt (V,C)
proof
let V be non empty set, C be finite non empty set,
A be Element of SubstitutionSet (V, C);
assume A = {};
then A1: -A = { {} } by Th15;
then -A in SubstitutionSet (V, C) by SUBSTLAT:2;
then mi -A = { {} } by A1,SUBSTLAT:11;
hence thesis by SUBSTLAT:27;
end;
theorem Th19:
for V being set, C being finite set
for A being Element of SubstitutionSet (V, C),
a being Element of PFuncs (V, C),
B being Element of SubstitutionSet (V, C) st B = { a } holds
A ^ B = {} implies ex b being finite set st b in -A & b c= a
proof
let V, C;
let A be Element of SubstitutionSet (V, C);
let a be Element of PFuncs (V, C);
let B be Element of SubstitutionSet (V, C) such that
A1: B = { a };
assume A2: A ^ B = {};
per cases;
suppose A3: A is non empty;
then A4: A = [A] by HEYTING1:def 2;
defpred P[Element of PFuncs (V, C),set] means
$2 in dom $1 /\ dom a & $1.$2 <> a.$2;
A5: now let s be Element of PFuncs (V, C) such that
A6: s in A;
not s tolerates a
proof
assume A7: s tolerates a;
a in B by A1,TARSKI:def 1;
then s \/ a in { s1 \/ t1 where s1,t1 is Element of PFuncs (V,C) :
s1 in A & t1 in B & s1 tolerates t1 } by A6,A7;
hence thesis by A2,SUBSTLAT:def 3;
end;
then consider x be set such that
A8: x in dom s /\ dom a & s.x <> a.x by PARTFUN1:def 6;
consider a' be Function such that
A9: a' = a & dom a' c= V & rng a' c= C by PARTFUN1:def 5;
dom s /\ dom a c= dom a' by A9,XBOOLE_1:17;
then dom s /\ dom a c= V by A9,XBOOLE_1:1;
then reconsider x as Element of [V] by A8,HEYTING1:def 2;
take x;
thus P[s,x] by A8;
end;
consider g be Element of Funcs (PFuncs (V, C), [V]) such that
A10: for s be Element of PFuncs (V, C) st s in A holds
P[s,g.s] from FuncsChoice(A5);
deffunc G(set)=g.$1;
defpred P[set] means not contradiction;
reconsider AA = A as finite non empty set by A3;
{ G(b) where b is Element of AA : P[b] } is finite
from FraenkelFinIm;
then reconsider UKA = { g.b where b is Element of [A] : not contradiction }
as finite set by A4;
set f = a|UKA;
A11: rng f c= rng a by RELAT_1:99;
consider kk be Function such that
A12: kk = a & dom kk c= V & rng kk c= C by PARTFUN1:def 5;
A13: f c= kk by A12,RELAT_1:88;
A14: dom f c= Involved A
proof
let x be set;
assume x in dom f;
then x in UKA by RELAT_1:86;
then consider b be Element of [A] such that A15: x = g.b;
reconsider b as finite Function by A4,Th2;
reconsider b' = b as Element of PFuncs (V, C) by A4,SETWISEO:14;
g.b' in dom b' /\ dom a by A4,A10;
then x in dom b by A15,XBOOLE_0:def 3;
hence thesis by A4,Def1;
end;
rng f c= C by A11,A12,XBOOLE_1:1;
then reconsider f' = f as Element of PFuncs (Involved A, C)
by A14,PARTFUN1:def 5;
for g be Element of PFuncs (V, C) st g in A holds not f tolerates g
proof
let g1 be Element of PFuncs (V, C);
reconsider g' = g1 as Function;
assume A16: g1 in A;
ex z be set st z in dom g1 /\ dom f & g'.z <> f.z
proof
set z = g.g1;
A17: g1.(g.g1) <> a.(g.g1) & z in dom g1 /\ dom a by A10,A16;
A18: g1.z <> a.z by A10,A16;
A19: z in dom a & z in dom g1 by A17,XBOOLE_0:def 3;
take z;
z in { g.b1 where b1 is Element of [A] : not contradiction }
by A4,A16;
then z in dom a /\ UKA by A19,XBOOLE_0:def 3;
then A20: z in dom f by RELAT_1:90;
hence z in dom g1 /\ dom f by A19,XBOOLE_0:def 3;
thus thesis by A18,A20,FUNCT_1:70;
end;
hence thesis by PARTFUN1:def 6;
end;
then f' in { f1 where f1 is Element of PFuncs (Involved A, C) :
for g be Element of PFuncs (V, C) st g in A holds not f1 tolerates g };
then f in -A by Def2;
hence thesis by A12,A13;
suppose A is empty;
then A21: -A = {{}} by Th15;
reconsider K = {} as finite set;
take K;
thus thesis by A21,TARSKI:def 1,XBOOLE_1:2;
end;
definition let V be set, C be finite set;
let A, B be Element of Fin PFuncs (V, C);
func A =>> B -> Element of Fin PFuncs (V, C) equals :Def3:
PFuncs (V, C) /\
{ union {f.i \ i where i is Element of PFuncs (V, C) : i in A}
where f is Element of PFuncs (A, B) : dom f = A };
coherence
proof
set Z = { union {f.i \ i where i is Element of PFuncs (V, C) : i in A}
where f is Element of PFuncs (A, B) : dom f = A};
set K = PFuncs (V, C) /\ Z;
A1: K c= PFuncs (V, C) by XBOOLE_1:17;
A2: Z = { union {f.i \ i where i is Element of PFuncs (V, C) : i in A}
where f is Element of PFuncs (A, B) : f in PFuncs(A,B) & dom f = A}
proof
thus Z c= { union {f.i \ i where i is Element of PFuncs (V, C) :
i in A } where f is Element of PFuncs (A, B) : f in PFuncs(A,B)
& dom f = A }
proof
let z be set;
assume z in Z;
then consider f1 be Element of PFuncs (A, B) such that
A3: z = union {f1.i \ i where i is Element of PFuncs (V, C) :
i in A} & dom f1 = A;
thus thesis by A3;
end;
thus { union {f.i \ i where i is Element of PFuncs (V, C) :
i in A} where f is Element of PFuncs (A, B) : f in PFuncs(A,B)
& dom f = A } c= Z
proof
let z be set;
assume z in { union {f.i \ i where i is Element of PFuncs (V, C) :
i in A} where f is Element of PFuncs (A, B) : f in PFuncs(A,B) &
dom f = A};
then consider f1 be Element of PFuncs (A, B) such that
A4: z = union {f1.i \ i where i is Element of PFuncs (V, C) : i in A}
& f1 in PFuncs (A, B) & dom f1 = A;
thus thesis by A4;
end;
end;
reconsider PF = PFuncs (A, B) as functional finite non empty set
by Th5;
deffunc F(Element of PF)=
union {$1.i \ i where i is Element of PFuncs (V, C) : i in A};
defpred P[Element of PF] means $1 in PFuncs(A,B) & dom $1 = A;
{ F(f) where f is Element of PF : P[f]}
is finite from FraenkelFinIm;
then K is finite by A2,FINSET_1:15;
hence thesis by A1,FINSUB_1:def 5;
end;
end;
theorem Th20:
for A, B being Element of Fin PFuncs (V, C), s being set st
s in A =>> B holds
ex f being PartFunc of A, B st
s = union {f.i \ i where i is Element of PFuncs (V, C) : i in A}
& dom f = A
proof
let A, B be Element of Fin PFuncs (V, C), s be set;
assume s in A =>> B;
then s in PFuncs (V, C) /\
{ union {f.i \ i where i is Element of PFuncs (V, C) : i in A}
where f is Element of PFuncs (A, B) : dom f = A } by Def3;
then s in { union {f.i \ i where i is Element of PFuncs (V, C) : i in A}
where f is Element of PFuncs (A, B) : dom f = A} by XBOOLE_0:def 3;
then consider f be Element of PFuncs (A, B) such that
A1: s = union {f.i \ i where i is Element of PFuncs (V, C) : i in A}
& dom f = A;
f is PartFunc of A, B by PARTFUN1:121;
hence thesis by A1;
end;
Lm3:
for V be set, C be finite set,
A be Element of Fin PFuncs (V, C),
K be Element of SubstitutionSet (V, C) holds
a in A ^ (A =>> K) implies ex b st b in K & b c= a
proof
let V be set, C be finite set,
A be Element of Fin PFuncs (V, C),
K be Element of SubstitutionSet (V, C);
assume a in A ^ (A =>> K); then consider b,c be set such that
A1: b in A and
A2: c in A =>> K and
A3: a = b \/ c by SUBSTLAT:15;
consider f be PartFunc of A, K such that
A4: c = union {f.i \ i where i is Element of PFuncs (V, C) : i in A }
& dom f = A by A2,Th20;
A5: f.b in K by A1,A4,PARTFUN1:27;
K c= PFuncs (V, C) by FINSUB_1:def 5;
then reconsider d = f.b as Element of PFuncs (V, C) by A5;
take d;
thus d in K by A1,A4,PARTFUN1:27;
A c= PFuncs (V, C) by FINSUB_1:def 5;
then reconsider b' = b as Element of PFuncs (V, C) by A1;
d \ b' in {f.i \ i where i is Element of PFuncs (V, C) : i in A} by A1;
then d \ b c= c by A4,ZFMISC_1:92;
hence d c= a by A3,XBOOLE_1:44;
end;
theorem
for V being set, C being finite set, A being Element of Fin PFuncs (V, C)
st A = {} holds A =>> A = {{}}
proof
let V be set, C be finite set, A be Element of Fin PFuncs (V, C);
assume A1: A = {};
defpred P[Function] means dom $1 = A;
deffunc F(Element of PFuncs (A, A))=
union {$1.i \ i where i is Element of PFuncs (V, C) : i in A};
deffunc G(set)={};
now let f be Element of PFuncs (A, A);
not ex x be set st x in
{f.i \ i where i is Element of PFuncs (V, C) : i in A}
proof
given x be set such that
A2: x in {f.i \ i where i is Element of PFuncs (V, C) : i in A};
consider x1 being Element of PFuncs (V, C) such that
A3: x = f.x1 \ x1 & x1 in A by A2;
thus contradiction by A1,A3;
end;
hence {f.i \ i where i is Element of PFuncs (V, C) : i in A} = {}
by XBOOLE_0:def 1;
end;
then A4: for v being Element of PFuncs (A, A) st P[v] holds F(v) = G(v)
by ZFMISC_1:2;
A5:{ F(f) where f is Element of PFuncs (A, A) : P[f]}
= { G(f) where f is Element of PFuncs (A, A) : P[f] }
from FraenkelF'R (A4);
A6: ex a being Element of PFuncs (A, A) st P[a]
proof
reconsider e = id A as Element of PFuncs (A, A) by PARTFUN1:119;
take e;
thus thesis by RELAT_1:71;
end;
A7: { {} where f is Element of PFuncs (A, A) : P[f] } = {{}}
from SingleFraenkel (A6);
{} is PartFunc of V,C by PARTFUN1:56;
then {} in PFuncs (V,C) by PARTFUN1:119;
then A8: {{}} c= PFuncs (V,C) by ZFMISC_1:37;
A =>> A = PFuncs (V,C) /\ {{}} by A5,A7,Def3
.= {{}} by A8,XBOOLE_1:28;
hence thesis;
end;
reserve u, v for Element of SubstLatt (V, C);
reserve s, t, a, b for Element of PFuncs (V,C);
reserve K, L for Element of SubstitutionSet (V, C);
Lm4:
for X being set st X c= K holds X in SubstitutionSet (V, C)
proof let X be set;
assume
A1: X c= K;
K c= PFuncs (V, C) & K is finite by FINSUB_1:def 5;
then X c= PFuncs (V, C) & X is finite by A1,FINSET_1:13,XBOOLE_1:1;
then reconsider B = X as Element of Fin PFuncs (V, C) by FINSUB_1:def 5;
A2: for x be set st x in X holds x is finite by A1,Th2;
for a,b st a in B & b in B & a c= b holds a = b by A1,SUBSTLAT:5;
then X in { A where A is Element of Fin PFuncs (V,C) :
( for u being set st u in A holds u is finite ) &
for s, t being Element of PFuncs (V, C) holds
( s in A & t in A & s c= t implies s = t ) } by A2;
hence X in SubstitutionSet (V, C) by SUBSTLAT:def 1;
end;
theorem Th22:
for X being set st X c= u holds
X is Element of SubstLatt (V, C)
proof let X be set;
reconsider u' = u as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4;
assume X c= u;
then X c= u';
then X in SubstitutionSet (V, C) by Lm4;
hence X is Element of SubstLatt (V, C) by SUBSTLAT:def 4;
end;
begin :: Lattice of substitutions is implicative
definition let V, C;
func pseudo_compl (V, C) -> UnOp of the carrier of SubstLatt (V, C) means
:Def4: for u' being Element of SubstitutionSet (V, C) st u' = u holds
it.u = mi(-u');
existence
proof
deffunc F(Element of SubstitutionSet (V, C))=mi(-$1);
consider IT being Function of SubstitutionSet (V, C),
SubstitutionSet (V, C) such that
A1: for u being Element of SubstitutionSet (V, C) holds
IT.u = F(u) from LambdaD;
SubstitutionSet (V, C) = the carrier of SubstLatt (V, C)
by SUBSTLAT:def 4;
then reconsider IT as UnOp of the carrier of SubstLatt (V, C);
take IT;
thus thesis by A1;
end;
correctness
proof
let IT,IT' be UnOp of the carrier of SubstLatt (V, C);
assume that
A2: for u' being Element of SubstitutionSet (V, C) st u' = u holds
IT.u = mi (-u') and
A3: for u' being Element of SubstitutionSet (V, C) st u' = u holds
IT'.u = mi (-u');
now let u;
reconsider u' = u as Element of SubstitutionSet (V, C)
by SUBSTLAT:def 4;
thus IT.u = mi (-u') by A2 .= IT'.u by A3;
end;
hence IT = IT' by FUNCT_2:113;
end;
func StrongImpl(V, C) -> BinOp of the carrier of SubstLatt (V, C) means
:Def5: for u', v' being Element of SubstitutionSet (V, C) st u' = u & v' = v
holds
it.(u,v) = mi (u' =>> v');
existence
proof
defpred P[set, set, set] means
for u', v' being Element of SubstitutionSet (V, C) st u' = $1 & v' = $2
holds $3 = mi (u' =>> v');
set ZA = the carrier of SubstLatt (V, C);
A4: for x,y being Element of ZA ex z being Element of ZA st P[x,y,z]
proof
let x,y be Element of ZA;
reconsider x' = x, y' = y as Element of SubstitutionSet (V, C)
by SUBSTLAT:def 4;
reconsider z = mi (x' =>> y') as Element of ZA by SUBSTLAT:def 4;
take z;
let u', v' be Element of SubstitutionSet (V, C);
assume u' = x & v' = y;
hence thesis;
end;
consider o being BinOp of the carrier of SubstLatt (V, C) such that
A5: for a,b being Element of SubstLatt (V, C) holds
P[a,b,o.(a,b)] from BinOpEx(A4);
take o;
let u,v;
let u', v' be Element of SubstitutionSet (V, C);
assume u' = u & v' = v;
hence o.(u,v) = mi (u' =>> v') by A5;
end;
correctness
proof let IT1,IT2 be BinOp of the carrier of SubstLatt (V, C);
assume that
A6: for u', v' being Element of SubstitutionSet (V, C) st u' = u & v' = v
holds IT1.(u,v) = mi (u' =>> v') and
A7: for u', v' being Element of SubstitutionSet (V, C) st u' = u & v' = v
holds IT2.(u,v) = mi (u' =>> v');
now let u, v;
reconsider u' = u, v' = v as Element of SubstitutionSet (V, C)
by SUBSTLAT:def 4;
thus IT1.(u,v) = mi (u' =>> v') by A6
.= IT2.(u,v) by A7;
end;
hence IT1 = IT2 by BINOP_1:2;
end;
let u;
func SUB u -> Element of Fin the carrier of SubstLatt (V, C) equals
:Def6: bool u;
coherence
proof
reconsider u' = u as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4;
u' is finite;
then A8: bool u is finite by FINSET_1:24;
bool u c= the carrier of SubstLatt (V, C)
proof let x be set;
assume x in bool u;
then x is Element of SubstLatt (V, C) by Th22;
hence thesis;
end;
hence thesis by A8,FINSUB_1:def 5;
end;
correctness;
func diff(u) -> UnOp of the carrier of SubstLatt (V, C) means
:Def7: it.v = u \ v;
existence
proof
u in the carrier of SubstLatt (V, C);
then A9: u in SubstitutionSet (V, C) by SUBSTLAT:def 4;
deffunc F(set)=u \ $1;
consider IT being Function such that
A10: dom IT = the carrier of SubstLatt (V, C) &
for v be set st v in
the carrier of SubstLatt (V, C) holds IT.v = F(v) from Lambda;
for x be set st x in the carrier of SubstLatt (V, C) holds
IT.x in Fin PFuncs (V, C)
proof
let x be set; assume x in the carrier of SubstLatt (V, C);
then A11: IT.x = u \ x by A10;
u \ x c= u by XBOOLE_1:36;
then u \ x in SubstitutionSet (V,C) by A9,Lm4;
hence thesis by A11;
end;
then reconsider IT as Function of the carrier of SubstLatt (V, C),
Fin PFuncs (V, C) by A10,FUNCT_2:5;
now let v be Element of SubstLatt (V, C);
u \ v c= u by XBOOLE_1:36;
then u \ v in SubstitutionSet (V,C) by A9,Lm4;
then IT.v in SubstitutionSet (V,C) by A10;
hence IT.v in the carrier of SubstLatt (V, C) by SUBSTLAT:def 4;
end;
then reconsider IT as UnOp of the carrier of SubstLatt (V, C)
by HEYTING1:1;
take IT; let v;
thus IT.v = u \ v by A10;
end;
correctness
proof
let IT,IT' be UnOp of the carrier of SubstLatt (V, C);
assume that
A12: IT.v = u \ v and
A13: IT'.v = u \ v;
now let v be Element of SubstLatt (V, C);
thus IT.v = u \ v by A12
.= IT'.v by A13;
end;
hence IT = IT' by FUNCT_2:113;
end;
end;
Lm5: v in SUB u implies v "\/" (diff u).v = u
proof
assume v in SUB u;
then A1: v in bool u by Def6;
A2: u \ v = (diff u).v by Def7;
reconsider u' = u, v' = v, dv = (diff u).v
as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4;
thus v "\/" (diff u).v = (the L_join of SubstLatt (V,C)).(v, (diff u).v)
by LATTICES:def 1
.= mi ( v' \/ dv ) by SUBSTLAT:def 4
.= mi u' by A1,A2,XBOOLE_1:45
.= u by SUBSTLAT:11;
end;
Lm6: for K be Element of Fin PFuncs (V, C) st a is finite & K = {a} holds
ex v be Element of SubstitutionSet (V,C) st
v in SUB u & v ^ K = {} &
for b st b in (diff u).v holds b tolerates a
proof
let K be Element of Fin PFuncs (V, C) such that A1: a is finite &
K = {a};
defpred P[Element of PFuncs (V, C)] means
$1 is finite & not $1 tolerates a;
deffunc F(set)=$1;
set M = { F(s) where s is Element of PFuncs (V, C):
F(s) in u & P[s] };
A2: M c= u from FrSet_1;
then reconsider v = M as Element of SubstLatt (V, C)
by Th22;
reconsider v as Element of SubstitutionSet (V,C) by SUBSTLAT:def 4;
take v;
v in bool u by A2;
hence v in SUB u by Def6;
deffunc F(Element of PFuncs (V, C),Element of PFuncs (V, C))=$1 \/ $2;
defpred P[Element of PFuncs (V, C),Element of PFuncs (V, C)] means
$1 in M & $2 in { a } & $1 tolerates $2;
defpred Q[Element of PFuncs (V, C),Element of PFuncs (V, C)] means
$2 = a & $1 in M & $1 tolerates $2;
A3: P[s,t] iff Q[s,t] by TARSKI:def 1;
A4: { F(s,t): P[s,t] } =
{ F(s',t') where s', t' is Element of PFuncs (V, C) :
Q[s',t'] } from Fraenkel6''(A3);
defpred P[Element of PFuncs (V, C)] means
$1 in M & $1 tolerates a;
defpred Q[Element of PFuncs (V, C)] means
not $1 tolerates a & $1 in u & $1 tolerates a;
s in M iff s is finite & not s tolerates a & s in u
proof
thus s in M implies s is finite & not s tolerates a & s in u
proof
assume s in M;
then consider s2 be Element of PFuncs (V, C) such that
A5: s2 = s & s2 in u & s2 is finite & not s2 tolerates a;
thus thesis by A5;
end;
thus s is finite & not s tolerates a & s in u implies s in M;
end;
then A6: P[s] iff Q[s];
deffunc F1(Element of PFuncs (V, C),Element of PFuncs (V, C))=$1 \/ $2;
defpred P1[Element of PFuncs (V, C),Element of PFuncs (V, C)] means
$1 in M & $1 tolerates $2;
A7: { F1(s,t) where t is Element of PFuncs (V, C)
: t = a & P1[s,t]} =
{ F1(s',a) where s' is Element of PFuncs (V, C) : P1[s',a]}
from FrEqua2;
deffunc F(Element of PFuncs (V, C))=$1 \/ a;
{ F(s') where s' is Element of PFuncs (V, C) : P[s']} =
{ F(s): Q[s]}
from Fraenkel6'(A6);
then A8: v ^ K = { s \/ a: not s tolerates a & s in u & s tolerates a }
by A1,A4,A7,SUBSTLAT:def 3;
thus v ^ K = {}
proof
assume v ^ K <> {};
then consider x be set such that A9: x in v ^ K by XBOOLE_0:def 1;
consider s1 be Element of PFuncs (V, C) such that
A10: x = s1 \/ a & not s1 tolerates a & s1 in u & s1 tolerates a
by A8,A9;
thus thesis by A10;
end;
let b;
assume b in (diff u).v;
then b in u \ v by Def7;
then A11: b in u & not b in M by XBOOLE_0:def 4;
u in the carrier of SubstLatt (V, C);
then u in SubstitutionSet (V, C) by SUBSTLAT:def 4;
then b is finite by A11,Th2;
hence b tolerates a by A11;
end;
definition let V, C;
func Atom(V, C) -> Function of PFuncs (V, C), the carrier of SubstLatt (V, C)
means
:Def8: for a being Element of PFuncs (V,C) holds it.a = mi { a };
existence
proof
A1: the carrier of SubstLatt (V, C) = SubstitutionSet (V, C)
by SUBSTLAT:def 4;
deffunc F(Element of PFuncs (V, C))= mi {$1};
consider f be Function of PFuncs (V, C), SubstitutionSet (V, C)
such that
A2: for a be Element of PFuncs (V, C) holds f.a = F(a) from LambdaD;
A3: now let x be set;
assume x in PFuncs (V, C);
then reconsider a = x as Element of PFuncs (V, C);
f.a = mi { a } by A2;
hence f.x in the carrier of SubstLatt (V, C) by A1;
end;
dom f = PFuncs (V, C) by FUNCT_2:def 1;
then reconsider f as Function of PFuncs (V, C), the carrier of SubstLatt (V
, C)
by A3,FUNCT_2:5;
take f; thus thesis by A2;
end;
correctness
proof let IT1,IT2 be
Function of PFuncs (V, C), the carrier of SubstLatt (V, C) such that
A4: (for a holds IT1.a = mi { a }) & for a holds IT2.a = mi { a };
now let a;
IT1.a = mi { a } & IT2.a = mi { a } by A4;
hence IT1.a = IT2.a;
end;
hence thesis by FUNCT_2:113;
end;
end;
Lm7:
for a be Element of PFuncs (V, C) st a is finite holds Atom (V, C).a = {a}
proof
let a be Element of PFuncs (V, C);
assume A1: a is finite;
{ a } in SubstitutionSet (V, C)
proof
A2: for u being set st u in { a } holds u is finite by A1,TARSKI:def 1;
for s, t being Element of PFuncs (V,C) holds
( s in { a } & t in { a } & s c= t implies s = t )
proof
let s, t be Element of PFuncs (V,C);
assume s in { a } & t in { a } & s c= t;
then s = a & t = a by TARSKI:def 1;
hence s = t;
end;
then { a } in { A where A is Element of Fin PFuncs (V,C) :
( for u being set st u in A holds u is finite ) &
for s, t being Element of PFuncs (V, C) holds
( s in A & t in A & s c= t implies s = t ) } by A2;
hence thesis by SUBSTLAT:def 1;
end;
then {a} = mi {a} by SUBSTLAT:11
.= Atom (V, C).a by Def8;
hence thesis;
end;
theorem Th23:
FinJoin (K, Atom(V, C)) = FinUnion(K, singleton PFuncs (V, C))
proof
A1: the L_join of SubstLatt (V, C) is commutative by LATTICE2:27;
A2: the L_join of SubstLatt (V, C) is associative by LATTICE2:29;
A3: the L_join of SubstLatt (V, C) is idempotent by LATTICE2:26;
A4: the L_join of SubstLatt (V, C) has_a_unity by LATTICE2:67;
deffunc F(Element of Fin PFuncs (V, C))= mi $1;
consider g being Function of Fin PFuncs (V, C), SubstitutionSet (V,C)
such that
A5: for B be Element of Fin PFuncs (V, C) holds g.B = F(B) from LambdaD;
the carrier of SubstLatt (V, C) = SubstitutionSet (V,C) by SUBSTLAT:def 4
;
then reconsider g as Function of Fin PFuncs (V, C),
the carrier of SubstLatt (V, C);
A6: g.{}.PFuncs (V, C) = mi {}.PFuncs (V, C) by A5
.= {} by SUBSTLAT:9
.= Bottom SubstLatt (V, C) by SUBSTLAT:26
.= the_unity_wrt the L_join of SubstLatt (V, C)
by A4,LATTICE2:28;
A7: now let x,y be Element of Fin PFuncs (V, C);
A8: g.x = mi x by A5;
A9: g.y = mi y by A5;
thus g.(x \/ y) = mi (x \/ y) by A5
.= mi (mi x \/ y) by SUBSTLAT:13
.= mi (mi x \/ mi y) by SUBSTLAT:13
.= (the L_join of SubstLatt (V, C)).(g.x,g.y)
by A8,A9,SUBSTLAT:def 4;
end;
A10: K c= PFuncs (V, C) by FINSUB_1:def 5;
then A11: K c= dom (Atom(V, C)) by FUNCT_2:def 1;
A12: dom singleton PFuncs (V, C) = PFuncs (V, C) by FUNCT_2:def 1;
A13: rng singleton PFuncs (V, C) c= Fin PFuncs (V, C);
dom g = Fin PFuncs (V, C) by FUNCT_2:def 1;
then dom ((g*singleton PFuncs (V, C))) = dom singleton PFuncs (V, C)
by A13,RELAT_1:46;
then A14: dom (Atom(V, C)|K) = K & dom ((g*singleton PFuncs (V, C))|K) = K
by A10,A11,A12,RELAT_1:91;
now let a be set; assume A15: a in K;
then reconsider a' = a as Element of PFuncs (V, C) by SETWISEO:14;
A16: a' is finite by A15,Th2;
then reconsider KL = {a'} as Element of SubstitutionSet (V,C) by Th6;
thus ((g*singleton PFuncs (V, C))|K).a
= (g*singleton PFuncs (V, C)).a by A15,FUNCT_1:72
.= g.(singleton PFuncs (V, C) .a') by FUNCT_2:21
.= g.{a} by SETWISEO:67
.= mi KL by A5
.= KL by SUBSTLAT:11
.= Atom (V, C).a' by A16,Lm7
.= (Atom (V, C)|K).a by A15,FUNCT_1:72;
end;
then A17: Atom(V, C)|K = (g*singleton PFuncs (V, C))|K by A14,FUNCT_1:9;
A18: mi (FinUnion(K,singleton PFuncs (V, C)))
c= FinUnion(K,singleton PFuncs (V, C)) by SUBSTLAT:8;
A19: FinUnion(K,singleton PFuncs (V, C))
c= mi (FinUnion(K,singleton PFuncs (V, C)))
proof let a be set;
assume
A20: a in FinUnion(K,singleton PFuncs (V, C));
then consider b be Element of PFuncs (V, C) such that
A21: b in K and
A22: a in (singleton PFuncs (V, C)).b by SETWISEO:70;
A23: a = b by A22,SETWISEO:68;
then A24: a is finite by A21,Th2;
now let s be finite set;
assume that
A25: s in FinUnion(K,singleton PFuncs (V, C)) and
A26: s c= a;
consider t such that
A27: t in K and
A28: s in (singleton PFuncs (V, C)).t by A25,SETWISEO:70;
A29: s = t by A28,SETWISEO:68;
K in SubstitutionSet (V, C);
then K in { A where A is Element of Fin PFuncs (V,C) :
( for u being set st u in A holds u is finite ) &
for s, t being Element of PFuncs (V, C) holds
( s in A & t in A & s c= t implies s = t ) } by SUBSTLAT:def 1;
then ex AA be Element of Fin PFuncs (V,C) st
K = AA & ( for u being set st u in AA holds u is finite ) &
for s, t being Element of PFuncs (V, C) holds
( s in AA & t in AA & s c= t implies s = t );
hence s = a by A21,A23,A26,A27,A29;
end;
hence a in
mi (FinUnion(K,singleton PFuncs (V, C))) by A20,A24,SUBSTLAT:7;
end;
reconsider gs = g*singleton PFuncs (V, C) as
Function of PFuncs (V, C), the carrier of SubstLatt (V, C) by FUNCT_2:19;
thus FinJoin(K, Atom (V, C)) = FinJoin(K, gs) by A17,LATTICE2:69
.= (the L_join of SubstLatt (V, C)) $$(K,gs)
by LATTICE2:def 3
.= g.(FinUnion(K,singleton PFuncs (V, C)))
by A1,A2,A3,A4,A6,A7,SETWISEO:65
.= mi (FinUnion(K,singleton PFuncs (V, C))) by A5
.= FinUnion(K,singleton PFuncs (V, C)) by A18,A19,XBOOLE_0:def 10;
end;
theorem Th24:
for u being Element of SubstitutionSet (V, C) holds
u = FinJoin(u, Atom (V, C))
proof
let u be Element of SubstitutionSet (V, C);
thus u = FinUnion(u, singleton PFuncs (V, C)) by SETWISEO:71
.= FinJoin(u, Atom(V, C)) by Th23;
end;
Lm8: (for a be set st a in u ex b be set st b in v & b c= a) implies u [= v
proof assume
A1: for a be set st a in u ex b be set st b in v & b c= a;
reconsider u' = u, v' = v as Element of SubstitutionSet (V, C)
by SUBSTLAT:def 4;
u "/\" v = (the L_meet of SubstLatt (V, C)).(u', v') by LATTICES:def 2
.= mi (u' ^ v') by SUBSTLAT:def 4
.= u' by A1,Th9;
hence u [= v by LATTICES:21;
end;
theorem Th25:
(diff u).v [= u
proof (diff u).v = u \ v by Def7;
then (diff u).v c= u by XBOOLE_1:36;
then for a be set st a in (diff u).v ex b be set st b in u & b c= a;
hence thesis by Lm8;
end;
theorem Th26:
for a being Element of PFuncs (V, C) st a is finite
for c being set st c in Atom(V, C).a holds c = a
proof
let a be Element of PFuncs (V, C);
assume a is finite;
then Atom(V, C).a = { a } by Lm7;
hence thesis by TARSKI:def 1;
end;
theorem Th27:
for a being Element of PFuncs (V, C) st
K = {a} & L = u & L ^ K = {} holds Atom(V, C).a [= pseudo_compl(V, C).u
proof
let a be Element of PFuncs (V, C);
assume
A1: K = {a} & L = u & L ^ K = {};
then a in K by TARSKI:def 1;
then A2: a is finite by Th2;
now let c be set;
assume A3: c in Atom(V, C).a;
then A4: c = a by A2,Th26;
reconsider c' = c as Element of PFuncs (V, C) by A2,A3,Th26;
consider b be finite set such that
A5: b in -L and
A6: b c= c' by A1,A4,Th19;
consider d be set such that
A7: d c= b and
A8: d in mi(-L) by A5,SUBSTLAT:10;
take e = d;
thus e in pseudo_compl(V, C).u by A1,A8,Def4;
thus e c= c by A6,A7,XBOOLE_1:1;
end;
hence Atom(V, C).a [= pseudo_compl(V, C).u by Lm8;
end;
theorem Th28:
for a being finite Element of PFuncs (V,C) holds a in Atom(V, C).a
proof
let a be finite Element of PFuncs (V,C);
Atom(V, C).a = { a } by Lm7;
hence thesis by TARSKI:def 1;
end;
Lm9: u [= v implies for x be set st x in u ex b be set st b in v & b c= x
proof
reconsider u' = u, v' = v as Element of SubstitutionSet (V, C)
by SUBSTLAT:def 4;
assume u [= v;
then u = u "/\" v by LATTICES:21
.= (the L_meet of SubstLatt (V, C)).(u,v) by LATTICES:def 2
.= mi (u' ^ v') by SUBSTLAT:def 4;
hence thesis by Th8;
end;
theorem Th29:
for u, v being Element of SubstitutionSet (V, C) holds
((for c being set st c in u ex b being set st b in v & b c= c \/ a)
implies ex b being set st b in u =>> v & b c= a )
proof
let u, v be Element of SubstitutionSet (V, C);
reconsider u' = u as Element of SubstLatt (V, C)
by SUBSTLAT:def 4;
assume that
A1: for b be set st b in u ex c be set st c in v & c c= b \/ a;
defpred P[set,set] means $2 in v & $2 c= $1 \/ a;
A2: now let b be Element of PFuncs (V, C); assume b in u;
then consider c be set such that
A3: c in v & c c= b \/ a by A1;
v c= PFuncs (V, C) by FINSUB_1:def 5;
then reconsider c as Element of PFuncs (V, C) by A3;
take x = c;
thus P[b,x] by A3;
end;
consider f' be Element of Funcs(PFuncs (V, C), PFuncs (V, C)) such that
A4: b in u implies P[b,f'.b] from FuncsChoice(A2);
consider f2 be Function such that
A5: f' = f2 & dom f2 = PFuncs (V, C) & rng f2 c= PFuncs (V, C)
by FUNCT_2:def 2;
set g = f'|u;
A6: for b be set st b in u' holds g.b c= b \/ a
proof
let b be set; assume A7: b in u';
u c= PFuncs (V, C) by FINSUB_1:def 5;
then reconsider b' = b as Element of PFuncs (V, C) by A7;
g.b' = f2.b' by A5,A7,FUNCT_1:72;
hence thesis by A4,A5,A7;
end;
A8: for b be set st b in u holds g.b in v
proof
let b be set; assume A9: b in u;
u c= PFuncs (V, C) by FINSUB_1:def 5;
then reconsider b' = b as Element of PFuncs (V, C) by A9;
g.b' = f2.b' by A5,A9,FUNCT_1:72;
hence thesis by A4,A5,A9;
end;
u c= PFuncs (V, C) by FINSUB_1:def 5;
then g is Function of u, PFuncs (V, C) by FUNCT_2:38;
then A10: dom g = u by FUNCT_2:def 1;
then g is Function of u, v by A8,FUNCT_2:5;
then rng g c= v by RELSET_1:12;
then reconsider g as Element of PFuncs (u, v) by A10,PARTFUN1:def 5;
set d = union {g.i \ i where i is Element of PFuncs (V, C) : i in u'};
A11: d c= a
proof
let x be set; assume x in d;
then consider Y be set such that
A12: x in Y &
Y in {g.i \ i where i is Element of PFuncs (V, C) : i in u'}
by TARSKI:def 4;
consider j be Element of PFuncs (V, C) such that
A13: Y = g.j \ j & j in u' by A12;
g.j c= j \/ a by A6,A13;
then g.j \j c= a by XBOOLE_1:43;
hence thesis by A12,A13;
end;
then reconsider d as Element of PFuncs (V, C) by Th3;
take d;
d in { union {f.i \ i where i is Element of PFuncs (V, C) : i in u}
where f is Element of PFuncs (u, v) : dom f = u } by A10;
then d in PFuncs (V, C) /\
{ union {f.i \ i where i is Element of PFuncs (V, C) : i in u}
where f is Element of PFuncs (u, v)
: dom f = u } by XBOOLE_0:def 3;
hence d in u =>> v by Def3;
thus thesis by A11;
end;
theorem Th30:
for a being finite Element of PFuncs (V,C) st
(for b being Element of PFuncs (V, C) st b in u holds b tolerates a ) &
u "/\" Atom(V, C).a [= v
holds Atom(V, C).a [= StrongImpl(V, C).(u, v)
proof
let a be finite Element of PFuncs (V,C);
assume that
A1: for b be Element of PFuncs (V, C) st b in u holds b tolerates a
and
A2: u "/\" Atom(V, C).a [= v;
reconsider u' = u, v' = v, Aa = (Atom(V, C).a)
as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4;
A3: now let c be set;
assume
A4: c in u;
then A5: c in u';
then reconsider c' = c as Element of PFuncs (V, C) by SETWISEO:14;
A6: a in Aa by Th28;
A7: c' tolerates a by A1,A4;
c is finite by A5,Th2;
then A8: c \/ a is finite by FINSET_1:14;
c \/ a in { s1 \/ t1 where s1,t1 is Element of PFuncs (V,C) :
s1 in u' & t1 in Aa & s1 tolerates t1 } by A4,A6,A7;
then c \/ a in u' ^ Aa by SUBSTLAT:def 3;
then consider b be set such that
A9: b c= c \/ a and
A10: b in mi(u' ^ Aa) by A8,SUBSTLAT:10;
b in (the L_meet of SubstLatt (V, C)).(u, Atom(V, C).a)
by A10,SUBSTLAT:def 4;
then b in u "/\" (Atom (V, C).a) by LATTICES:def 2;
then consider d be set such that
A11: d in v and
A12: d c= b by A2,Lm9;
take e = d;
thus e in v by A11;
thus e c= c \/ a by A9,A12,XBOOLE_1:1;
end;
now let c be set;
assume A13: c in Atom(V, C).a;
then c = a by Th26;
then consider b be set such that
A14: b in u' =>> v' and
A15: b c= c by A3,Th29;
c in Aa by A13;
then c is finite by Th2;
then b is finite by A15,FINSET_1:13;
then consider d be set such that
A16: d c= b and
A17: d in mi(u' =>> v') by A14,SUBSTLAT:10;
take e = d;
thus e in (StrongImpl(V, C).(u, v)) by A17,Def5;
thus e c= c by A15,A16,XBOOLE_1:1;
end;
hence Atom(V, C).a [= StrongImpl(V, C).(u, v) by Lm8;
end;
deffunc M(set, set) = the L_meet of SubstLatt ($1, $2);
theorem Th31:
u "/\" pseudo_compl(V, C).u = Bottom SubstLatt (V, C)
proof
reconsider u' = u as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4;
thus u "/\" pseudo_compl(V, C).u =
M(V, C).(u, pseudo_compl(V, C).u) by LATTICES:def 2
.= M(V, C).(u, mi(-u')) by Def4
.= mi(u' ^ mi(-u')) by SUBSTLAT:def 4
.= mi(u' ^ -u') by SUBSTLAT:20
.= Bottom SubstLatt (V, C) by Th17;
end;
theorem Th32:
u "/\" StrongImpl(V, C).(u, v) [= v
proof
now let a be set;
reconsider u' = u, v' = v as Element of SubstitutionSet (V, C)
by SUBSTLAT:def 4;
A1: u "/\" StrongImpl(V, C).(u, v)
= M(V, C).(u, StrongImpl(V, C).(u, v)) by LATTICES:def 2
.= M(V, C).(u, mi(u' =>> v')) by Def5
.= mi(u' ^ mi(u' =>> v')) by SUBSTLAT:def 4
.= mi(u' ^ (u' =>> v')) by SUBSTLAT:20;
assume a in u "/\" StrongImpl(V, C).(u, v);
then a in u' ^ (u' =>> v') by A1,SUBSTLAT:6;
hence ex b be set st b in v & b c= a by Lm3;
end;
hence thesis by Lm8;
end;
Lm10:
now let V, C, u, v;
deffunc IMPL(Element of SubstLatt (V, C),
Element of SubstLatt (V, C))
= FinJoin(SUB $1,
M(V, C).:(pseudo_compl(V, C), StrongImpl(V, C)[:](diff $1, $2)));
set Psi = M(V, C).:(pseudo_compl(V, C), StrongImpl(V, C)[:](diff u, v));
A1: now let w be Element of SubstLatt (V, C);
set u2 = (diff u).w,
pc = pseudo_compl(V, C).w,
si = StrongImpl(V, C).(u2, v);
assume w in SUB u;
then A2: w "\/" u2 = u by Lm5;
A3: w "/\" (pc "/\" si) = (w "/\" pc) "/\" si by LATTICES:def 7
.= Bottom SubstLatt (V, C) "/\" si by Th31
.= Bottom SubstLatt (V, C) by LATTICES:40;
A4: u2 "/\" si [= v by Th32;
M(V, C)[;](u, Psi).w = M(V, C).(u, Psi.w) by FUNCOP_1:66
.= u "/\" Psi.w by LATTICES:def 2
.= u "/\" M(V, C).(pc, StrongImpl(V, C)[:](diff u, v).w) by FUNCOP_1:48
.= u "/\" (pc "/\" StrongImpl(V, C)[:](diff u, v).w) by LATTICES:def 2
.= u "/\" (pc "/\" si) by FUNCOP_1:60
.= (w "/\" (pc "/\" si)) "\/" (u2 "/\" (pc "/\"
si)) by A2,LATTICES:def 11
.= u2 "/\" (si "/\" pc) by A3,LATTICES:39
.= (u2 "/\" si) "/\" pc by LATTICES:def 7;
then M(V, C)[;](u, Psi).w [= u2 "/\" si by LATTICES:23;
hence M(V, C)[;](u, Psi).w [= v by A4,LATTICES:25;
end;
u "/\" IMPL(u,v) = FinJoin(SUB u, M(V, C)[;](u, Psi)) by LATTICE2:83;
hence u "/\" IMPL(u,v) [= v by A1,LATTICE2:70;
let w be Element of SubstLatt (V, C);
reconsider v' = v as Element of SubstitutionSet (V, C)
by SUBSTLAT:def 4;
A5: v = FinJoin(v', Atom(V, C)) by Th24;
then A6: u "/\" v = FinJoin(v', M(V, C)[;](u, Atom(V, C))) by LATTICE2:83;
assume
A7: u "/\" v [= w;
now let a be Element of PFuncs (V, C);
assume A8: a in v';
then M(V, C)[;](u, Atom(V, C)).a [= w by A6,A7,LATTICE2:46;
then M(V, C).(u, Atom(V, C).a) [= w by FUNCOP_1:66;
then A9: u "/\" Atom(V, C).a [= w by LATTICES:def 2;
reconsider SA = {a} as Element of Fin PFuncs (V, C);
A10: a is finite by A8,Th2;
then reconsider SS = {a} as Element of SubstitutionSet (V, C) by Th6;
consider v be Element of SubstitutionSet (V, C) such that
A11: v in SUB u and
A12: v ^ SA = {} and
A13: for b be Element of PFuncs (V, C) st
b in (diff u).v holds b tolerates a by A10,Lm6;
A14: v ^ SS = {} by A12;
reconsider v' = v as Element of SubstLatt (V, C)
by SUBSTLAT:def 4;
set dv = (diff u).v';
dv [= u by Th25;
then dv "/\" Atom(V, C).a [= u "/\" Atom(V, C).a
by LATTICES:27;
then A15: dv "/\" Atom(V, C).a [= w by A9,LATTICES:25;
set pf = pseudo_compl(V, C),
sf = StrongImpl(V, C)[:](diff u, w);
A16: a is finite by A8,Th2;
A17: Atom(V, C).a [= pf.v' by A14,Th27;
Atom(V, C).a [= StrongImpl(V, C).((diff u).v', w)
by A13,A15,A16,Th30;
then A18: Atom(V, C).a [= sf.v' by FUNCOP_1:60;
pf.v'"/\" sf.v' = M(V, C).(pf.v', sf.v') by LATTICES:def 2
.= M(V, C).:(pf, sf).v' by FUNCOP_1:48;
then Atom(V, C).a [= M(V, C).:(pf, sf).v' by A17,A18,FILTER_0:7;
hence Atom(V, C).a [= IMPL(u,w) by A11,LATTICE2:44;
end;
hence v [= IMPL(u,w) by A5,LATTICE2:70;
end;
Lm11: SubstLatt (V, C) is implicative
proof let p,q be Element of SubstLatt (V, C);
take r = FinJoin(SUB p,M(V, C).:(pseudo_compl(V, C),
StrongImpl(V, C)[:](diff p, q)));
thus p "/\" r [= q &
for r1 being Element of SubstLatt (V, C) st
p "/\" r1 [= q holds r1 [= r by Lm10;
end;
definition let V, C;
cluster SubstLatt (V, C) -> implicative;
coherence by Lm11;
end;
theorem
u => v = FinJoin(SUB u,
(the L_meet of SubstLatt (V, C)).:(pseudo_compl(V, C),
StrongImpl(V, C)[:](diff u, v)))
proof
deffunc IMPL(Element of SubstLatt (V, C),
Element of SubstLatt (V, C))
= FinJoin(SUB $1,M(V, C).:(pseudo_compl(V, C),
StrongImpl(V, C)[:](diff $1, $2)));
u "/\" IMPL(u,v) [= v & for w be Element of SubstLatt (V, C)
st u "/\" w [= v holds w [= IMPL(u,v) by Lm10;
hence thesis by FILTER_0:def 8;
end;