:: Algebra of Normal Forms Is a Heyting Algebra :: by Andrzej Trybulec :: :: Received January 3, 1991 :: Copyright (c) 1991-2021 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; begin :: Preliminaries theorem :: HEYTING1:1 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; 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 :: HEYTING1:def 1 for a st a in B holds a in C; end; reserve A for set; definition let A; assume A is non empty; func [A] -> non empty set equals :: HEYTING1:def 2 A; 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 :: HEYTING1:2 B = {} implies mi B = {}; registration let A; cluster non empty for Element of Normal_forms_on A; end; definition let A,a; redefine func { a } -> Element of Normal_forms_on A; end; definition let A; let u be Element of NormForm A; func @u -> Element of Normal_forms_on A equals :: HEYTING1:def 3 u; end; reserve K,L for Element of Normal_forms_on A; theorem :: HEYTING1:3 mi (K^K) = K; theorem :: HEYTING1:4 for X being set st X c= K holds X in Normal_forms_on A; theorem :: HEYTING1:5 for X being set st X c= u holds X is Element of NormForm A; definition let A; func Atom(A) -> Function of DISJOINT_PAIRS A, the carrier of NormForm A means :: HEYTING1:def 4 it.a = { a }; end; theorem :: HEYTING1:6 c in Atom(A).a implies c = a; theorem :: HEYTING1:7 a in Atom(A).a; theorem :: HEYTING1:8 Atom(A).a = singleton DISJOINT_PAIRS A .a; theorem :: HEYTING1:9 FinJoin(K, Atom(A)) = FinUnion(K, singleton DISJOINT_PAIRS A); theorem :: HEYTING1:10 u = FinJoin(@u, Atom(A)); 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 :: HEYTING1:def 5 for a,b being Element of [:Fin A, Fin A:] holds it.(a,b) = a \ b; end; definition let A,B; func -B -> Element of Fin DISJOINT_PAIRS A equals :: HEYTING1:def 6 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 }; let C; func B =>> C -> Element of Fin DISJOINT_PAIRS A equals :: HEYTING1:def 7 DISJOINT_PAIRS A /\ { FinPairUnion(B,pair_diff A.:(f,incl DISJOINT_PAIRS A)) : f.:B c= C }; end; theorem :: HEYTING1:11 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 }]; theorem :: HEYTING1:12 [{},{}] is Element of DISJOINT_PAIRS A; theorem :: HEYTING1:13 for K st K = {} holds -K = {[{},{}]}; theorem :: HEYTING1:14 for K,L st K = {} & L = {} holds K =>> L = {[{},{}]}; theorem :: HEYTING1:15 for a being Element of DISJOINT_PAIRS {} holds a = [{},{}]; theorem :: HEYTING1:16 DISJOINT_PAIRS {} = {[{},{}]}; theorem :: HEYTING1:17 {[{},{}]} is Element of Normal_forms_on A; theorem :: HEYTING1:18 c in B =>> C implies ex f st f.:B c= C & c = FinPairUnion(B, pair_diff A.:(f,incl DISJOINT_PAIRS A)); theorem :: HEYTING1:19 K ^ { a } = {} implies ex b st b in -K & b c= a; theorem :: HEYTING1:20 (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; theorem :: HEYTING1:21 K ^ -K = {}; definition let A; func pseudo_compl(A) -> UnOp of the carrier of NormForm A means :: HEYTING1:def 8 it.u = mi(-@u); func StrongImpl(A) -> BinOp of the carrier of NormForm A means :: HEYTING1:def 9 it.(u, v) = mi (@u =>> @v); let u; func SUB u -> Element of Fin the carrier of NormForm A equals :: HEYTING1:def 10 bool u; func diff(u) -> UnOp of the carrier of NormForm A means :: HEYTING1:def 11 it.v = u \ v; end; theorem :: HEYTING1:22 (diff u).v [= u; theorem :: HEYTING1:23 u "/\" pseudo_compl(A).u = Bottom NormForm A; theorem :: HEYTING1:24 u "/\" StrongImpl(A).(u, v) [= v; theorem :: HEYTING1:25 @u ^ { a } = {} implies Atom(A).a [= pseudo_compl(A).u; theorem :: HEYTING1:26 (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); registration let A; cluster NormForm A -> implicative; end; theorem :: HEYTING1:27 u => v = FinJoin(SUB u, (the L_meet of NormForm A).:( pseudo_compl(A), StrongImpl(A)[:](diff u, v))); theorem :: HEYTING1:28 Top NormForm A = {[{},{}]};