environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, TREES_2, ZFMISC_1, FINSEQ_1, XBOOLE_0, TREES_1, FUNCT_1, RELAT_1, ORDINAL4, NAT_1, CARD_1, XXREAL_0, PARTFUN1, TARSKI, ORDINAL1, ARYTM_3, FINSET_1, FUNCOP_1, MARGREL1, MCART_1, QC_LANG1, XBOOLEAN, VALUED_1, ZF_LANG, MODAL_1, TREES_3;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, WELLORD2, XCMPLX_0, NAT_1, DOMAIN_1, MCART_1, RELAT_1, FUNCT_1, RELSET_1, FINSEQ_1, FUNCOP_1, FINSEQ_2, FUNCT_2, FINSET_1, PARTFUN1, TREES_1, TREES_2, XXREAL_0, TREES_3;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, FUNCT_1, NAT_1, ENUMSET1, TREES_1, TREES_2, FUNCOP_1, DOMAIN_1, PARTFUN1, FINSEQ_1, FINSET_1, CARD_1, WELLORD2, CARD_2, ZFMISC_1, FINSEQ_2, RELAT_1, FUNCT_2, RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, TREES_3, XTUPLE_0, ORDINAL1;
schemes TREES_2, CLASSES1, NAT_1, FUNCT_2, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XXREAL_0, XREAL_0, FINSEQ_1, TREES_1, TREES_2, CARD_1, RELSET_1, TREES_3, XTUPLE_0;
constructors HIDDEN, PARTFUN1, WELLORD2, DOMAIN_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_2, TREES_2, RELSET_1, FUNCOP_1, TREES_3, XTUPLE_0, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities ;
expansions TARSKI, XBOOLE_0;
Lm1:
for m being Nat holds {} is_a_proper_prefix_of <*m*>
by XBOOLE_1:2;
Lm2:
for f being Function st dom f is finite holds
f is finite
definition
existence
ex b1 being DTree-set of [:NAT,NAT:] st
( ( for x being DecoratedTree of [:NAT,NAT:] st x in b1 holds
x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds
( x in b1 iff for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Nat st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) )
uniqueness
for b1, b2 being DTree-set of [:NAT,NAT:] st ( for x being DecoratedTree of [:NAT,NAT:] st x in b1 holds
x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds
( x in b1 iff for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Nat st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) & ( for x being DecoratedTree of [:NAT,NAT:] st x in b2 holds
x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds
( x in b2 iff for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Nat st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) holds
b1 = b2
end;
Lm3:
for n, m being Nat holds <*0*> in dom ((elementary_tree 1) --> [n,m])
theorem Th30:
for
A,
A1,
B,
B1 being
MP-wff st
A '&' B = A1 '&' B1 holds
(
A = A1 &
B = B1 )
Lm4:
for A, B being MP-wff holds
( VERUM <> 'not' A & VERUM <> (#) A & VERUM <> A '&' B )
Lm5:
[0,0] is MP-conective
Lm6:
for p being MP-variable holds VERUM <> @ p