:: Lattice of Substitutions Is a Heyting Algebra
:: by Adam Grabowski
::
:: Received December 31, 1998
:: Copyright (c) 1998-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies SUBSET_1, SUBSTLAT, FINSET_1, FUNCT_1, FINSUB_1, PARTFUN1,
TARSKI, XBOOLE_0, SETWISEO, ORDINAL4, NORMFORM, RELAT_1, ARYTM_1,
LATTICES, FUNCT_2, HEYTING1, BINOP_1, STRUCT_0, ZFMISC_1, FDIFF_1,
EQREL_1, LATTICE2, PBOOLE, FUNCOP_1, FILTER_0, XBOOLEAN, HEYTING2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
FUNCOP_1, BINOP_1, FINSET_1, FINSUB_1, FUNCT_2, PARTFUN1, LATTICES,
STRUCT_0, SUBSTLAT, SETWISEO, HEYTING1, LATTICE2, FILTER_0;
constructors FUNCOP_1, SETWISEO, FILTER_0, LATTICE2, HEYTING1, SUBSTLAT,
RELSET_1, BINOP_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FINSET_1,
FINSUB_1, SETWISEO, STRUCT_0, LATTICES, SUBSTLAT, FUNCT_2, RELSET_1,
PRE_POLY, LATTICE2;
requirements SUBSET, BOOLE;
definitions TARSKI, FILTER_0, XBOOLE_0;
expansions TARSKI, XBOOLE_0;
theorems ZFMISC_1, TARSKI, FINSUB_1, FINSET_1, PARTFUN1, BINOP_1, LATTICES,
LATTICE2, RELAT_1, FUNCT_1, FUNCT_2, SUBSTLAT, SETWISEO, FUNCOP_1,
FILTER_0, HEYTING1, RELSET_1, XBOOLE_0, XBOOLE_1, PRE_POLY;
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);
theorem Th1:
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 that
A1: b in SubstitutionSet (V, C) and
A2: a in b;
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 A1,SUBSTLAT:def 1;
then
ex A being Element of Fin PFuncs (V,C) st 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 );
hence thesis by A1,A2;
end;
Lm1: for A, B, C be set st A = B \/ C & A c= B holds A = B
by XBOOLE_1:7;
begin :: Some properties of sets of substitutions
theorem Th2:
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 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 that
A2: s in { a } and
A3: t in { a } and
s c= t;
s = a by A2,TARSKI:def 1;
hence thesis by A3,TARSKI:def 1;
end;
for u being set st u in {a} holds u is finite;
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
b in A and
A2: c in B and
A3: a = b \/ c by A1,SUBSTLAT:15;
take c;
thus thesis by A2,A3,XBOOLE_1:7;
end;
theorem Th4:
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
b in A and
A3: c in B and
A4: a = b \/ c by A1,A2,SUBSTLAT:15;
take c;
thus thesis by A3,A4,XBOOLE_1:7;
end;
theorem Th5:
(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 object;
reconsider aa=a as set by TARSKI:1;
A3: A c= PFuncs (V, C) by FINSUB_1:def 5;
assume
A4: a in mi (A ^ B);
then consider b, c be set such that
A5: b in A and
c in B and
A6: a = b \/ c by A2,SUBSTLAT:15;
A7: b c= aa by A6,XBOOLE_1:7;
consider b1 be set such that
A8: b1 in B and
A9: b1 c= b by A1,A5;
B c= PFuncs (V, C) by FINSUB_1:def 5;
then reconsider b9 = b, b19 = b1 as Element of PFuncs (V, C) by A5,A8,A3;
A10: b = b1 \/ b by A9,XBOOLE_1:12;
b19 tolerates b9 by A9,PARTFUN1:54;
then b in A ^ B by A5,A8,A10,SUBSTLAT:16;
hence thesis by A4,A5,A7,SUBSTLAT:6;
end;
thus A c= mi (A ^ B)
proof
let a be object;
reconsider aa=a as set by TARSKI:1;
A11: A c= PFuncs (V, C) by FINSUB_1:def 5;
assume
A12: a in A;
then consider b be set such that
A13: b in B and
A14: b c= aa by A1;
B c= PFuncs (V, C) by FINSUB_1:def 5;
then reconsider a9 = a, b9 = b as Element of PFuncs (V, C) by A12,A13,A11;
A15: a9 tolerates b9 by A14,PARTFUN1:54;
A16: a in mi A by A12,SUBSTLAT:11;
A17: for b be finite set st b in A ^ B & b c= aa holds b = a
proof
let b be finite set;
assume that
A18: b in A ^ B and
A19: b c= aa;
consider c, d be set such that
A20: c in A and
d in B and
A21: b = c \/ d by A18,SUBSTLAT:15;
c c= b by A21,XBOOLE_1:7;
then c c= aa by A19;
then c = a by A16,A20,SUBSTLAT:6;
hence thesis by A19,A21,Lm1;
end;
a9 = a9 \/ b9 by A14,XBOOLE_1:12;
then
A22: a9 in A ^ B by A12,A13,A15,SUBSTLAT:16;
aa is finite by A12,Th1;
hence thesis by A22,A17,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 -> set means
:Def1:
for x being object holds
x in it iff ex f being finite Function st f in A & x in dom f;
existence
proof
defpred P[object] means
ex f being finite Function st f in A & $1 in dom f;
consider X be set such that
A1: for x being object holds x in X iff x in V & P[x] from XBOOLE_0:sch 1;
take X;
let x be object;
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 and
A3: x in dom f;
A c= PFuncs (V, C) by FINSUB_1:def 5;
then
ex f1 being Function st f = f1 & dom f1 c= V & rng f1 c= C by A2,
PARTFUN1:def 3;
hence thesis by A1,A2,A3;
end;
uniqueness
proof
defpred P[object] means
ex f being finite Function st f in A & $1 in dom f;
let r,s be set such that
A4: for x being object holds
x in r iff ex f being finite Function st f in A & x in dom f and
A5: for x being object holds
x in s iff ex f being finite Function st f in A & x in dom f;
for X1,X2 being set st (for x being object holds x in X1 iff P[x]) &
(for
x being object holds x in X2 iff P[x]) holds X1 = X2
from XBOOLE_0:sch 3;
hence thesis by A4,A5;
end;
end;
reserve C for finite set;
reserve A, B for Element of SubstitutionSet (V, C);
theorem Th6:
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 object;
assume a in Involved A;
then consider f being finite Function such that
A1: f in A and
A2: a in dom f by Def1;
A c= PFuncs (V, C) by FINSUB_1:def 5;
then ex f1 being Function st f = f1 & dom f1 c= V & rng f1 c= C by A1,
PARTFUN1:def 3;
hence thesis by 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
deffunc F(Function)=dom $1;
let V be set, C be finite set, A be non empty Element of Fin PFuncs (V, C);
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 x be set st x in X holds x is finite
proof
let x be set;
assume x in X;
then ex f1 being Element of PFuncs(V, C) st x = dom f1 & f1 in A & f1
is finite;
hence thesis;
end;
A2: A is finite;
A3: { F(f) where f is Element of PFuncs(V, C) : f in A } is finite from
FRAENKEL:sch 21(A2);
for x be object holds x in Involved A iff ex Y be set st x in Y & Y in X
proof
let x be object;
hereby
assume x in Involved A;
then consider f being finite Function such that
A4: f in A and
A5: x in dom f by Def1;
A c= PFuncs (V,C) by FINSUB_1:def 5;
then dom f in X by A4;
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 and
A7: Y in X;
ex f1 being Element of PFuncs(V, C) st Y = dom f1 & f1 in A & f1
is finite by A7;
hence thesis by A6,Def1;
end;
then
A8: Involved A = union X by TARSKI:def 4;
A9: for g being Element of PFuncs(V, C) holds P[g] implies Q[g];
X c= { F(f) where f is Element of PFuncs(V, C) : Q[f]} from FRAENKEL:sch
1(A9);
hence thesis by A3,A8,A1,FINSET_1:7;
end;
theorem Th7:
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 object such that
A2: x in Involved A by XBOOLE_0:def 1;
ex f being finite Function st f in A & x in dom f by A2,Def1;
hence thesis by A1;
end;
registration
let V be set, C being finite set, A being Element of Fin PFuncs (V, C);
cluster Involved A -> finite;
coherence
proof
per cases;
suppose
A is non empty;
hence thesis by Lm2;
end;
suppose
A is empty;
hence thesis by Th7;
end;
end;
end;
theorem
for C being finite set, A being Element of Fin PFuncs ({}, C) holds
Involved A = {} by Th6,XBOOLE_1:3;
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
{ 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
deffunc F(set)=$1;
defpred Q[set] means not contradiction;
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;
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 };
A1: the set of all f where f is Element of PFuncs (Involved A, C)
c= PFuncs (Involved A, C)
proof
let a be object;
assume a in the set of all
f where f is Element of PFuncs (Involved A, C) ;
then ex f1 be Element of PFuncs (Involved A, C) st f1 = a & not
contradiction;
hence thesis;
end;
A2: for v being Element of PFuncs (Involved A, C) holds P[v] implies Q[v];
A3: { 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 FRAENKEL:sch 1(A2);
A4: M c= PFuncs (V, C)
proof
let a be object;
assume a in M;
then ex f1 be Element of PFuncs (Involved A, C) st f1 = a & for g be
Element of PFuncs (V, C) st g in A holds not f1 tolerates g;
then
A5: a in PFuncs (Involved A, C);
Involved A c= V by Th6;
then PFuncs (Involved A, C) c= PFuncs (V, C) by PARTFUN1:50;
hence thesis by A5;
end;
PFuncs (Involved A, C) is finite by PRE_POLY:17;
hence thesis by A3,A1,A4,FINSUB_1:def 5;
end;
end;
theorem Th9:
A ^ -A = {}
proof
assume A ^ -A <> {};
then consider x be object 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
x = s1 \/ t1 and
A2: s1 in A and
A3: t1 in -A and
A4: s1 tolerates t1;
ex f1 be Element of PFuncs (Involved A, C) st f1 = t1 & for g be
Element of PFuncs (V, C) st g in A holds not f1 tolerates g by A3;
hence thesis by A2,A4;
end;
theorem Th10:
A = {} implies -A = { {} }
proof
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;
assume
A1: A = {};
then
A2: for g be Element of PFuncs (V, C) st g in A holds not {} tolerates g;
{ xx where xx is Element of PFuncs (Involved A, C) : P[xx]} c= PFuncs (
Involved A, C) from FRAENKEL:sch 10;
then -A c= PFuncs ({}, C) by A1,Th7;
then
A3: -A c= { {} } by PARTFUN1:48;
{} in { {} } by TARSKI:def 1;
then {} in PFuncs ({}, C) by PARTFUN1:48;
then {} in PFuncs (Involved A, C) by A1,Th7;
then {} in -A by A2;
then { {} } c= -A by ZFMISC_1:31;
hence thesis by A3;
end;
theorem
A = { {} } implies -A = {}
proof
assume
A1: A = {{}};
assume -A <> {};
then consider x1 be object such that
A2: x1 in -A by XBOOLE_0:def 1;
consider f1 being Element of PFuncs (Involved A, C) such that
x1 = f1 and
A3: for g be Element of PFuncs (V, C) st g in {{}} holds not f1
tolerates g by A1,A2;
A4: {} in {{}} by TARSKI:def 1;
{} is PartFunc of V, C by RELSET_1:12;
then
A5: {} in PFuncs (V, C) by PARTFUN1:45;
f1 tolerates {} by PARTFUN1:59;
hence thesis by A3,A5,A4;
end;
theorem Th12:
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);
mi (A ^ -A) = {} by Th9,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 Th10;
then -A in SubstitutionSet (V, C) by SUBSTLAT:2;
then mi -A = { {} } by A1,SUBSTLAT:11;
hence thesis by SUBSTLAT:27;
end;
theorem Th14:
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 reconsider AA = A as finite non empty set;
defpred P[Element of PFuncs (V, C),set] means $2 in dom $1 /\ dom a & $1.
$2 <> a.$2;
defpred P[set] means not contradiction;
A4: ex kk be Function st kk = a & dom kk c= V & rng kk c= C by PARTFUN1:def 3;
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 object such that
A8: x in dom s /\ dom a and
A9: s.x <> a.x by PARTFUN1:def 4;
consider a9 be Function such that
A10: a9 = a and
A11: dom a9 c= V and
rng a9 c= C by PARTFUN1:def 3;
dom s /\ dom a c= dom a9 by A10,XBOOLE_1:17;
then dom s /\ dom a c= V by A11;
then reconsider x as Element of [V] by A8,HEYTING1:def 2;
take x;
thus P[s,x] by A8,A9;
end;
consider g be Element of Funcs (PFuncs (V, C), [V]) such that
A12: for s be Element of PFuncs (V, C) st s in A holds P[s,g.s] from
FRAENKEL:sch 27(A5);
deffunc G(set)=g.$1;
A13: A = [A] by A3,HEYTING1:def 2;
{ G(b) where b is Element of AA : P[b] } is finite from PRE_CIRC:sch
1;
then reconsider
UKA = the set of all g.b where b is Element of [A] as
finite set by A13;
set f = a|UKA;
A14: dom f c= Involved A
proof
let x be object;
assume x in dom f;
then x in UKA by RELAT_1:57;
then consider b be Element of [A] such that
A15: x = g.b;
reconsider b as finite Function by A13,Th1;
reconsider b9 = b as Element of PFuncs (V, C) by A13,SETWISEO:9;
g.b9 in dom b9 /\ dom a by A13,A12;
then x in dom b by A15,XBOOLE_0:def 4;
hence thesis by A13,Def1;
end;
rng f c= rng a by RELAT_1:70;
then rng f c= C by A4;
then reconsider f9 = f as Element of PFuncs (Involved A, C) by A14,
PARTFUN1:def 3;
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 g9 = g1 as Function;
assume
A16: g1 in A;
ex z be set st z in dom g1 /\ dom f & g9.z <> f.z
proof
set z = g.g1;
take z;
A17: z in dom g1 /\ dom a by A12,A16;
then
A18: z in dom a by XBOOLE_0:def 4;
z in the set of all g.b1 where b1 is Element of [A] by A13,A16;
then z in dom a /\ UKA by A18,XBOOLE_0:def 4;
then
A19: z in dom f by RELAT_1:61;
z in dom g1 by A17,XBOOLE_0:def 4;
hence z in dom g1 /\ dom f by A19,XBOOLE_0:def 4;
g1.z <> a.z by A12,A16;
hence thesis by A19,FUNCT_1:47;
end;
hence thesis by PARTFUN1:def 4;
end;
then f9 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 };
hence thesis by RELAT_1:59;
end;
suppose
A20: A is empty;
reconsider K = {} as finite set;
take K;
-A = {{}} by A20,Th10;
hence thesis by TARSKI:def 1;
end;
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
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
reconsider PF = PFuncs (A, B) as functional finite non empty set
by PRE_POLY:17;
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: 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 object;
assume z in Z;
then
ex f1 be Element of PFuncs (A, B) st z = union {f1.i \ i where i is
Element of PFuncs (V, C) : i in A} & dom f1 = A;
hence thesis;
end;
defpred P[Element of PF] means $1 in PFuncs(A,B) & dom $1 = A;
deffunc F(Element of PF)= union {$1.i \ i where i is Element of PFuncs (V,
C) : i in A};
A2: { F(f) where f is Element of PF : P[f]} is finite from PRE_CIRC:sch 1;
K c= PFuncs (V, C) by XBOOLE_1:17;
hence thesis by A1,A2,FINSUB_1:def 5;
end;
end;
theorem Th15:
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 { 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 4;
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} and
A2: dom f = A;
f is PartFunc of A, B by PARTFUN1:47;
hence thesis by A1,A2;
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);
A1: K c= PFuncs (V, C) by FINSUB_1:def 5;
assume a in A ^ (A =>> K);
then consider b,c be set such that
A2: b in A and
A3: c in A =>> K and
A4: a = b \/ c by SUBSTLAT:15;
A c= PFuncs (V, C) by FINSUB_1:def 5;
then reconsider b9 = b as Element of PFuncs (V, C) by A2;
consider f be PartFunc of A, K such that
A5: c = union {f.i \ i where i is Element of PFuncs (V, C) : i in A } and
A6: dom f = A by A3,Th15;
f.b in K by A2,A6,PARTFUN1:4;
then reconsider d = f.b as Element of PFuncs (V, C) by A1;
take d;
thus d in K by A2,A6,PARTFUN1:4;
d \ b9 in {f.i \ i where i is Element of PFuncs (V, C) : i in A} by A2;
hence thesis by A4,A5,XBOOLE_1:44,ZFMISC_1:74;
end;
theorem
for V being set, C being finite set, A being Element of Fin PFuncs (V,
C ) st A = {} holds A =>> A = {{}}
proof
deffunc G(set)={};
let V be set, C be finite set, A be Element of Fin PFuncs (V, C);
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};
A1: ex a being Element of PFuncs (A, A) st P[a]
proof
reconsider e = id A as Element of PFuncs (A, A) by PARTFUN1:45;
take e;
thus thesis;
end;
A2: { {} where f is Element of PFuncs (A, A) : P[f] } = {{}} from LATTICE3:
sch 1 (A1);
assume
A3: A = {};
now
let f be Element of PFuncs (A, A);
not ex x be object st x in {f.i \ i where i is Element of PFuncs (V, C) :
i in A}
proof
given x be object such that
A4: x in {f.i \ i where i is Element of PFuncs (V, C) : i in A};
ex x1 being Element of PFuncs (V, C) st x = f.x1 \ x1 & x1 in A by A4;
hence contradiction by A3;
end;
hence {f.i \ i where i is Element of PFuncs (V, C) : i in A} = {} by
XBOOLE_0:def 1;
end;
then
A5: for v being Element of PFuncs (A, A) st P[v] holds F(v) = G(v) by
ZFMISC_1:2;
A6: { 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 FRAENKEL:sch 6 (A5);
{} is PartFunc of V,C by RELSET_1:12;
then {} in PFuncs (V,C) by PARTFUN1:45;
then {{}} c= PFuncs (V,C) by ZFMISC_1:31;
hence thesis by A6,A2,XBOOLE_1:28;
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) by FINSUB_1:def 5;
then X c= PFuncs (V, C) by A1;
then reconsider B = X as Element of Fin PFuncs (V, C) by A1,FINSUB_1:def 5;
A2: for a,b st a in B & b in B & a c= b holds a = b by A1,SUBSTLAT:5;
for x be set st x in X holds x is finite by A1,Th1;
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 thesis by SUBSTLAT:def 1;
end;
theorem Th17:
for X being set st X c= u holds X is Element of SubstLatt (V, C)
proof
let X be set;
reconsider u9 = u as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4;
assume X c= u;
then X c= u9;
then X in SubstitutionSet (V, C) by Lm4;
hence thesis 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
u9 being Element of SubstitutionSet (V, C) st u9 = u holds it.u = mi(
-u9);
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 FUNCT_2:sch 4;
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,IT9 be UnOp of the carrier of SubstLatt (V, C);
assume that
A2: for u9 being Element of SubstitutionSet (V, C) st u9 = u holds IT.
u = mi (-u9) and
A3: for u9 being Element of SubstitutionSet (V, C) st u9 = u holds IT9
.u = mi (-u9);
now
let u;
reconsider u9 = u as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4;
thus IT.u = mi (-u9) by A2
.= IT9.u by A3;
end;
hence IT = IT9 by FUNCT_2:63;
end;
func StrongImpl(V, C) -> BinOp of the carrier of SubstLatt (V, C) means
:
Def5: for u9, v9 being Element of SubstitutionSet (V, C) st u9 = u & v9 = v
holds it.(u,v) = mi (u9 =>> v9);
existence
proof
set ZA = the carrier of SubstLatt (V, C);
defpred P[set, set, set] means for u9, v9 being Element of SubstitutionSet
(V, C) st u9 = $1 & v9 = $2 holds $3 = mi (u9 =>> v9);
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 x9 = x, y9 = y as Element of SubstitutionSet (V, C) by
SUBSTLAT:def 4;
reconsider z = mi (x9 =>> y9) as Element of ZA by SUBSTLAT:def 4;
take z;
let u9, v9 be Element of SubstitutionSet (V, C);
assume that
A5: u9 = x and
A6: v9 = y;
thus thesis by A5,A6;
end;
consider o being BinOp of the carrier of SubstLatt (V, C) such that
A7: for a,b being Element of SubstLatt (V, C) holds P[a,b,o.(a,b)]
from BINOP_1:sch 3(A4);
take o;
let u,v;
let u9, v9 be Element of SubstitutionSet (V, C);
assume that
A8: u9 = u and
A9: v9 = v;
thus thesis by A7,A8,A9;
end;
correctness
proof
let IT1,IT2 be BinOp of the carrier of SubstLatt (V, C);
assume that
A10: for u9, v9 being Element of SubstitutionSet (V, C) st u9 = u & v9
= v holds IT1.(u,v) = mi (u9 =>> v9) and
A11: for u9, v9 being Element of SubstitutionSet (V, C) st u9 = u & v9
= v holds IT2.(u,v) = mi (u9 =>> v9);
now
let u, v;
reconsider u9 = u, v9 = v as Element of SubstitutionSet (V, C) by
SUBSTLAT:def 4;
thus IT1.(u,v) = mi (u9 =>> v9) by A10
.= IT2.(u,v) by A11;
end;
hence IT1 = IT2 by BINOP_1:2;
end;
let u;
func SUB u -> Element of Fin the carrier of SubstLatt (V, C) equals
bool u;
coherence
proof
reconsider u9 = u as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4;
A12: bool u c= the carrier of SubstLatt (V, C)
proof
let x be object;
assume x in bool u;
then x is Element of SubstLatt (V, C) by Th17;
hence thesis;
end;
u9 is finite;
hence thesis by A12,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
deffunc F(set)=u \ $1;
consider IT being Function such that
A13: 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 FUNCT_1:sch 5;
u in the carrier of SubstLatt (V, C);
then
A14: u in SubstitutionSet (V, C) by SUBSTLAT:def 4;
for x be object st x in the carrier of SubstLatt (V, C) holds IT.x in
Fin PFuncs (V, C)
proof
let x be object;
assume
A15: x in the carrier of SubstLatt (V, C);
reconsider x as set by TARSKI:1;
A16: IT.x = u \ x by A13,A15;
u \ x in SubstitutionSet (V,C) by A14,Lm4;
hence thesis by A16;
end;
then reconsider
IT as Function of the carrier of SubstLatt (V, C), Fin PFuncs (
V, C) by A13,FUNCT_2:3;
now
let v be Element of SubstLatt (V, C);
u \ v in SubstitutionSet (V,C) by A14,Lm4;
then IT.v in SubstitutionSet (V,C) by A13;
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 thesis by A13;
end;
correctness
proof
let IT,IT9 be UnOp of the carrier of SubstLatt (V, C);
assume that
A17: IT.v = u \ v and
A18: IT9.v = u \ v;
now
let v be Element of SubstLatt (V, C);
thus IT.v = u \ v by A17
.= IT9.v by A18;
end;
hence IT = IT9 by FUNCT_2:63;
end;
end;
Lm5: v in SUB u implies v "\/" (diff u).v = u
proof
assume
A1: v in SUB u;
reconsider u9 = u, v9 = v, dv = (diff u).v as Element of SubstitutionSet (V,
C) by SUBSTLAT:def 4;
A2: u \ v = (diff u).v by Def7;
thus v "\/" (diff u).v = (the L_join of SubstLatt (V,C)).(v, (diff u).v) by
LATTICES:def 1
.= mi ( v9 \/ dv ) by SUBSTLAT:def 4
.= mi u9 by A1,A2,XBOOLE_1:45
.= u by SUBSTLAT:11;
end;
Lm6: for K be Element of Fin PFuncs (V, C) st 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
deffunc F(set)=$1;
let K be Element of Fin PFuncs (V, C) such that
A1: K = {a};
deffunc F1(Element of PFuncs (V, C),Element of PFuncs (V, C))=$1 \/ $2;
defpred Q[Element of PFuncs (V, C)] means not $1 tolerates a & $1 in u & $1
tolerates a;
deffunc F(Element of PFuncs (V, C),Element of PFuncs (V, C))=$1 \/ $2;
defpred P[Element of PFuncs (V, C)] means $1 is finite & not $1 tolerates a;
set M = { F(s) where s is Element of PFuncs (V, C): F(s) in u & P[s] };
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;
defpred P[Element of PFuncs (V, C)] means $1 in M & $1 tolerates a;
defpred P1[Element of PFuncs (V, C),Element of PFuncs (V, C)] means $1 in M
& $1 tolerates $2;
deffunc F(Element of PFuncs (V, C))=$1 \/ a;
A2: M c= u from FRAENKEL:sch 17;
then reconsider v = M as Element of SubstLatt (V, C) by Th17;
reconsider v as Element of SubstitutionSet (V,C) by SUBSTLAT:def 4;
take v;
thus v in SUB u by A2;
A3: P[s,t] iff Q[s,t] by TARSKI:def 1;
A4: { F(s,t): P[s,t] } = { F(s9,t9) where s9, t9 is Element of PFuncs (V, C)
: Q[s9,t9] } from FRAENKEL:sch 4(A3);
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 ex s2 be Element of PFuncs (V, C) st s2 = s & s2 in u & s2 is
finite & not s2 tolerates a;
hence thesis;
end;
thus thesis;
end;
then
A5: P[s] iff Q[s];
A6: { F(s9) where s9 is Element of PFuncs (V, C) : P[s9]} = { F(s): Q[s]}
from FRAENKEL:sch 3(A5);
{ F1(s,t) where t is Element of PFuncs (V, C) : t = a & P1[s,t]} = { F1(
s9,a) where s9 is Element of PFuncs (V, C) : P1[s9,a]} from FRAENKEL:sch 20;
then
A7: v ^ K = { s \/ a: not s tolerates a & s in u & s tolerates a } by A1,A4,A6,
SUBSTLAT:def 3;
thus v ^ K = {}
proof
assume v ^ K <> {};
then consider x be object such that
A8: x in v ^ K by XBOOLE_0:def 1;
ex s1 be Element of PFuncs (V, C) st x = s1 \/ a &( not s1 tolerates
a)& s1 in u & s1 tolerates a by A7,A8;
hence thesis;
end;
let b;
assume b in (diff u).v;
then
A9: b in u \ v by Def7;
then
A10: not b in M by XBOOLE_0:def 5;
u in the carrier of SubstLatt (V, C);
then u in SubstitutionSet (V, C) by SUBSTLAT:def 4;
then b is finite by A9,Th1;
hence thesis by A9,A10;
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
deffunc F(Element of PFuncs (V, C))= mi {.$1.};
consider f be Function of PFuncs (V, C), SubstitutionSet (V, C) such that
A1: for a be Element of PFuncs (V, C) holds f.a = F(a) from FUNCT_2:
sch 4;
A2: the carrier of SubstLatt (V, C) = SubstitutionSet (V, C) by SUBSTLAT:def 4;
A3: now
let x be object;
assume x in PFuncs (V, C);
then reconsider a = x as Element of PFuncs (V, C);
f.a = mi {.a.} by A1;
hence f.x in the carrier of SubstLatt (V, C) by A2;
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:3;
take f;
thus thesis by A1;
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.} and
A5: for a holds IT2.a = mi {.a.};
now
let a;
IT1.a = mi {.a.} by A4;
hence IT1.a = IT2.a by A5;
end;
hence thesis by FUNCT_2:63;
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);
A1: 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 that
A2: s in { a } and
A3: t in { a } and
s c= t;
s = a by A2,TARSKI:def 1;
hence thesis by A3,TARSKI:def 1;
end;
assume a is finite;
then for u being set st u in { a } holds u is finite;
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;
then { a } in SubstitutionSet (V, C) by SUBSTLAT:def 1;
then {a} = mi {.a.} by SUBSTLAT:11
.= Atom (V, C).a by Def8;
hence thesis;
end;
theorem Th18:
FinJoin (K, Atom(V, C)) = FinUnion(K, singleton PFuncs (V, C))
proof
deffunc F(Element of Fin PFuncs (V, C))= mi $1;
A1: FinUnion(K,singleton PFuncs (V, C)) c= mi (FinUnion(K,singleton PFuncs
(V, C)))
proof
let a be object;
reconsider aa=a as set by TARSKI:1;
assume
A2: a in FinUnion(K,singleton PFuncs (V, C));
then consider b be Element of PFuncs (V, C) such that
A3: b in K and
A4: a in (singleton PFuncs (V, C)).b by SETWISEO:57;
A5: a = b by A4,SETWISEO:55;
A6: now
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
A7: 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 );
let s be finite set;
assume that
A8: s in FinUnion(K,singleton PFuncs (V, C)) and
A9: s c= aa;
consider t such that
A10: t in K and
A11: s in (singleton PFuncs (V, C)).t by A8,SETWISEO:57;
s = t by A11,SETWISEO:55;
hence s = a by A3,A5,A9,A10,A7;
end;
aa is finite by A3,A5,Th1;
hence thesis by A2,A6,SUBSTLAT:7;
end;
consider g being Function of Fin PFuncs (V, C), SubstitutionSet (V,C) such
that
A12: for B be Element of Fin PFuncs (V, C) holds g.B = F(B) from FUNCT_2:
sch 4;
reconsider g as Function of Fin PFuncs (V, C), the carrier of SubstLatt (V,
C) by SUBSTLAT:def 4;
A13: now
let x,y be Element of Fin PFuncs (V, C);
A14: g.x = mi x by A12;
A15: g.y = mi y by A12;
thus g.(x \/ y) = mi (x \/ y) by A12
.= 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 A14,A15,SUBSTLAT:def 4;
end;
A16: now
let a be object;
assume
A17: a in K;
then reconsider a9 = a as Element of PFuncs (V, C) by SETWISEO:9;
A18: a9 is finite by A17,Th1;
then reconsider KL = {a9} as Element of SubstitutionSet (V,C) by Th2;
thus ((g*singleton PFuncs (V, C))|K).a = (g*singleton PFuncs (V, C)).a by
A17,FUNCT_1:49
.= g.(singleton PFuncs (V, C) .a9) by FUNCT_2:15
.= g.{a} by SETWISEO:54
.= mi KL by A12
.= KL by SUBSTLAT:11
.= Atom (V, C).a9 by A18,Lm7
.= (Atom (V, C)|K).a by A17,FUNCT_1:49;
end;
A19: mi (FinUnion(K,singleton PFuncs (V, C))) c= FinUnion(K,singleton PFuncs
(V, C)) by SUBSTLAT:8;
A20: rng singleton PFuncs (V, C) c= Fin PFuncs (V, C);
A21: K c= PFuncs (V, C) by FINSUB_1:def 5;
then K c= dom (Atom(V, C)) by FUNCT_2:def 1;
then
A22: dom (Atom(V, C)|K) = K by RELAT_1:62;
reconsider gs = g*singleton PFuncs (V, C) as Function of PFuncs (V, C), the
carrier of SubstLatt (V, C);
A23: g.{}.PFuncs (V, C) = mi {}.PFuncs (V, C) by A12
.= {} by SUBSTLAT:9
.= Bottom SubstLatt (V, C) by SUBSTLAT:26
.= the_unity_wrt the L_join of SubstLatt (V, C) by LATTICE2:18;
dom g = Fin PFuncs (V, C) by FUNCT_2:def 1;
then
A24: dom ((g*singleton PFuncs (V, C))) = dom singleton PFuncs (V, C) by A20,
RELAT_1:27;
dom singleton PFuncs (V, C) = PFuncs (V, C) by FUNCT_2:def 1;
then dom ((g*singleton PFuncs (V, C))|K) = K by A21,A24,RELAT_1:62;
hence FinJoin(K, Atom (V, C)) = FinJoin(K, gs) by A22,A16,FUNCT_1:2
,LATTICE2:53
.= (the L_join of SubstLatt (V, C)) $$(K,gs) by LATTICE2:def 3
.= g.(FinUnion(K,singleton PFuncs (V, C))) by A23,A13,SETWISEO:53
.= mi (FinUnion(K,singleton PFuncs (V, C))) by A12
.= FinUnion(K,singleton PFuncs (V, C)) by A19,A1;
end;
theorem Th19:
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:58
.= FinJoin(u, Atom(V, C)) by Th18;
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 u9 = u, v9 = v as Element of SubstitutionSet (V, C) by
SUBSTLAT:def 4;
u "/\" v = (the L_meet of SubstLatt (V, C)).(u9, v9) by LATTICES:def 2
.= mi (u9 ^ v9) by SUBSTLAT:def 4
.= u9 by A1,Th5;
hence thesis by LATTICES:4;
end;
theorem Th20:
(diff u).v [= u
proof
(diff u).v = u \ v by Def7;
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 Th21:
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 Th22:
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 that
A1: K = {a} and
A2: L = u and
A3: L ^ K = {};
a in K by A1,TARSKI:def 1;
then
A4: a is finite by Th1;
now
let c be set;
assume
A5: c in Atom(V, C).a;
then reconsider c9 = c as Element of PFuncs (V, C) by A4,Th21;
c = a by A4,A5,Th21;
then consider b be finite set such that
A6: b in -L and
A7: b c= c9 by A1,A3,Th14;
consider d be set such that
A8: d c= b and
A9: d in mi(-L) by A6,SUBSTLAT:10;
take e = d;
thus e in pseudo_compl(V, C).u by A2,A9,Def4;
thus e c= c by A7,A8;
end;
hence thesis by Lm8;
end;
theorem Th23:
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 u9 = u, v9 = v as Element of SubstitutionSet (V, C) by
SUBSTLAT:def 4;
assume u [= v;
then u = u "/\" v by LATTICES:4
.= (the L_meet of SubstLatt (V, C)).(u,v) by LATTICES:def 2
.= mi (u9 ^ v9) by SUBSTLAT:def 4;
hence thesis by Th4;
end;
theorem Th24:
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 u9 = u as Element of SubstLatt (V, C) by SUBSTLAT:def 4;
defpred P[set,set] means $2 in v & $2 c= $1 \/ a;
assume that
A1: for b be set st b in u ex c be set st c in v & c c= b \/ 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 and
A4: 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,A4;
end;
consider f9 be Element of Funcs(PFuncs (V, C), PFuncs (V, C)) such that
A5: b in u implies P[b,f9.b] from FRAENKEL:sch 27(A2);
set g = f9|u;
consider f2 be Function such that
A6: f9 = f2 and
dom f2 = PFuncs (V, C) and
rng f2 c= PFuncs (V, C) by FUNCT_2:def 2;
u c= PFuncs (V, C) by FINSUB_1:def 5;
then g is Function of u, PFuncs (V, C) by FUNCT_2:32;
then
A7: dom g = u by FUNCT_2:def 1;
for b be object st b in u holds g.b in v
proof
let b be object;
assume
A8: b in u;
u c= PFuncs (V, C) by FINSUB_1:def 5;
then reconsider b9 = b as Element of PFuncs (V, C) by A8;
g.b9 = f2.b9 by A6,A8,FUNCT_1:49;
hence thesis by A5,A6,A8;
end;
then g is Function of u, v by A7,FUNCT_2:3;
then
A9: rng g c= v by RELAT_1:def 19;
A10: for b be set st b in u9 holds g.b c= b \/ a
proof
let b be set;
assume
A11: b in u9;
u c= PFuncs (V, C) by FINSUB_1:def 5;
then reconsider b9 = b as Element of PFuncs (V, C) by A11;
g.b9 = f2.b9 by A6,A11,FUNCT_1:49;
hence thesis by A5,A6,A11;
end;
reconsider g as Element of PFuncs (u, v) by A7,A9,PARTFUN1:def 3;
set d = union {g.i \ i where i is Element of PFuncs (V, C) : i in u9};
A12: d c= a
proof
let x be object;
assume x in d;
then consider Y be set such that
A13: x in Y and
A14: Y in {g.i \ i where i is Element of PFuncs (V, C) : i in u9} by
TARSKI:def 4;
consider j be Element of PFuncs (V, C) such that
A15: Y = g.j \ j and
A16: j in u9 by A14;
g.j c= j \/ a by A10,A16;
then g.j \j c= a by XBOOLE_1:43;
hence thesis by A13,A15;
end;
then reconsider d as Element of PFuncs (V, C) by PRE_POLY:15;
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 A7;
hence d in u =>> v by XBOOLE_0:def 4;
thus thesis by A12;
end;
theorem Th25:
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 u9 = u, v9 = v, Aa = (Atom(V, C).a) as Element of SubstitutionSet
(V, C) by SUBSTLAT:def 4;
A3: now
let c be set;
A4: a in Aa by Th23;
assume
A5: c in u;
then
A6: c in u9;
then reconsider c9 = c as Element of PFuncs (V, C) by SETWISEO:9;
c9 tolerates a by A1,A5;
then
c \/ a in { s1 \/ t1 where s1,t1 is Element of PFuncs (V,C) : s1 in u9
& t1 in Aa & s1 tolerates t1 } by A5,A4;
then
A7: c \/ a in u9 ^ Aa by SUBSTLAT:def 3;
c is finite by A6,Th1;
then consider b be set such that
A8: b c= c \/ a and
A9: b in mi(u9 ^ Aa) by A7,SUBSTLAT:10;
b in (the L_meet of SubstLatt (V, C)).(u, Atom(V, C).a) by A9,
SUBSTLAT:def 4;
then b in u "/\" (Atom (V, C).a) by LATTICES:def 2;
then consider d be set such that
A10: d in v and
A11: d c= b by A2,Lm9;
take e = d;
thus e in v by A10;
thus e c= c \/ a by A8,A11;
end;
now
let c be set;
assume
A12: c in Atom(V, C).a;
then c = a by Th21;
then consider b be set such that
A13: b in u9 =>> v9 and
A14: b c= c by A3,Th24;
c in Aa by A12;
then c is finite by Th1;
then consider d be set such that
A15: d c= b and
A16: d in mi(u9 =>> v9) by A13,A14,SUBSTLAT:10;
take e = d;
thus e in (StrongImpl(V, C).(u, v)) by A16,Def5;
thus e c= c by A14,A15;
end;
hence thesis by Lm8;
end;
deffunc M(set, set) = the L_meet of SubstLatt ($1, $2);
theorem Th26:
u "/\" pseudo_compl(V, C).u = Bottom SubstLatt (V, C)
proof
reconsider u9 = 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(-u9)) by Def4
.= mi(u9 ^ mi(-u9)) by SUBSTLAT:def 4
.= mi(u9 ^ -u9) by SUBSTLAT:20
.= Bottom SubstLatt (V, C) by Th12;
end;
theorem Th27:
u "/\" StrongImpl(V, C).(u, v) [= v
proof
now
reconsider u9 = u, v9 = v as Element of SubstitutionSet (V, C) by
SUBSTLAT:def 4;
let a be set;
assume
A1: a in u "/\" StrongImpl(V, C).(u, v);
u "/\" StrongImpl(V, C).(u, v) = M(V, C).(u, StrongImpl(V, C).(u, v))
by LATTICES:def 2
.= M(V, C).(u, mi(u9 =>> v9)) by Def5
.= mi(u9 ^ mi(u9 =>> v9)) by SUBSTLAT:def 4
.= mi(u9 ^ (u9 =>> v9)) by SUBSTLAT:20;
then a in u9 ^ (u9 =>> v9) 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));
reconsider v9 = v as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4;
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);
A2: w "/\" (pc "/\" si) = (w "/\" pc) "/\" si by LATTICES:def 7
.= Bottom SubstLatt (V, C) "/\" si by Th26
.= Bottom SubstLatt (V, C);
assume w in SUB u;
then
A3: w "\/" u2 = u by Lm5;
M(V, C)[;](u, Psi).w = M(V, C).(u, Psi.w) by FUNCOP_1:53
.= u "/\" Psi.w by LATTICES:def 2
.= u "/\" M(V, C).(pc, StrongImpl(V, C)[:](diff u, v).w) by FUNCOP_1:37
.= u "/\" (pc "/\" StrongImpl(V, C)[:](diff u, v).w) by LATTICES:def 2
.= u "/\" (pc "/\" si) by FUNCOP_1:48
.= (w "/\" (pc "/\" si)) "\/" (u2 "/\" (pc "/\" si)) by A3,
LATTICES:def 11
.= u2 "/\" (si "/\" pc) by A2
.= (u2 "/\" si) "/\" pc by LATTICES:def 7;
then
A4: M(V, C)[;](u, Psi).w [= u2 "/\" si by LATTICES:6;
u2 "/\" si [= v by Th27;
hence M(V, C)[;](u, Psi).w [= v by A4,LATTICES:7;
end;
u "/\" IMPL(u,v) = FinJoin(SUB u, M(V, C)[;](u, Psi)) by LATTICE2:66;
hence u "/\" IMPL(u,v) [= v by A1,LATTICE2:54;
let w be Element of SubstLatt (V, C);
assume
A5: u "/\" v [= w;
A6: v = FinJoin(v9, Atom(V, C)) by Th19;
then
A7: u "/\" v = FinJoin(v9, M(V, C)[;](u, Atom(V, C))) by LATTICE2:66;
now
set pf = pseudo_compl(V, C), sf = StrongImpl(V, C)[:](diff u, w);
let a be Element of PFuncs (V, C);
reconsider SA = {.a.} as Element of Fin PFuncs (V, C);
consider v be Element of SubstitutionSet (V, C) such that
A8: v in SUB u and
A9: v ^ SA = {} and
A10: for b be Element of PFuncs (V, C) st b in (diff u).v holds b
tolerates a by Lm6;
assume
A11: a in v9;
then
A12: a is finite by Th1;
reconsider v9 = v as Element of SubstLatt (V, C) by SUBSTLAT:def 4;
set dv = (diff u).v9;
M(V, C)[;](u, Atom(V, C)).a [= w by A7,A5,A11,LATTICE2:31;
then M(V, C).(u, Atom(V, C).a) [= w by FUNCOP_1:53;
then
A13: u "/\" Atom(V, C).a [= w by LATTICES:def 2;
a is finite by A11,Th1;
then reconsider SS = {a} as Element of SubstitutionSet (V, C) by Th2;
v ^ SS = {} by A9;
then
A14: Atom(V, C).a [= pf.v9 by Th22;
dv "/\" Atom(V, C).a [= u "/\" Atom(V, C).a by Th20,LATTICES:9;
then dv "/\" Atom(V, C).a [= w by A13,LATTICES:7;
then Atom(V, C).a [= StrongImpl(V, C).((diff u).v9, w) by A10,A12,Th25;
then
A15: Atom(V, C).a [= sf.v9 by FUNCOP_1:48;
pf.v9"/\" sf.v9 = M(V, C).(pf.v9, sf.v9) by LATTICES:def 2
.= M(V, C).:(pf, sf).v9 by FUNCOP_1:37;
then Atom(V, C).a [= M(V, C).:(pf, sf).v9 by A14,A15,FILTER_0:7;
hence Atom(V, C).a [= IMPL(u,w) by A8,LATTICE2:29;
end;
hence v [= IMPL(u,w) by A6,LATTICE2:54;
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;
registration
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)))
;
A1: for w be Element of SubstLatt (V, C) st u "/\" w [= v holds w [= IMPL(u,
v) by Lm10;
u "/\" IMPL(u,v) [= v by Lm10;
hence thesis by A1,FILTER_0:def 7;
end;