:: HILBERT2 semantic presentation

REAL is set

bool REAL is non empty set

bool NAT is non empty set
bool NAT is non empty set

{{},1} is non empty set
Trees is non empty constituted-Trees set
bool Trees is non empty set

bool HP-WFF is non empty set

Seg 1 is non empty V33() V40(1) Element of bool NAT

tree {} is non empty V33() Tree-like set

len {} is V38() set
p is set
union p is set

Union q is set

dom x is set
rng q is set
union (rng q) is set
f is set
x . f is set
[f,(x . f)] is set
{f,(x . f)} is non empty set
{f} is non empty set
{{f,(x . f)},{f}} is non empty set
r is set
dom q is set
s is set
q . s is set

dom s is set
r is set
q . r is set

dom s is set
s . f is set
[f,(s . f)] is set
{f,(s . f)} is non empty set
{f} is non empty set
{{f,(s . f)},{f}} is non empty set
dom q is set
p is set

q is set

(<*q*> ^ f) . 1 is set
p is set

q is set
rng <*p*> is non empty set
{p} is non empty set
p is set

f is set

p is set

q is non empty Tree-like set
x is non empty Tree-like set
tree (q,x) is non empty Tree-like set

tree <*q,x*> is non empty Tree-like set

<*q,x*> . (f + 1) is set

<*p*> . 1 is set

<*q,x*> . (f + 1) is set

F1() is non empty Tree-like set

q is set

p is set

(p -tree (q,x)) . {} is set

p is set

q . {} is set

(p -tree (q,x)) . is set
(p -tree (q,x)) . <*1*> is set
x . {} is set

dom q is non empty Tree-like set

<*q,x*> . (0 + 1) is set

(p -tree <*q,x*>) . is set

(p -tree <*q,x*>) . () is set
dom x is non empty Tree-like set

<*q,x*> . (1 + 1) is set
(p -tree <*q,x*>) . <*1*> is set

(p -tree <*q,x*>) . (<*1*> ^ r) is set
p is set

<*q,x*> . (0 + 1) is set

<*q,x*> . (1 + 1) is set
p is set

dom (p -tree q) is non empty Tree-like set
dom q is non empty Element of bool NAT

tree (doms x) is non empty Tree-like set
p is set

p is set

{ b1 where b1 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF : P1[b1] } is set
q is set

f is set

() + (len (q ^ x)) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
1 + (len (q ^ x)) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

() + (len (q ^ x)) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
1 + (len (q ^ x)) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

p . 1 is set

1 + (2 + q) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

p . 1 is set

2 + (1 + q) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

q . 1 is set

2 + (1 + p) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

1 + (2 + p) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

p . 1 is set

(len (<*2*> ^ p)) + (len q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(() + (len p)) + (len q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(1 + (len p)) + (len q) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

1 + ((len p) + (len q)) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

(len (<*1*> ^ p)) + (len q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(() + (len p)) + (len q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(1 + (len p)) + (len q) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

1 + ((len p) + (len q)) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

r . 1 is set
s . 1 is set

(<*2*> ^ (s ^ c9)) . 1 is set

<*2*> ^ ((Y9 ^ IMrMs) ^ s) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ (Y9 ^ IMrMs)) ^ s is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ (s ^ c9)) . 1 is set

<*1*> ^ ((Y9 ^ IMrMs) ^ s) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ (Y9 ^ IMrMs)) ^ s is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(p '&' q) . 1 is set

(p '&' q) . 1 is set

(2 + 1) + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

2 + (1 + p) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

(q '&' x) . 1 is set

(p => q) . 1 is set

(1 + 2) + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

1 + (2 + p) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

(q => x) . 1 is set

VERUM . 1 is set
F1() is set
{ (b1) where b1 is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT : verum } is set
{ b1 where b1 is functional Element of bool HP-WFF : ( VERUM in b1 & ( for b2 being V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT holds (b2) in b1 ) & ( for b2, b3 being Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF holds
( ( not b2 '&' b3 in b1 & not b2 => b3 in b1 ) or ( b2 in b1 & b3 in b1 ) ) ) & ex b2 being Relation-like b1 -defined Function-like total set st
( b2 . VERUM = F1() & ( for b3 being V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT holds b2 . (b3) = F2(b3) ) & ( for b3, b4 being Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF holds
( not b3 '&' b4 in b1 or for b5, b6, b7 being set holds
( not b5 = b2 . b3 or not b6 = b2 . b4 or not b7 = b2 . (b3 '&' b4) or P1[b3,b4,b5,b6,b7] ) ) ) & ( for b3, b4 being Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF holds
( not b3 => b4 in b1 or for b5, b6, b7 being set holds
( not b5 = b2 . b3 or not b6 = b2 . b4 or not b7 = b2 . (b3 => b4) or P2[b3,b4,b5,b6,b7] ) ) ) ) )
}
is set

x is set

{ (b1) where b1 is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT : verum } \/ is non empty set

f is set

F2(r) is set

F2(s) is set

F2(r) is set

c9 is set
f . s is set
Y9 is set
f . s is set
IMrMs is set
f . (s '&' s) is set

f . (r) is set
F2(r) is set
r is set
union r is set
s is set

s . VERUM is set
s is set
s is set

Y9 . VERUM is set

Y9 . VERUM is set

rng s is set
c9 is set
dom s is set
Y9 is set
s . Y9 is set

IMrMs . VERUM is set
c9 is functional set

dom Y9 is set
dom IMrMs is set
dom s is set
N is set
s . N is set

N . VERUM is set
N is set
s . N is set

Y9 . (p) is set
IMrMs . (p) is set
F2(p) is set

q . VERUM is set

q . VERUM is set

p . VERUM is set

Y9 . p is set
IMrMs . p is set

Y9 . q is set
IMrMs . q is set

Y9 . (p '&' q) is set
IMrMs . (p '&' q) is set

Y9 . (p => q) is set
IMrMs . (p => q) is set

x . VERUM is set

y . VERUM is set

MZ1 . VERUM is set

x . VERUM is set

y . VERUM is set

MZ1 . VERUM is set
p is set
(dom Y9) /\ (dom IMrMs) is set
Y9 . p is set
IMrMs . p is set
Y9 . VERUM is set
IMrMs . VERUM is set

q . VERUM is set

x . VERUM is set

dom s is set
N is set
s . N is set
dom Y9 is set

N . VERUM is set
N is set
s . N is set
dom IMrMs is set

p . VERUM is set
union c9 is set
Union s is set
IMrMs is set
s . IMrMs is set

N . VERUM is set

dom Y9 is set

IMrMs . N is set

IMrMs . N is set
IMrMs . (N '&' N) is set
p is set
dom s is set
s . p is set
q is set
x is set
y is set

z . VERUM is set
dom z is set
z . (N '&' N) is set
MZ1 is functional Element of bool HP-WFF

c20 . VERUM is set
z . N is set
MZ1 is functional Element of bool HP-WFF

c20 . VERUM is set
z . N is set
dom s is set
s . s is set

N . VERUM is set
N is set

q is Relation-like p</