:: Algebra of Normal Forms Is a Heyting Algebra
:: by Andrzej Trybulec
::
:: Received January 3, 1991
:: Copyright (c) 1991-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, FUNCT_1, SUBSET_1, RELAT_1, FINSUB_1, TARSKI, NORMFORM,
ZFMISC_1, SETWISEO, QC_LANG1, ORDINAL4, STRUCT_0, LATTICE2, LATTICES,
BINOP_1, PBOOLE, EQREL_1, FUNCT_2, ARYTM_1, MCART_1, FINSET_1, FUNCT_3,
FDIFF_1, FUNCOP_1, FILTER_0, XBOOLEAN, HEYTING1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, XTUPLE_0, XFAMILY, MCART_1, BINOP_1, FUNCOP_1,
FINSET_1, FINSUB_1, DOMAIN_1, LATTICES, LATTICE2, SETWISEO, NORMFORM,
FILTER_0, FUNCT_3;
constructors DOMAIN_1, FUNCT_3, FUNCOP_1, FINSET_1, SETWISEO, FILTER_0,
LATTICE2, NORMFORM, RELSET_1, XTUPLE_0, BINOP_1, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, FINSET_1, FINSUB_1,
STRUCT_0, LATTICES, NORMFORM, LATTICE2, RELAT_1, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, FILTER_0, XBOOLE_0;
equalities NORMFORM;
expansions TARSKI, XBOOLE_0, NORMFORM;
theorems LATTICES, LATTICE2, FUNCOP_1, NORMFORM, TARSKI, FUNCT_2, DOMAIN_1,
FINSUB_1, FINSET_1, BINOP_1, FUNCT_1, FRAENKEL, SETWISEO, FILTER_0,
ZFMISC_1, XBOOLE_0, XBOOLE_1;
schemes FRAENKEL, FUNCT_2, BINOP_1;
begin
:: Preliminaries
theorem Th1:
for A,B,C being non empty set, f being Function of A,B st for x
being Element of A holds f.x in C holds f is Function of A,C
proof
let A,B,C be non empty set, f be Function of A,B;
assume for x being Element of A holds f.x in C;
then dom f = A & for x be object holds x in A implies f.x in C
by FUNCT_2:def 1;
hence thesis by FUNCT_2:3;
end;
reserve A for non empty set,
a for Element of A;
definition
let A;
let B,C be Element of Fin A;
redefine pred B c= C means :: redefines c= (TARSKI, definition)
for a st a in B holds a in C;
compatibility
proof
thus B c= C implies for a st a in B holds a in C;
assume
A1: for a st a in B holds a in C;
let x be object;
assume
A2: x in B;
then x is Element of A by SETWISEO:9;
hence thesis by A1,A2;
end;
end;
reserve A for set;
definition
let A;
assume
A1: A is non empty;
func [A] -> non empty set equals
:Def2:
A;
correctness by A1;
end;
reserve B,C for Element of Fin DISJOINT_PAIRS A,
x for Element of [:Fin A, Fin A:],
a,b,c,d,s,t,s9,t9,t1,t2,s1,s2 for Element of DISJOINT_PAIRS A,
u,v,w for Element of NormForm A;
theorem
B = {} implies mi B = {} by NORMFORM:40,XBOOLE_1:3;
Lm1: now
let A,a;
reconsider B = {. a .} as Element of Fin DISJOINT_PAIRS A;
now
let c,b such that
A1: c in B and
A2: b in B and
c c= b;
c = a by A1,TARSKI:def 1;
hence c = b by A2,TARSKI:def 1;
end;
hence { a } is Element of Normal_forms_on A by NORMFORM:33;
end;
registration
let A;
cluster non empty for Element of Normal_forms_on A;
existence
proof
set a = the Element of DISJOINT_PAIRS A;
{a} is Element of Normal_forms_on A by Lm1;
hence thesis;
end;
end;
definition
let A,a;
redefine func { a } -> Element of Normal_forms_on A; :: redefines { (TARSKI, definition)
coherence by Lm1;
end;
definition
let A;
let u be Element of NormForm A;
func @u -> Element of Normal_forms_on A equals
u;
coherence by NORMFORM:def 12;
end;
reserve K,L for Element of Normal_forms_on A;
theorem Th3:
mi (K^K) = K
proof
thus mi (K^K) = mi K by NORMFORM:55
.= K by NORMFORM:42;
end;
theorem Th4:
for X being set st X c= K holds X in Normal_forms_on A
proof
let X be set;
assume
A1: X c= K;
K c= DISJOINT_PAIRS A by FINSUB_1:def 5;
then X c= DISJOINT_PAIRS A by A1;
then reconsider B = X as Element of Fin DISJOINT_PAIRS A by A1,FINSUB_1:def 5
;
for a,b st a in B & b in B & a c= b holds a = b by A1,NORMFORM:32;
hence thesis;
end;
theorem Th5:
for X being set st X c= u holds X is Element of NormForm A
proof
let X be set;
assume
A1: X c= u;
u = @u;
then X in Normal_forms_on A by A1,Th4;
hence thesis by NORMFORM:def 12;
end;
definition
let A;
func Atom(A) -> Function of DISJOINT_PAIRS A, the carrier of NormForm A
means
:Def4:
it.a = { a };
existence
proof
set f = singleton DISJOINT_PAIRS A;
A1: dom f = DISJOINT_PAIRS A by FUNCT_2:def 1;
A2: the carrier of NormForm A = Normal_forms_on A by NORMFORM:def 12;
now
let x be object;
assume x in DISJOINT_PAIRS A;
then reconsider a = x as Element of DISJOINT_PAIRS A;
f.a = { a } by SETWISEO:54;
hence f.x in the carrier of NormForm A by A2;
end;
then reconsider
f as Function of DISJOINT_PAIRS A, the carrier of NormForm A by A1,
FUNCT_2:3;
take f;
thus thesis by SETWISEO:54;
end;
uniqueness
proof
let IT1,IT2 be Function of DISJOINT_PAIRS A, the carrier of NormForm A
such that
A3: for a holds IT1.a = { a } and
A4: for a holds IT2.a = { a };
now
let a;
IT1.a = { a } by A3;
hence IT1.a = IT2.a by A4;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem Th6:
c in Atom(A).a implies c = a
proof
Atom(A).a = { a } by Def4;
hence thesis by TARSKI:def 1;
end;
theorem Th7:
a in Atom(A).a
proof
Atom(A).a = { a } by Def4;
hence thesis by TARSKI:def 1;
end;
theorem
Atom(A).a = singleton DISJOINT_PAIRS A .a
proof
thus (singleton DISJOINT_PAIRS A).a = {a} by SETWISEO:54
.= Atom A.a by Def4;
end;
theorem Th9:
FinJoin(K, Atom(A)) = FinUnion(K, singleton DISJOINT_PAIRS A)
proof
deffunc F(Element of Fin DISJOINT_PAIRS A) = mi $1;
A1: FinUnion(K,singleton DISJOINT_PAIRS A) c= mi (FinUnion(K,singleton
DISJOINT_PAIRS A))
proof
let a;
assume
A2: a in FinUnion(K,singleton DISJOINT_PAIRS A);
then consider b such that
A3: b in K and
A4: a in (singleton DISJOINT_PAIRS A).b by SETWISEO:57;
A5: a = b by A4,SETWISEO:55;
now
let s;
assume that
A6: s in FinUnion(K,singleton DISJOINT_PAIRS A) and
A7: s c= a;
consider t such that
A8: t in K and
A9: s in (singleton DISJOINT_PAIRS A).t by A6,SETWISEO:57;
s = t by A9,SETWISEO:55;
hence s = a by A3,A5,A7,A8,NORMFORM:32;
end;
hence thesis by A2,NORMFORM:39;
end;
A10: mi (FinUnion(K,singleton DISJOINT_PAIRS A)) c= FinUnion(K,singleton
DISJOINT_PAIRS A) by NORMFORM:40;
consider g being Function of Fin DISJOINT_PAIRS A, Normal_forms_on A such
that
A11: g.B = F(B) from FUNCT_2:sch 4;
reconsider g as Function of Fin DISJOINT_PAIRS A,the carrier of NormForm A
by NORMFORM:def 12;
A12: g.{}.DISJOINT_PAIRS A = mi {}.DISJOINT_PAIRS A by A11
.= {} by NORMFORM:40,XBOOLE_1:3
.= Bottom NormForm A by NORMFORM:57
.= the_unity_wrt the L_join of NormForm A by LATTICE2:18;
A13: now
let x,y be Element of Fin DISJOINT_PAIRS A;
A14: @(g.x) = mi x & @(g.y) = mi y by A11;
thus g.(x \/ y) = mi (x \/ y) by A11
.= mi (mi x \/ y) by NORMFORM:44
.= mi (mi x \/ mi y) by NORMFORM:45
.= (the L_join of NormForm A).(g.x,g.y) by A14,NORMFORM:def 12;
end;
A15: now
let a;
thus (g*singleton DISJOINT_PAIRS A).a = g.(singleton DISJOINT_PAIRS A .a)
by FUNCT_2:15
.= g.{a} by SETWISEO:54
.= mi { a } by A11
.= { a } by NORMFORM:42
.= Atom A.a by Def4;
end;
thus FinJoin(K, Atom A) = (the L_join of NormForm A) $$(K,Atom A) by
LATTICE2:def 3
.= (the L_join of NormForm A) $$(K,g*singleton DISJOINT_PAIRS A) by A15,
FUNCT_2:63
.= g.(FinUnion(K,singleton DISJOINT_PAIRS A)) by A12,A13,SETWISEO:53
.= mi (FinUnion(K,singleton DISJOINT_PAIRS A)) by A11
.= FinUnion(K,singleton DISJOINT_PAIRS A) by A10,A1;
end;
theorem Th10:
u = FinJoin(@u, Atom(A))
proof
thus u = FinUnion(@u, singleton DISJOINT_PAIRS A) by SETWISEO:58
.= FinJoin(@u, Atom(A)) by Th9;
end;
Lm2: u [= v implies for x st x in u ex b st b in v & b c= x
proof
assume u [= v;
then
A1: v = u "\/" v by LATTICES:def 3
.= (the L_join of NormForm A).(u,v) by LATTICES:def 1
.= mi (@u \/ @v) by NORMFORM:def 12;
let x;
assume
A2: x in u;
u = @u;
then reconsider c = x as Element of DISJOINT_PAIRS A by A2,SETWISEO:9;
c in u \/ v by A2,XBOOLE_0:def 3;
then consider b such that
A3: b c= c & b in mi (@u \/ @v) by NORMFORM:41;
take b;
thus thesis by A1,A3;
end;
Lm3: (for a st a in u ex b st b in v & b c= a) implies u [= v
proof
assume
A1: for a st a in u ex b st b in v & b c= a;
A2: mi(@u \/ @v) c= @v
proof
let a;
assume
A3: a in mi(@u \/ @v);
then a in u \/ v by NORMFORM:36;
then a in u or a in v by XBOOLE_0:def 3;
then consider b such that
A4: b in v and
A5: b c= a by A1;
b in u \/ v by A4,XBOOLE_0:def 3;
hence thesis by A3,A4,A5,NORMFORM:38;
end;
A6: @v c= mi(@u \/ @v)
proof
let a;
assume
A7: a in @v;
then
A8: a in mi @v by NORMFORM:42;
A9: now
let b;
assume that
A10: b in u \/ v and
A11: b c= a;
b in u or b in v by A10,XBOOLE_0:def 3;
then consider c such that
A12: c in v and
A13: c c= b by A1;
c = a by A8,A11,A12,A13,NORMFORM:2,38;
hence b = a by A11,A13,NORMFORM:1;
end;
a in @u \/ @v by A7,XBOOLE_0:def 3;
hence thesis by A9,NORMFORM:39;
end;
u "\/" v = (the L_join of NormForm A).(u,v) by LATTICES:def 1
.= mi (@u \/ @v) by NORMFORM:def 12
.= v by A2,A6;
hence thesis by LATTICES:def 3;
end;
reserve f,f9 for (Element of Funcs(DISJOINT_PAIRS A, [:Fin A,Fin A:])),
g,h for Element of Funcs(DISJOINT_PAIRS A, [A]);
definition
let A be set;
func pair_diff A -> BinOp of [:Fin A,Fin A:] means
:Def5:
for a,b being Element of [:Fin A, Fin A:] holds it.(a,b) = a \ b;
existence
proof
deffunc F(Element of [:Fin A,Fin A:], Element of [:Fin A,Fin A:]) = $1 \
$2;
thus ex f being BinOp of [:Fin A,Fin A:] st for a,b being Element of [:Fin
A, Fin A:] holds f.(a,b) = F(a,b) from BINOP_1:sch 4;
end;
correctness
proof
let IT,IT9 be BinOp of [:Fin A,Fin A:] such that
A1: for a,b being Element of [:Fin A, Fin A:] holds IT.(a,b) = a \ b and
A2: for a,b being Element of [:Fin A, Fin A:] holds IT9.(a,b) = a \ b;
now
let a,b be Element of [:Fin A, Fin A:];
IT.(a,b) = a \ b by A1;
hence IT.(a,b) = IT9.(a,b) by A2;
end;
hence thesis by BINOP_1:2;
end;
end;
definition
let A,B;
func -B -> Element of Fin DISJOINT_PAIRS A equals
DISJOINT_PAIRS A /\ { [{ g
.t1 : g.t1 in t1`2 & t1 in B }, { g.t2 : g.t2 in t2`1 & t2 in B }] : s in B
implies g.s in s`1 \/ s`2 };
coherence
proof
deffunc G(set)=$1`1 \/ $1`2;
defpred Q[Function] means $1.:B c= union { s`1 \/ s`2 : s in B };
defpred P[Function] means s in B implies $1.s in s`1 \/ s`2;
deffunc F(Element of Funcs(DISJOINT_PAIRS A, [A])) = [{ $1.s1 : $1.s1 in
s1`2 & s1 in B }, { $1.s2 : $1.s2 in s2`1 & s2 in B }];
set N = { F(g) : s in B implies g.s in s`1 \/ s`2 };
set N9 = { F(g) : g.:B c= union { s`1 \/ s`2 : s in B } };
set M = DISJOINT_PAIRS A /\ N;
A1: now
let X be set;
assume X in { s`1 \/ s`2 : s in B };
then ex s st X = s`1 \/ s`2 & s in B;
hence X is finite;
end;
A2: now
let g,h;
defpred P1[set] means g.$1 in $1`1;
defpred P2[set] means g.$1 in $1`2;
defpred Q1[set] means h.$1 in $1`1;
defpred Q2[set] means h.$1 in $1`2;
assume
A3: g|B = h|B;
then
A4: for s st s in B holds P1[s] iff Q1[s] by FRAENKEL:1;
A5: { g.s2 where s2 is Element of DISJOINT_PAIRS A: P1[s2] & s2 in B }
= { h.t2 where t2 is Element of DISJOINT_PAIRS A: Q1[t2] & t2 in B } from
FRAENKEL:sch 9(A3,A4);
A6: for s st s in B holds P2[s] iff Q2[s] by A3,FRAENKEL:1;
{ g.s1 where s1 is Element of DISJOINT_PAIRS A: P2[s1] & s1 in B }
= { h.t1 where t1 is Element of DISJOINT_PAIRS A: Q2[t1] & t1 in B } from
FRAENKEL:sch 9(A3,A6);
hence F(g) = F(h) by A5;
end;
A7: for g holds P[g] implies Q[g]
proof
let g such that
A8: for s holds s in B implies g.s in s`1 \/ s`2;
let x be object;
assume x in g.:B;
then consider y being object such that
A9: y in dom(g) and
A10: y in B and
A11: x = g.y by FUNCT_1:def 6;
reconsider y as Element of DISJOINT_PAIRS A by A9;
A12: y`1 \/ y`2 in { s`1 \/ s`2 : s in B } by A10;
g.y in y`1 \/ y`2 by A8,A10;
hence thesis by A11,A12,TARSKI:def 4;
end;
A13: { F(g) where g is Element of Funcs(DISJOINT_PAIRS A, [A]):P[g] } c= {
F(g) where g is Element of Funcs(DISJOINT_PAIRS A, [A]):Q[g] } from FRAENKEL:
sch 1(A7);
A14: B is finite;
{ G(s) : s in B } is finite from FRAENKEL:sch 21(A14);
then
A15: union { s`1 \/ s`2 : s in B } is finite by A1,FINSET_1:7;
A16: N9 is finite from FRAENKEL:sch 25(A14,A15,A2);
M c= DISJOINT_PAIRS A by XBOOLE_1:17;
hence thesis by A13,A16,FINSUB_1:def 5;
end;
correctness;
let C;
func B =>> C -> Element of Fin DISJOINT_PAIRS A equals
DISJOINT_PAIRS A /\ {
FinPairUnion(B,pair_diff A.:(f,incl DISJOINT_PAIRS A)) : f.:B c= C };
coherence
proof
deffunc F(Element of Funcs(DISJOINT_PAIRS A, [:Fin A,Fin A:])) =
FinPairUnion(B,pair_diff A.:($1,incl DISJOINT_PAIRS A));
set N = { FinPairUnion(B,pair_diff A.:(f,incl DISJOINT_PAIRS A)): f.:B c=
C };
set IT = DISJOINT_PAIRS A /\ N;
A17: IT c= DISJOINT_PAIRS A by XBOOLE_1:17;
A18: now
let f,f9;
assume f|B = f9|B;
then pair_diff A.:(f,incl DISJOINT_PAIRS A)|B = pair_diff A.:(f9,incl
DISJOINT_PAIRS A)|B by FUNCOP_1:23;
hence F(f)=F(f9) by NORMFORM:22;
end;
A19: C is finite;
A20: B is finite;
{ F(f): f.:B c= C } is finite from FRAENKEL:sch 25(A20,A19,A18);
hence thesis by A17,FINSUB_1:def 5;
end;
correctness;
end;
theorem Th11:
c in -B implies ex g st (for s st s in B holds g.s in s`1 \/ s`2
) & c = [{ g.t1 : g.t1 in t1`2 & t1 in B }, { g.t2 : g.t2 in t2`1 & t2 in B }]
proof
assume c in -B;
then
c in { [{ g.t1 : g.t1 in t1`2 & t1 in B }, { g.t2 : g.t2 in t2`1 & t2 in
B }] : s in B implies g.s in s`1 \/ s`2 } by XBOOLE_0:def 4;
then
ex g st c = [{ g.t1 : g.t1 in t1`2 & t1 in B }, { g.t2 : g.t2 in t2`1 &
t2 in B }] & for s st s in B holds g.s in s`1 \/ s`2;
hence thesis;
end;
theorem Th12:
[{},{}] is Element of DISJOINT_PAIRS A
proof
[{},{}] = [{}.A,{}.A] & [{},{}]`1 misses [{},{}]`2;
hence thesis by NORMFORM:29;
end;
theorem Th13:
for K st K = {} holds -K = {[{},{}]}
proof
let K;
assume
A1: K = {};
A2: { [{ g.t1 : g.t1 in t1`2 & t1 in K }, { g.t2 : g.t2 in t2`1 & t2 in K }]
: s in K implies g.s in s`1 \/ s`2 } = {[{},{}]}
proof
thus { [{ g.t1 : g.t1 in t1`2 & t1 in K }, { g.t2 : g.t2 in t2`1 & t2 in K
} ] : s in K implies g.s in s`1 \/ s`2 } c= {[{},{}]}
proof
let x be object;
assume x in { [{ g.t1 : g.t1 in t1`2 & t1 in K }, { g.t2 : g.t2 in t2`1
& t2 in K }] : s in K implies g.s in s`1 \/ s`2 };
then consider g such that
A3: x = [{ g.t1 : g.t1 in t1`2 & t1 in K }, { g.t2 : g.t2 in t2`1 &
t2 in K }] and
s in K implies g.s in s`1 \/ s`2;
A4: x`2 = { g.t2 : g.t2 in t2`1 & t2 in K } by A3;
A5: now
set y = the Element of x`2;
assume x`2 <> {};
then y in x`2;
then ex t1 st y = g.t1 & g.t1 in t1`1 & t1 in K by A4;
hence contradiction by A1;
end;
A6: x`1 = { g.t1 : g.t1 in t1`2 & t1 in K } by A3;
now
set y = the Element of x`1;
assume x`1 <> {};
then y in x`1;
then ex t1 st y = g.t1 & g.t1 in t1`2 & t1 in K by A6;
hence contradiction by A1;
end;
then x = [{},{}] by A3,A5;
hence thesis by TARSKI:def 1;
end;
thus {[{},{}]} c= { [{ g.t1 : g.t1 in t1`2 & t1 in K }, { g.t2 : g.t2 in
t2`1 & t2 in K }] : s in K implies g.s in s`1 \/ s`2 }
proof
set g = the Element of Funcs(DISJOINT_PAIRS A, [A]);
let x be object;
assume x in {[{},{}]};
then
A7: x = [{},{}] by TARSKI:def 1;
A8: now
set y = the Element of { g.t1 : g.t1 in t1`2 & t1 in K };
assume { g.t1 : g.t1 in t1`2 & t1 in K } <> {};
then y in { g.t1 : g.t1 in t1`2 & t1 in K };
then ex t1 st y = g.t1 & g.t1 in t1`2 & t1 in K;
hence contradiction by A1;
end;
A9: now
set y = the Element of { g.t2 : g.t2 in t2`1 & t2 in K };
assume { g.t2 : g.t2 in t2`1 & t2 in K } <> {};
then y in { g.t2 : g.t2 in t2`1 & t2 in K };
then ex t1 st y = g.t1 & g.t1 in t1`1 & t1 in K;
hence contradiction by A1;
end;
s in K implies g.s in s`1 \/ s`2 by A1;
hence thesis by A7,A8,A9;
end;
end;
[{},{}] is Element of DISJOINT_PAIRS A by Th12;
hence thesis by A2,ZFMISC_1:46;
end;
theorem Th14:
for K,L st K = {} & L = {} holds K =>> L = {[{},{}]}
proof
let K,L;
assume that
A1: K = {} and
L = {};
A2: {} = {}.A;
A3: K = {}.DISJOINT_PAIRS A by A1;
A4: now
let f;
thus FinPairUnion(K,pair_diff A.:(f,incl DISJOINT_PAIRS A)) =
the_unity_wrt FinPairUnion A by A3,NORMFORM:18,SETWISEO:31
.= [{},{}] by A2,NORMFORM:19;
end;
A5: { FinPairUnion(K,pair_diff A.:(f,incl DISJOINT_PAIRS A)) : f.:K c= L } =
{[{},{}]}
proof
thus { FinPairUnion(K,pair_diff A.:(f,incl DISJOINT_PAIRS A)) : f.:K c= L
} c= {[{},{}]}
proof
let x be object;
assume x in { FinPairUnion(K,pair_diff A.:(f,incl DISJOINT_PAIRS A)) :
f.:K c= L };
then
ex f st x = FinPairUnion(K,pair_diff A.:(f,incl DISJOINT_PAIRS A)) &
f.:K c= L;
then x = [{},{}] by A4;
hence thesis by TARSKI:def 1;
end;
thus {[{},{}]} c= { FinPairUnion(K,pair_diff A.:(f,incl DISJOINT_PAIRS A))
: f.: K c= L }
proof
set f9 = the (Element of Funcs(DISJOINT_PAIRS A, [:Fin A,Fin A:]));
let x be object;
assume x in {[{},{}]};
then x = [{},{}] by TARSKI:def 1;
then
A6: x = FinPairUnion(K,pair_diff A.:(f9,incl DISJOINT_PAIRS A)) by A4;
f9.:K c= L by A1;
hence thesis by A6;
end;
end;
[{},{}] is Element of DISJOINT_PAIRS A by Th12;
hence thesis by A5,ZFMISC_1:46;
end;
theorem Th15:
for a being Element of DISJOINT_PAIRS {} holds a = [{},{}]
proof
let a be Element of DISJOINT_PAIRS {};
consider x,y being Element of Fin {} such that
A1: a = [x,y] by DOMAIN_1:1;
x = {} by FINSUB_1:15,TARSKI:def 1;
hence thesis by A1,FINSUB_1:15,TARSKI:def 1;
end;
theorem Th16:
DISJOINT_PAIRS {} = {[{},{}]}
proof
thus DISJOINT_PAIRS {} c= {[{},{}]}
proof
let x be object;
assume x in DISJOINT_PAIRS {};
then x = [{},{}] by Th15;
hence thesis by TARSKI:def 1;
end;
thus {[{},{}]} c= DISJOINT_PAIRS {}
proof
let x be object;
assume x in {[{},{}]};
then x = [{},{}] by TARSKI:def 1;
then x is Element of DISJOINT_PAIRS {} by Th12;
hence thesis;
end;
end;
Lm4: Fin DISJOINT_PAIRS {} = { {}, {[{},{}]}}
proof
thus Fin DISJOINT_PAIRS {} = bool DISJOINT_PAIRS {} by Th16,FINSUB_1:14
.= { {}, {[{},{}]}} by Th16,ZFMISC_1:24;
end;
theorem Th17:
{[{},{}]} is Element of Normal_forms_on A
proof
[{},{}] is Element of DISJOINT_PAIRS A by Th12;
then {[{},{}]} c= DISJOINT_PAIRS A by ZFMISC_1:31;
then reconsider B = {[{},{}]} as Element of Fin DISJOINT_PAIRS A by
FINSUB_1:def 5;
now
let a,b be Element of DISJOINT_PAIRS A;
assume that
A1: a in B and
A2: b in B and
a c= b;
a = [{},{}] by A1,TARSKI:def 1;
hence a = b by A2,TARSKI:def 1;
end;
hence thesis by NORMFORM:33;
end;
theorem Th18:
c in B =>> C implies ex f st f.:B c= C & c = FinPairUnion(B,
pair_diff A.:(f,incl DISJOINT_PAIRS A))
proof
assume c in B =>> C;
then
c in { FinPairUnion(B,pair_diff A.:(f,incl DISJOINT_PAIRS A)) : f.:B c=
C } by XBOOLE_0:def 4;
then
ex f st c = FinPairUnion(B,pair_diff A.:(f,incl DISJOINT_PAIRS A)) & f.:
B c= C;
hence thesis;
end;
theorem Th19:
K ^ { a } = {} implies ex b st b in -K & b c= a
proof
assume
A1: K ^ { a } = {};
now
per cases;
suppose
A2: A is non empty;
defpred P[set,set] means $2 in $1`1 /\ a`2 \/ $1`2 /\ a`1;
A3: A = [A] by A2,Def2;
A4: now
A5: a in { a } by TARSKI:def 1;
let s;
assume s in K;
then not s \/ a in DISJOINT_PAIRS A by A1,A5,NORMFORM:35;
then consider x being Element of [A] such that
A6: x in s`1 & x in a`2 or x in a`1 & x in s`2 by A3,NORMFORM:28;
take x;
x in s`1 /\ a`2 or x in s`2 /\ a`1 by A6,XBOOLE_0:def 4;
hence P[s,x] by XBOOLE_0:def 3;
end;
consider g such that
A7: s in K implies P[s,g.s] from FRAENKEL:sch 27(A4);
set c1 = { g.t1 : g.t1 in t1`2 & t1 in K }, c2 = { g.t2 : g.t2 in t2`1 &
t2 in K };
A8: c2 c= a`2
proof
let x be object;
assume x in c2;
then consider t such that
A9: x = g.t & g.t in t`1 and
A10: t in K;
g.t in t`1 /\ a`2 \/ t`2 /\ a`1 by A7,A10;
then g.t in t`1 /\ a`2 or g.t in t`2 /\ a`1 by XBOOLE_0:def 3;
then g.t in t`1 & g.t in a`2 or g.t in t`2 & g.t in a`1 by
XBOOLE_0:def 4;
hence thesis by A9,NORMFORM:27;
end;
A11: c1 c= a`1
proof
let x be object;
assume x in c1;
then consider t such that
A12: x = g.t & g.t in t`2 and
A13: t in K;
g.t in t`1 /\ a`2 \/ t`2 /\ a`1 by A7,A13;
then g.t in t`1 /\ a`2 or g.t in t`2 /\ a`1 by XBOOLE_0:def 3;
then g.t in t`1 & g.t in a`2 or g.t in t`2 & g.t in a`1 by
XBOOLE_0:def 4;
hence thesis by A12,NORMFORM:27;
end;
then reconsider c = [c1,c2] as Element of DISJOINT_PAIRS A by A8,
NORMFORM:30;
take c;
now
let s;
assume s in K;
then g.s in s`1 /\ a`2 \/ s`2 /\ a`1 by A7;
then g.s in s`1 /\ a`2 or g.s in s`2 /\ a`1 by XBOOLE_0:def 3;
then g.s in s`1 & g.s in a`2 or g.s in s`2 & g.s in a`1 by
XBOOLE_0:def 4;
hence g.s in s`1 \/ s`2 by XBOOLE_0:def 3;
end;
then c in { [{ h.t1 : h.t1 in t1`2 & t1 in K }, { h.t2 : h.t2 in t2`1 &
t2 in K }] : s in K implies h.s in s`1 \/ s`2 };
hence c in -K by XBOOLE_0:def 4;
thus c c= a by A11,A8;
end;
suppose
A14: not A is non empty;
reconsider Z = {[{},{}]} as Element of Normal_forms_on {} by Th17;
take b=a;
A15: a = [{},{}] by A14,Th15;
mi (Z^Z) <> {} by Th3;
then K <> {[{},{}]} by A1,A14,A15,NORMFORM:40,XBOOLE_1:3;
then K = {} by A14,Lm4,TARSKI:def 2;
then -K = {[{},{}]} by Th13;
hence b in -K by A15,TARSKI:def 1;
thus b c= a;
end;
end;
hence thesis;
end;
Lm5: now
let A,K,b,f;
thus (pair_diff A.:(f,incl DISJOINT_PAIRS A)).b = pair_diff A.(f.b,(incl
DISJOINT_PAIRS A).b) by FUNCOP_1:37
.= pair_diff A.(f.b,b) by FUNCT_1:18
.= f.b \ b by Def5;
end;
theorem Th20:
(for c st c in u ex b st b in v & b c= c \/ a) implies ex b st b
in @u =>> @v & b c= a
proof
defpred P[Element of DISJOINT_PAIRS A,Element of [:Fin A, Fin A:]] means $2
in @v & $2 c= $1 \/ a;
assume
A1: for b st b in u ex c st c in v & c c= b \/ a;
A2: now
let b;
assume b in @u;
then consider c such that
A3: c in v & c c= b \/ a by A1;
reconsider c as Element of [:Fin A, Fin A:];
take x = c;
thus P[b,x] by A3;
end;
consider f9 such that
A4: b in @u implies P[b,f9.b] from FRAENKEL:sch 27(A2);
set d = FinPairUnion(@u,pair_diff A.:(f9,incl DISJOINT_PAIRS A));
A5: now
let s;
assume s in u;
then
A6: f9.s c= a \/ s by A4;
(pair_diff A.:(f9,incl DISJOINT_PAIRS A)).s = f9.s \ s by Lm5;
hence (pair_diff A.: (f9,incl DISJOINT_PAIRS A)).s c= a by A6,NORMFORM:15;
end;
then reconsider d as Element of DISJOINT_PAIRS A by NORMFORM:21,26;
take d;
b in u implies f9.b in v by A4;
then f9.:(@u) c= v by SETWISEO:10;
then d in { FinPairUnion(@u,pair_diff A.:(f,incl DISJOINT_PAIRS A)) : f.:@u
c= v };
hence d in @u =>> @v by XBOOLE_0:def 4;
thus thesis by A5,NORMFORM:21;
end;
Lm6: a in K ^ (K =>> @u) implies ex b st b in u & b c= a
proof
assume a in K ^ (K =>> @u);
then consider b,c such that
A1: b in K and
A2: c in K =>> @u and
A3: a = b \/ c by NORMFORM:34;
consider f such that
A4: f.:K c= u and
A5: c = FinPairUnion(K,pair_diff A.:(f,incl DISJOINT_PAIRS A)) by A2,Th18;
A6: f.b in f.:K by A1,FUNCT_2:35;
u = @u;
then reconsider d = f.b as Element of DISJOINT_PAIRS A by A4,A6,SETWISEO:9;
take d;
thus d in u by A4,A6;
(pair_diff A.:(f,incl DISJOINT_PAIRS A)).b = f.b \ b by Lm5;
hence thesis by A1,A3,A5,NORMFORM:14,16;
end;
theorem Th21:
K ^ -K = {}
proof
set x = the Element of K ^ -K;
assume
A1: K ^ -K <> {};
then reconsider a = x as Element of DISJOINT_PAIRS A by SETWISEO:9;
consider b,c such that
A2: b in K and
A3: c in -K and
A4: a = b \/ c by A1,NORMFORM:34;
A5: a`1 = b`1 \/ c`1 by A4;
A6: a`2 = b`2 \/ c`2 by A4;
consider g such that
A7: s in K implies g.s in s`1 \/ s`2 and
A8: c = [{ g.t1 : g.t1 in t1`2 & t1 in K }, { g.t2 : g.t2 in t2`1 & t2
in K }] by A3,Th11;
A9: g.b in b`1 \/ b`2 by A2,A7;
now
per cases by A9,XBOOLE_0:def 3;
case
A10: g.b in b`1;
hence g.b in a`1 by A5,XBOOLE_0:def 3;
g.b in { g.t2 : g.t2 in t2`1 & t2 in K } by A2,A10;
then g.b in c`2 by A8;
hence g.b in a`2 by A6,XBOOLE_0:def 3;
end;
case
A11: g.b in b`2;
hence g.b in a`2 by A6,XBOOLE_0:def 3;
g.b in { g.t1 : g.t1 in t1`2 & t1 in K } by A2,A11;
then g.b in c`1 by A8;
hence g.b in a`1 by A5,XBOOLE_0:def 3;
end;
end;
then a`1 /\ a`2 <> {} by XBOOLE_0:def 4;
then a`1 meets a`2;
hence contradiction by NORMFORM:25;
end;
definition
let A;
func pseudo_compl(A) -> UnOp of the carrier of NormForm A means
:Def8:
it.u = mi(-@u);
existence
proof
deffunc F(Element of NormForm A) = mi(-@$1);
consider IT being Function of the carrier of NormForm A, Normal_forms_on A
such that
A1: IT.u = F(u) from FUNCT_2:sch 4;
reconsider IT as UnOp of the carrier of NormForm A by NORMFORM:def 12;
take IT;
let u;
thus thesis by A1;
end;
correctness
proof
let IT,IT9 be UnOp of the carrier of NormForm A;
assume that
A2: IT.u = mi (-@u) and
A3: IT9.u = mi (-@u);
now
let u;
thus IT.u = mi (-@u) by A2
.= IT9.u by A3;
end;
hence IT = IT9 by FUNCT_2:63;
end;
func StrongImpl(A) -> BinOp of the carrier of NormForm A means
:Def9:
it.(u, v) = mi (@u =>> @v);
existence
proof
deffunc F(Element of NormForm A, Element of NormForm A) = mi (@$1 =>> @$2);
consider IT being Function of [:(the carrier of NormForm A), the carrier
of NormForm A:], Normal_forms_on A such that
A4: IT.(u,v) = F(u,v) from BINOP_1:sch 4;
reconsider IT as BinOp of the carrier of NormForm A by NORMFORM:def 12;
take IT;
let u,v;
thus thesis by A4;
end;
correctness
proof
let IT,IT9 be BinOp of the carrier of NormForm A;
assume that
A5: IT.(u,v) = mi (@u =>> @v) and
A6: IT9.(u,v) = mi (@u =>> @v);
now
let u,v;
thus IT.(u,v) = mi (@u =>> @v) by A5
.= IT9.(u,v) by A6;
end;
hence IT = IT9 by BINOP_1:2;
end;
let u;
func SUB u -> Element of Fin the carrier of NormForm A equals
bool u;
coherence
proof
A7: bool u c= the carrier of NormForm A
proof
let x be object;
assume x in bool u;
then x is Element of NormForm A by Th5;
hence thesis;
end;
u = @u;
hence thesis by A7,FINSUB_1:def 5;
end;
correctness;
func diff(u) -> UnOp of the carrier of NormForm A means
:Def11:
it.v = u \ v;
existence
proof
deffunc F(Element of NormForm A) = @u \ @$1;
consider IT being Function of the carrier of NormForm A, Fin
DISJOINT_PAIRS A such that
A8: IT.v = F(v) from FUNCT_2:sch 4;
now
let v be Element of NormForm A;
@u \ @v in Normal_forms_on A by Th4,XBOOLE_1:36;
then IT.v in Normal_forms_on A by A8;
hence IT.v in the carrier of NormForm A by NORMFORM:def 12;
end;
then reconsider IT as UnOp of the carrier of NormForm A by Th1;
take IT;
let v;
v = @v;
hence thesis by A8;
end;
correctness
proof
let IT,IT9 be UnOp of the carrier of NormForm A;
assume that
A9: IT.v = u \ v and
A10: IT9.v = u \ v;
now
let v be Element of NormForm A;
thus IT.v = u \ v by A9
.= IT9.v by A10;
end;
hence IT = IT9 by FUNCT_2:63;
end;
end;
deffunc J(set) = the L_join of NormForm $1;
deffunc M(set) = the L_meet of NormForm $1;
Lm7: for u,v st v in SUB u holds v "\/" (diff u).v = u
proof
let u,v;
assume
A1: v in SUB u;
A2: @u \ @v = @((diff u).v) by Def11;
thus v "\/" (diff u).v = J(A).(v, (diff u).v) by LATTICES:def 1
.= mi ( @v \/ (@u \ @v)) by A2,NORMFORM:def 12
.= mi (@u) by A1,XBOOLE_1:45
.= u by NORMFORM:42;
end;
theorem Th22:
(diff u).v [= u
proof
(diff u).v = u \ v by Def11;
then for a st a in (diff u).v ex b st b in u & b c= a;
hence thesis by Lm3;
end;
Lm8: ex v st v in SUB u & @v ^ { a } = {} & for b st b in (diff u).v holds b
\/ a in DISJOINT_PAIRS A
proof
defpred Q[set] means not contradiction;
deffunc F(set)=$1;
defpred P[Element of DISJOINT_PAIRS A] means not $1 \/ a in DISJOINT_PAIRS A;
set M = { F(s) : F(s) in u & P[s]};
deffunc F1(Element of DISJOINT_PAIRS A) = $1 \/ a;
defpred P1[set] means $1 in u;
defpred P2[Element of DISJOINT_PAIRS A] means P1[$1] & P[$1];
A1: { F1(t) where t is Element of DISJOINT_PAIRS A : t in {s where s is
Element of DISJOINT_PAIRS A: P2[s]} & Q[t]} = { F1(s) where s is Element of
DISJOINT_PAIRS A: P2[s] & Q[s] } from FRAENKEL:sch 14;
defpred F[set,set] means $1 in M;
defpred D[set,set] means $1 in M & $2 in { a };
A2: { F1(s1) : P2[s1] & Q[s1] } = { F1(s2) : P2[s2]}
proof
thus { F1(s1) : P2[s1] & Q[s1] } c= { F1(s2) : P2[s2]}
proof
let x be object;
assume x in { F1(s1) : P2[s1] & Q[s1] };
then ex s1 st x=F1(s1) &( P2[s1])& Q[s1];
hence thesis;
end;
let x be object;
assume x in { F1(s1) : P2[s1] };
then ex s1 st x=F1(s1) & P2[s1];
hence thesis;
end;
A3: M c= u from FRAENKEL:sch 17;
then reconsider v = M as Element of NormForm A by Th5;
take v;
thus v in SUB u by A3;
defpred E[set,set] means $2 = a & $1 in M;
deffunc G(Element of DISJOINT_PAIRS A, Element of DISJOINT_PAIRS A)=$1 \/ $2;
A4: { F1(t) : t in {s : P2[s]} & Q[t]} = { F1(t1) : t1 in {s1 : P2[s1]}}
proof
thus { F1(t) : t in {s : P2[s]} & Q[t]} c= { F1(t1) : t1 in {s1 : P2[s1]}}
proof
let x be object;
assume x in { F1(t) : t in {s : P2[s]} & Q[t]};
then ex t st x=F1(t) & t in {s : P2[s]} & Q[t];
hence thesis;
end;
let x be object;
assume x in { F1(t) : t in {s : P2[s]}};
then ex t st x=F1(t) & t in {s : P2[s]};
hence thesis;
end;
A5: { G(s,t) where t is Element of DISJOINT_PAIRS A : t = a & F[s,t] } = {
G(s9,a): F[s9,a]} from FRAENKEL:sch 20;
A6: D[s,t] iff E[s,t] by TARSKI:def 1;
A7: { G(s,t): D[s,t] } = { G(s9,t9): E[s9,t9] } from FRAENKEL:sch 4(A6);
{ F1(s): P1[s] & not F1(s) in DISJOINT_PAIRS A } misses DISJOINT_PAIRS A
from FRAENKEL:sch 18;
hence @v ^ { a } = {} by A1,A4,A2,A7,A5;
let b;
assume b in (diff u).v;
then
A8: b in u \ v by Def11;
then not b in M by XBOOLE_0:def 5;
hence thesis by A8;
end;
theorem Th23:
u "/\" pseudo_compl(A).u = Bottom NormForm A
proof
reconsider zero = {} as Element of Normal_forms_on A by NORMFORM:31;
A1: @(pseudo_compl(A).u) = mi(-@u) by Def8;
thus u "/\" pseudo_compl(A).u = M(A).(u, pseudo_compl(A).u) by LATTICES:def 2
.= mi(@u ^ mi(-@u)) by A1,NORMFORM:def 12
.= mi(@u ^ -@u) by NORMFORM:51
.= mi(zero) by Th21
.= {} by NORMFORM:40,XBOOLE_1:3
.= Bottom NormForm A by NORMFORM:57;
end;
theorem Th24:
u "/\" StrongImpl(A).(u, v) [= v
proof
now
let a;
assume
A1: a in u "/\" StrongImpl(A).(u, v);
A2: @(StrongImpl(A).(u, v)) = mi(@u =>> @v) by Def9;
u "/\" StrongImpl(A).(u, v) = M(A).(u, StrongImpl(A).(u, v)) by
LATTICES:def 2
.= mi(@u ^ mi(@u =>> @v)) by A2,NORMFORM:def 12
.= mi(@u ^ (@u =>> @v)) by NORMFORM:51;
then a in @u ^ (@u =>> @v) by A1,NORMFORM:36;
hence ex b st b in v & b c= a by Lm6;
end;
hence thesis by Lm3;
end;
theorem Th25:
@u ^ { a } = {} implies Atom(A).a [= pseudo_compl(A).u
proof
assume
A1: @u ^ { a } = {};
now
let c;
assume c in Atom(A).a;
then c = a by Th6;
then consider b such that
A2: b in -@u and
A3: b c= c by A1,Th19;
consider d such that
A4: d c= b and
A5: d in mi(-@u) by A2,NORMFORM:41;
take e = d;
thus e in pseudo_compl(A).u by A5,Def8;
thus e c= c by A3,A4,NORMFORM:2;
end;
hence thesis by Lm3;
end;
theorem Th26:
(for b st b in u holds b \/ a in DISJOINT_PAIRS A ) & u "/\"
Atom(A).a [= w implies Atom(A).a [= StrongImpl(A).(u, w)
proof
assume that
A1: for b st b in u holds b \/ a in DISJOINT_PAIRS A and
A2: u "/\" Atom(A).a [= w;
A3: now
let c;
assume
A4: c in u;
then
A5: c \/ a is Element of DISJOINT_PAIRS A by A1;
a in @(Atom(A).a) by Th7;
then c \/ a in @u ^ @(Atom(A).a) by A1,A4,NORMFORM:35;
then consider b such that
A6: b c= c \/ a and
A7: b in mi(@u ^ @(Atom(A).a)) by A5,NORMFORM:41;
b in M(A).(u, Atom(A).a) by A7,NORMFORM:def 12;
then b in u "/\" Atom(A).a by LATTICES:def 2;
then consider d such that
A8: d in w and
A9: d c= b by A2,Lm2;
take e = d;
thus e in w by A8;
thus e c= c \/ a by A6,A9,NORMFORM:2;
end;
now
let c;
assume c in Atom(A).a;
then c = a by Th6;
then consider b such that
A10: b in @u =>> @w and
A11: b c= c by A3,Th20;
consider d such that
A12: d c= b and
A13: d in mi(@u =>> @w) by A10,NORMFORM:41;
take e = d;
thus e in (StrongImpl(A).(u, w)) by A13,Def9;
thus e c= c by A11,A12,NORMFORM:2;
end;
hence thesis by Lm3;
end;
Lm9: now
let A,u,v;
deffunc IMPL(Element of NormForm A, Element of NormForm A) = FinJoin(SUB $1,
M(A).: (pseudo_compl(A), StrongImpl(A)[:](diff $1, $2)));
set Psi = M(A).:(pseudo_compl(A), StrongImpl(A)[:](diff u, v));
A1: now
let w;
set u2 = (diff u).w, pc = pseudo_compl(A).w, si = StrongImpl(A).(u2, v);
A2: w "/\" (pc "/\" si) = (w "/\" pc) "/\" si by LATTICES:def 7
.= Bottom NormForm A "/\" si by Th23
.= Bottom NormForm A;
assume w in SUB u;
then
A3: w "\/" u2 = u by Lm7;
M(A)[;](u, Psi).w = M(A).(u, Psi.w) by FUNCOP_1:53
.= u "/\" Psi.w by LATTICES:def 2
.= u "/\" M(A).(pc, StrongImpl(A)[:](diff u, v).w) by FUNCOP_1:37
.= u "/\" (pc "/\" StrongImpl(A)[:](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(A)[;](u, Psi).w [= u2 "/\" si by LATTICES:6;
u2 "/\" si [= v by Th24;
hence M(A)[;](u, Psi).w [= v by A4,LATTICES:7;
end;
u "/\" IMPL(u,v) = FinJoin(SUB u, M(A)[;](u, Psi)) by LATTICE2:66;
hence u "/\" IMPL(u,v) [= v by A1,LATTICE2:54;
let w;
assume
A5: u "/\" v [= w;
A6: v = FinJoin(@v, Atom(A)) by Th10;
then
A7: u "/\" v = FinJoin(@v, M(A)[;](u, Atom(A))) by LATTICE2:66;
now
set pf = pseudo_compl(A), sf = StrongImpl(A)[:](diff u, w);
let a;
assume a in @v;
then M(A)[;](u, Atom(A)).a [= w by A7,A5,LATTICE2:31;
then M(A).(u, Atom(A).a) [= w by FUNCOP_1:53;
then
A8: u "/\" Atom(A).a [= w by LATTICES:def 2;
consider v such that
A9: v in SUB u and
A10: @v ^ { a } = {} and
A11: for b st b in (diff u).v holds b \/ a in DISJOINT_PAIRS A by Lm8;
(diff u).v "/\" Atom(A).a [= u "/\" Atom(A).a by Th22,LATTICES:9;
then (diff u).v "/\" Atom(A).a [= w by A8,LATTICES:7;
then Atom(A).a [= StrongImpl(A).((diff u).v, w) by A11,Th26;
then
A12: Atom(A).a [= sf.v by FUNCOP_1:48;
A13: pf.v "/\" sf.v = M(A).(pf.v, sf.v) by LATTICES:def 2
.= M(A).:(pf, sf).v by FUNCOP_1:37;
Atom(A).a [= pf.v by A10,Th25;
then Atom(A).a [= M(A).:(pf, sf).v by A12,A13,FILTER_0:7;
hence Atom(A).a [= IMPL(u,w) by A9,LATTICE2:29;
end;
hence v [= IMPL(u,w) by A6,LATTICE2:54;
end;
Lm10: NormForm A is implicative
proof
let p,q be Element of NormForm A;
take r = FinJoin(SUB p,M(A).:(pseudo_compl(A), StrongImpl(A)[:](diff p, q)));
thus p "/\" r [= q & for r1 being Element of NormForm A st p "/\" r1 [= q
holds r1 [= r by Lm9;
end;
registration
let A;
cluster NormForm A -> implicative;
coherence by Lm10;
end;
theorem Th27:
u => v = FinJoin(SUB u, (the L_meet of NormForm A).:(
pseudo_compl(A), StrongImpl(A)[:](diff u, v)))
proof
deffunc IMPL(Element of NormForm A, Element of NormForm A) = FinJoin(SUB $1,
M(A).: (pseudo_compl(A), StrongImpl(A)[:](diff $1, $2)));
u "/\" IMPL(u,v) [= v & for w st u "/\" w [= v holds w [= IMPL(u,v) by Lm9;
hence thesis by FILTER_0:def 7;
end;
theorem
Top NormForm A = {[{},{}]}
proof
reconsider O = {[{},{}]} as Element of Normal_forms_on A by Th17;
set sd = StrongImpl(A)[:](diff Bottom NormForm A, Bottom NormForm A);
set F=M(A).:(pseudo_compl(A), sd);
A1: @(pseudo_compl(A).Bottom NormForm A) = mi(-@Bottom NormForm A) by Def8
.= mi O by Th13,NORMFORM:57
.= O by NORMFORM:42;
A2: Bottom NormForm A = {} by NORMFORM:57;
then (diff Bottom NormForm A).Bottom NormForm A = {} \ {} by Def11
.= Bottom NormForm A by NORMFORM:57;
then
A3: @(sd.Bottom NormForm A) = StrongImpl(A).(Bottom NormForm A, Bottom
NormForm A) by FUNCOP_1:48
.= mi(@Bottom NormForm A =>> @Bottom NormForm A) by Def9
.= mi O by A2,Th14
.= O by NORMFORM:42;
thus Top NormForm A = (Bottom NormForm A) => Bottom NormForm A by FILTER_0:28
.= FinJoin(SUB Bottom NormForm A,F) by Th27
.= J(A)$$(SUB Bottom NormForm A,F) by LATTICE2:def 3
.= F.Bottom NormForm A by A2,SETWISEO:17,ZFMISC_1:1
.= M(A).(pseudo_compl(A).Bottom NormForm A, sd.Bottom NormForm A) by
FUNCOP_1:37
.= mi (O^O) by A1,A3,NORMFORM:def 12
.= {[{},{}]} by Th3;
end;