begin
begin
begin
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
begin
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;