environ
vocabularies HIDDEN, NUMBERS, PBOOLE, FUNCT_1, CARD_3, RELAT_1, TARSKI, FINSEQ_1, ORDINAL4, XBOOLE_0, SUBSET_1, HILBERT1, TREES_1, TREES_A, CARD_1, ARYTM_3, TREES_2, TREES_4, TREES_3, TREES_9, FUNCT_6, QC_LANG1, XBOOLEAN, ZF_LANG, GLIB_000, XXREAL_0, NAT_1, ORDINAL1, ZFMISC_1, PARTFUN1, FUNCT_4, FUNCOP_1, HILBERT2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, CARD_3, RELAT_1, FUNCT_1, PARTFUN1, XCMPLX_0, NAT_1, FINSEQ_1, FUNCOP_1, FUNCT_4, FUNCT_6, PBOOLE, TREES_1, TREES_2, TREES_3, TREES_4, TREES_9, HILBERT1, XXREAL_0;
definitions TARSKI, FUNCT_1, HILBERT1, PARTFUN1;
theorems PBOOLE, ZFMISC_1, FUNCT_1, HILBERT1, ORDERS_1, SUBSET_1, TARSKI, FUNCT_4, FUNCOP_1, WELLFND1, CARD_3, GRFUNC_1, NAT_1, FINSEQ_1, TREES_1, TREES_4, TREES_2, TREES_9, FINSEQ_2, TREES_3, RELAT_1, ORDINAL1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, CARD_1, PARTFUN1, EQREL_1;
schemes PBOOLE, NAT_1, FINSEQ_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, XREAL_0, NAT_1, FINSEQ_1, TREES_2, TREES_3, HILBERT1, TREES_4;
constructors HIDDEN, FUNCT_4, XREAL_0, NAT_1, CARD_3, TREES_4, HILBERT1, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities HILBERT1, FUNCOP_1;
expansions TARSKI, FUNCT_1, HILBERT1;
scheme
HPMSSExL{
F1()
-> set ,
F2(
Element of
NAT )
-> set ,
P1[
Element of
HP-WFF ,
Element of
HP-WFF ,
set ,
set ,
set ],
P2[
Element of
HP-WFF ,
Element of
HP-WFF ,
set ,
set ,
set ] } :
provided
A1:
for
p,
q being
Element of
HP-WFF for
a,
b being
set ex
c being
set st
P1[
p,
q,
a,
b,
c]
and A2:
for
p,
q being
Element of
HP-WFF for
a,
b being
set ex
d being
set st
P2[
p,
q,
a,
b,
d]
and A3:
for
p,
q being
Element of
HP-WFF for
a,
b,
c,
d being
set st
P1[
p,
q,
a,
b,
c] &
P1[
p,
q,
a,
b,
d] holds
c = d
and A4:
for
p,
q being
Element of
HP-WFF for
a,
b,
c,
d being
set st
P2[
p,
q,
a,
b,
c] &
P2[
p,
q,
a,
b,
d] holds
c = d
definition
existence
ex b1 being ManySortedSet of HP-WFF st
( b1 . VERUM = root-tree VERUM & ( for n being Element of NAT holds b1 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = b1 . p & q9 = b1 . q & b1 . (p '&' q) = (p '&' q) -tree (p9,q9) & b1 . (p => q) = (p => q) -tree (p9,q9) ) ) )
uniqueness
for b1, b2 being ManySortedSet of HP-WFF st b1 . VERUM = root-tree VERUM & ( for n being Element of NAT holds b1 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = b1 . p & q9 = b1 . q & b1 . (p '&' q) = (p '&' q) -tree (p9,q9) & b1 . (p => q) = (p => q) -tree (p9,q9) ) ) & b2 . VERUM = root-tree VERUM & ( for n being Element of NAT holds b2 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = b2 . p & q9 = b2 . q & b2 . (p '&' q) = (p '&' q) -tree (p9,q9) & b2 . (p => q) = (p => q) -tree (p9,q9) ) ) holds
b1 = b2
end;