:: CQC_SIM1 semantic presentation

REAL is V56() V57() V58() V62() V74() V75() V77() set
NAT is non empty non trivial V35() V36() V37() V56() V57() V58() V59() V60() V61() V62() non finite V72() V74() V78() V79() Element of bool REAL

RAT is V56() V57() V58() V59() V62() set

COMPLEX is V56() V62() set
INT is V56() V57() V58() V59() V60() V62() set
NAT is non empty non trivial V35() V36() V37() V56() V57() V58() V59() V60() V61() V62() non finite V72() V74() V78() V79() set

1 is non empty ext-real positive non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V72() V73() V74() V75() V76() V78() Element of NAT
2 is non empty ext-real positive non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V72() V73() V74() V75() V76() V78() Element of NAT
3 is non empty ext-real positive non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V72() V73() V74() V75() V76() V78() Element of NAT
A is non empty Relation-like QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool ()

QC-symbols A is non empty set

q is Element of QC-symbols A

4 is non empty ext-real positive non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V72() V73() V74() V75() V76() V78() Element of NAT
[4,q] is V18() set
{4,q} is non empty finite set
{4} is non empty trivial V56() V57() V58() V59() V60() V61() finite V67() V72() V73() V74() V75() V76() V80(1) set
{{4,q},{4}} is non empty finite V67() set
r is Element of QC-symbols A

[4,r] is V18() set
{4,r} is non empty finite set
{{4,r},{4}} is non empty finite V67() set
A is set
p is set

{A} is non empty trivial finite V80(1) set

{p} is non empty trivial finite V80(1) set
[:{A},{p}:] is non empty Relation-like finite set

q +* (A .--> p) is Relation-like Function-like set
Im ((q +* (A .--> p)),A) is set
(q +* (A .--> p)) .: {A} is finite set
r is set
proj1 (q +* (A .--> p)) is set
f is set
(q +* (A .--> p)) . f is set
proj1 (A .--> p) is finite set
(A .--> p) . f is set
proj1 (A .--> p) is finite set
proj1 (q +* (A .--> p)) is set
(A .--> p) . A is set
(q +* (A .--> p)) . A is set
p is set
A is set
r is set

{r} is non empty trivial finite V80(1) set

f +* (p --> r) is Relation-like Function-like set
(f +* (p --> r)) .: A is set
f .: A is set
(f .: A) \/ {r} is non empty set
h is set
proj1 (f +* (p --> r)) is set
u is set
(f +* (p --> r)) . u is set
proj1 (p --> r) is set
(p --> r) . u is set
f . u is set
proj1 f is set
A is set
p is set

{A} is non empty trivial finite V80(1) set

{p} is non empty trivial finite V80(1) set
[:{A},{p}:] is non empty Relation-like finite set

q +* (A .--> p) is Relation-like Function-like set
r is set
r \ {A} is Element of bool r

(q +* (A .--> p)) .: (r \ {A}) is set
q .: (r \ {A}) is set
f is set
proj1 (A .--> p) is finite set
proj1 (q +* (A .--> p)) is set
h is set
(q +* (A .--> p)) . h is set
proj1 q is set
q . h is set
f is set
proj1 q is set
h is set
q . h is set
proj1 (A .--> p) is finite set
(q +* (A .--> p)) . h is set
proj1 (q +* (A .--> p)) is set
p is set
A is set
{A} is non empty trivial finite V80(1) set

{p} is non empty trivial finite V80(1) set
[:{A},{p}:] is non empty Relation-like finite set

q +* (A .--> p) is Relation-like Function-like set
r is set
r \ {A} is Element of bool r

q .: (r \ {A}) is set
(q +* (A .--> p)) .: (r \ {A}) is set
(q +* (A .--> p)) .: r is set
((q +* (A .--> p)) .: r) \ {p} is Element of bool ((q +* (A .--> p)) .: r)
bool ((q +* (A .--> p)) .: r) is non empty cup-closed diff-closed preBoolean set
f is set
proj1 (A .--> p) is finite set
proj1 (q +* (A .--> p)) is set
h is set
(q +* (A .--> p)) . h is set
proj1 q is set
q . h is set
f is set
proj1 (q +* (A .--> p)) is set
h is set
(q +* (A .--> p)) . h is set
proj1 (A .--> p) is finite set
(A .--> p) . h is set
A is non empty Relation-like QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of bool ()

QC-pred_symbols A is non empty set
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set

p is Element of CQC-WFF A
q is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
q -ary_QC-pred_symbols A is non empty Element of bool ()

r is Element of q -ary_QC-pred_symbols A

r ! f is Element of QC-WFF A
len f is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
fixed_QC-variables A is non empty Element of bool ()
{ (f . b1) where b1 is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT : ( 1 <= b1 & b1 <= len f & f . b1 in fixed_QC-variables A ) } is set
free_QC-variables A is non empty Element of bool ()
{ (f . b1) where b1 is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT : ( 1 <= b1 & b1 <= len f & f . b1 in free_QC-variables A ) } is set
A is non empty Relation-like QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of bool ()

p is Element of CQC-WFF A
q is Element of QC-WFF A
'not' q is Element of QC-WFF A
A is non empty Relation-like QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of bool ()

p is Element of CQC-WFF A
q is Element of QC-WFF A
r is Element of QC-WFF A
q '&' r is Element of QC-WFF A
A is non empty Relation-like QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of bool ()

QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool ()

p is Element of CQC-WFF A

r is Element of QC-WFF A
All (q,r) is Element of QC-WFF A

len A is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
{ (A . b1) where b1 is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT : ( 1 <= b1 & b1 <= len A ) } is set
p is set
dom A is V56() V57() V58() V59() V60() V61() finite V74() V75() V76() Element of bool NAT
q is set
A . q is set
r is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
p is set
q is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
A . q is set
dom A is V56() V57() V58() V59() V60() V61() finite V74() V75() V76() Element of bool NAT
F2() is non empty set
F1() is non empty Relation-like QC-alphabet
QC-WFF F1() is non empty set
[:(QC-WFF F1()),F2():] is non empty Relation-like set
bool [:(QC-WFF F1()),F2():] is non empty cup-closed diff-closed preBoolean set
VERUM F1() is Element of CQC-WFF F1()
CQC-WFF F1() is non empty Element of bool (QC-WFF F1())
bool (QC-WFF F1()) is non empty cup-closed diff-closed preBoolean set
F3() is Element of F2()
A is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
A + 1 is non empty ext-real positive non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V72() V73() V74() V75() V76() V78() Element of NAT
p is non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():]
q is Element of QC-WFF F1()

QC-symbols F1() is non empty set
[:NAT,(QC-symbols F1()):] is non empty non trivial Relation-like non finite set
len (@ q) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
p . q is Element of F2()
F4(q) is Element of F2()
the_argument_of q is Element of QC-WFF F1()
p . () is Element of F2()
F5((p . ()),q) is Element of F2()
the_left_argument_of q is Element of QC-WFF F1()
p . is Element of F2()
the_right_argument_of q is Element of QC-WFF F1()
p . is Element of F2()
F6((),(),q) is Element of F2()
the_scope_of q is Element of QC-WFF F1()
p . () is Element of F2()
F7((p . ()),q) is Element of F2()
r is Element of F2()
r is Element of F2()
r is Element of F2()
r is Element of F2()
r is Element of F2()
r is Element of F2()
r is Element of F2()
f is Element of F2()
h is Element of F2()
u is Element of F2()
K is Element of F2()
f is Element of F2()
q is non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():]
r is non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():]
f is Element of QC-WFF F1()

QC-symbols F1() is non empty set
[:NAT,(QC-symbols F1()):] is non empty non trivial Relation-like non finite set
len (@ f) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
r . f is Element of F2()
F4(f) is Element of F2()
the_argument_of f is Element of QC-WFF F1()
r . () is Element of F2()
F5((r . ()),f) is Element of F2()
the_left_argument_of f is Element of QC-WFF F1()
r . is Element of F2()
the_right_argument_of f is Element of QC-WFF F1()
r . is Element of F2()
F6((),(),f) is Element of F2()
the_scope_of f is Element of QC-WFF F1()
r . () is Element of F2()
F7((r . ()),f) is Element of F2()
p . f is Element of F2()
p . f is Element of F2()

len (@ ()) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
p . () is Element of F2()
p . f is Element of F2()

len () is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
p . is Element of F2()

len () is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
p . is Element of F2()
p . f is Element of F2()

len (@ ()) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
p . () is Element of F2()
p . f is Element of F2()

the non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():] is non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():]
p is Element of QC-WFF F1()

QC-symbols F1() is non empty set
[:NAT,(QC-symbols F1()):] is non empty non trivial Relation-like non finite set
len (@ p) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
the non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():] . p is Element of F2()
F4(p) is Element of F2()
the_argument_of p is Element of QC-WFF F1()
the non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():] . () is Element of F2()
F5(( the non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():] . ()),p) is Element of F2()
the_left_argument_of p is Element of QC-WFF F1()
the non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():] . is Element of F2()
the_right_argument_of p is Element of QC-WFF F1()
the non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():] . is Element of F2()
F6(( the non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():] . ),( the non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():] . ),p) is Element of F2()
the_scope_of p is Element of QC-WFF F1()
the non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():] . () is Element of F2()
F7(( the non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():] . ()),p) is Element of F2()
A is set
p is Element of QC-WFF F1()

QC-symbols F1() is non empty set
[:NAT,(QC-symbols F1()):] is non empty non trivial Relation-like non finite set
len (@ p) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
q is non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():]
q . A is set
r is non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():]
r . p is Element of F2()
f is Element of QC-WFF F1()

len (@ f) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
q . f is Element of F2()
r . f is Element of F2()
F4(f) is Element of F2()

len (@ (VERUM F1())) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
q . (VERUM F1()) is Element of F2()
r . (VERUM F1()) is Element of F2()
the_argument_of f is Element of QC-WFF F1()

len (@ ()) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
q . () is Element of F2()
r . () is Element of F2()
F5((r . ()),f) is Element of F2()
the_left_argument_of f is Element of QC-WFF F1()

len () is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
q . is Element of F2()
r . is Element of F2()
the_right_argument_of f is Element of QC-WFF F1()

len () is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
q . is Element of F2()
r . is Element of F2()
F6((),(),f) is Element of F2()
the_scope_of f is Element of QC-WFF F1()

len (@ ()) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
q . () is Element of F2()
r . () is Element of F2()
F7((r . ()),f) is Element of F2()

proj1 A is set
proj2 A is set
p is set
q is set
A . q is set
r is Element of QC-WFF F1()

QC-symbols F1() is non empty set
[:NAT,(QC-symbols F1()):] is non empty non trivial Relation-like non finite set
len (@ r) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
f is non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():]
f . r is Element of F2()
p is non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():]
p . (VERUM F1()) is Element of F2()
q is Element of QC-WFF F1()

QC-symbols F1() is non empty set
[:NAT,(QC-symbols F1()):] is non empty non trivial Relation-like non finite set
len (@ q) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
r is non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():]
r . (VERUM F1()) is Element of F2()
f is Element of QC-WFF F1()
p . f is Element of F2()
F4(f) is Element of F2()
the_argument_of f is Element of QC-WFF F1()
p . () is Element of F2()
F5((p . ()),f) is Element of F2()
the_left_argument_of f is Element of QC-WFF F1()
p . is Element of F2()
the_right_argument_of f is Element of QC-WFF F1()
p . is Element of F2()
F6((),(),f) is Element of F2()
the_scope_of f is Element of QC-WFF F1()
p . () is Element of F2()
F7((p . ()),f) is Element of F2()
h is Element of QC-WFF F1()

len (@ h) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
u is non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():]
u . f is Element of F2()

len (@ f) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
f is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
r9 is Element of QC-WFF F1()

len (@ r9) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
u . r9 is Element of F2()
F4(r9) is Element of F2()
the_argument_of r9 is Element of QC-WFF F1()
u . () is Element of F2()
F5((u . ()),r9) is Element of F2()
the_left_argument_of r9 is Element of QC-WFF F1()
u . () is Element of F2()
the_right_argument_of r9 is Element of QC-WFF F1()
u . is Element of F2()
F6((u . ()),(u . ),r9) is Element of F2()
the_scope_of r9 is Element of QC-WFF F1()
u . () is Element of F2()
F7((u . ()),r9) is Element of F2()

len (@ ()) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
s9 is Element of QC-WFF F1()

len (@ s9) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
u . s9 is Element of F2()
F4(s9) is Element of F2()
the_argument_of s9 is Element of QC-WFF F1()
u . () is Element of F2()
F5((u . ()),s9) is Element of F2()
the_left_argument_of s9 is Element of QC-WFF F1()
u . () is Element of F2()
the_right_argument_of s9 is Element of QC-WFF F1()
u . is Element of F2()
F6((u . ()),(u . ),s9) is Element of F2()
the_scope_of s9 is Element of QC-WFF F1()
u . () is Element of F2()
F7((u . ()),s9) is Element of F2()
u . () is Element of F2()
s9 is Element of QC-WFF F1()

len (@ s9) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT

len () is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT

len () is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
u is Element of QC-WFF F1()

len (@ u) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
u . u is Element of F2()
F4(u) is Element of F2()
the_argument_of u is Element of QC-WFF F1()
u . () is Element of F2()
F5((u . ()),u) is Element of F2()
the_left_argument_of u is Element of QC-WFF F1()
u . is Element of F2()
the_right_argument_of u is Element of QC-WFF F1()
u . is Element of F2()
F6((),(),u) is Element of F2()
the_scope_of u is Element of QC-WFF F1()
u . () is Element of F2()
F7((u . ()),u) is Element of F2()
u is Element of QC-WFF F1()

len (@ u) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
u . u is Element of F2()
F4(u) is Element of F2()
the_argument_of u is Element of QC-WFF F1()
u . () is Element of F2()
F5((u . ()),u) is Element of F2()
the_left_argument_of u is Element of QC-WFF F1()
u . is Element of F2()
the_right_argument_of u is Element of QC-WFF F1()
u . is Element of F2()
F6((),(),u) is Element of F2()
the_scope_of u is Element of QC-WFF F1()
u . () is Element of F2()
F7((u . ()),u) is Element of F2()
u . is Element of F2()
u is Element of QC-WFF F1()

len (@ u) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
u . is Element of F2()
u is Element of QC-WFF F1()

len (@ u) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT

len (@ ()) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
r9 is Element of QC-WFF F1()

len (@ r9) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
u . r9 is Element of F2()
F4(r9) is Element of F2()
the_argument_of r9 is Element of QC-WFF F1()
u . () is Element of F2()
F5((u . ()),r9) is Element of F2()
the_left_argument_of r9 is Element of QC-WFF F1()
u . () is Element of F2()
the_right_argument_of r9 is Element of QC-WFF F1()
u . is Element of F2()
F6((u . ()),(u . ),r9) is Element of F2()
the_scope_of r9 is Element of QC-WFF F1()
u . () is Element of F2()
F7((u . ()),r9) is Element of F2()
u . () is Element of F2()
r9 is Element of QC-WFF F1()

len (@ r9) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
F2() is non empty set
F3() is non empty set
Funcs (F2(),F3()) is non empty functional FUNCTION_DOMAIN of F2(),F3()
F1() is non empty Relation-like QC-alphabet
CQC-WFF F1() is non empty Element of bool (QC-WFF F1())
QC-WFF F1() is non empty set
bool (QC-WFF F1()) is non empty cup-closed diff-closed preBoolean set
[:(CQC-WFF F1()),(Funcs (F2(),F3())):] is non empty Relation-like set
bool [:(CQC-WFF F1()),(Funcs (F2(),F3())):] is non empty cup-closed diff-closed preBoolean set
VERUM F1() is Element of CQC-WFF F1()
F4() is Relation-like F2() -defined F3() -valued Function-like total quasi_total Element of Funcs (F2(),F3())
bound_QC-variables F1() is non empty Element of bool (QC-variables F1())
QC-variables F1() is non empty set
bool (QC-variables F1()) is non empty cup-closed diff-closed preBoolean set
QC-pred_symbols F1() is non empty set
[:(QC-WFF F1()),(Funcs (F2(),F3())):] is non empty Relation-like set
bool [:(QC-WFF F1()),(Funcs (F2(),F3())):] is non empty cup-closed diff-closed preBoolean set
A is non empty Relation-like QC-WFF F1() -defined Funcs (F2(),F3()) -valued Function-like total quasi_total Function-yielding V93() Element of bool [:(QC-WFF F1()),(Funcs (F2(),F3())):]
A . (VERUM F1()) is Relation-like Function-like Element of Funcs (F2(),F3())
A | (CQC-WFF F1()) is Relation-like CQC-WFF F1() -defined QC-WFF F1() -defined Funcs (F2(),F3()) -valued Function-like Function-yielding V93() Element of bool [:(QC-WFF F1()),(Funcs (F2(),F3())):]
p is non empty Relation-like CQC-WFF F1() -defined Funcs (F2(),F3()) -valued Function-like total quasi_total Function-yielding V93() Element of bool [:(CQC-WFF F1()),(Funcs (F2(),F3())):]
p . (VERUM F1()) is Relation-like Function-like Element of Funcs (F2(),F3())
q is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
q -ary_QC-pred_symbols F1() is non empty Element of bool (QC-pred_symbols F1())
bool (QC-pred_symbols F1()) is non empty cup-closed diff-closed preBoolean set

f is Element of q -ary_QC-pred_symbols F1()
f ! r is Element of CQC-WFF F1()
p . (f ! r) is Relation-like Function-like Element of Funcs (F2(),F3())
F5(q,f,r) is Relation-like F2() -defined F3() -valued Function-like total quasi_total Element of Funcs (F2(),F3())
the_arity_of f is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT

the_pred_symbol_of (f ! r) is Element of QC-pred_symbols F1()
A . (f ! r) is Relation-like Function-like Element of Funcs (F2(),F3())
q is Element of CQC-WFF F1()
'not' q is Element of CQC-WFF F1()
p . () is Relation-like Function-like Element of Funcs (F2(),F3())
p . q is Relation-like Function-like Element of Funcs (F2(),F3())
F6((p . q),q) is Relation-like F2() -defined F3() -valued Function-like total quasi_total Element of Funcs (F2(),F3())
r is Element of CQC-WFF F1()
q '&' r is Element of CQC-WFF F1()
p . (q '&' r) is Relation-like Function-like Element of Funcs (F2(),F3())
p . r is Relation-like Function-like Element of Funcs (F2(),F3())
F7((p . q),(p . r),q,r) is Relation-like F2() -defined F3() -valued Function-like total quasi_total Element of Funcs (F2(),F3())
f is Element of bound_QC-variables F1()
All (f,q) is Element of CQC-WFF F1()
p . (All (f,q)) is Relation-like Function-like Element of Funcs (F2(),F3())
F8(f,(p . q),q) is Relation-like F2() -defined F3() -valued Function-like total quasi_total Element of Funcs (F2(),F3())
A . q is Relation-like Function-like Element of Funcs (F2(),F3())
the_argument_of () is Element of QC-WFF F1()
A . () is Relation-like Function-like Element of Funcs (F2(),F3())
A . r is Relation-like Function-like Element of Funcs (F2(),F3())
the_left_argument_of (q '&' r) is Element of QC-WFF F1()
the_right_argument_of (q '&' r) is Element of QC-WFF F1()
A . (q '&' r) is Relation-like Function-like Element of Funcs (F2(),F3())
bound_in (All (f,q)) is Element of bound_QC-variables F1()
the_scope_of (All (f,q)) is Element of QC-WFF F1()
A . (All (f,q)) is Relation-like Function-like Element of Funcs (F2(),F3())
F1() is non empty Relation-like QC-alphabet
CQC-WFF F1() is non empty Element of bool (QC-WFF F1())
QC-WFF F1() is non empty set
bool (QC-WFF F1()) is non empty cup-closed diff-closed preBoolean set
F2() is non empty set
F3() is non empty set
Funcs (F2(),F3()) is non empty functional FUNCTION_DOMAIN of F2(),F3()
[:(CQC-WFF F1()),(Funcs (F2(),F3())):] is non empty Relation-like set
bool [:(CQC-WFF F1()),(Funcs (F2(),F3())):] is non empty cup-closed diff-closed preBoolean set
[:F2(),F3():] is non empty Relation-like set
bool [:F2(),F3():] is non empty cup-closed diff-closed preBoolean set
F4() is non empty Relation-like CQC-WFF F1() -defined Funcs (F2(),F3()) -valued Function-like total quasi_total Function-yielding V93() Element of bool [:(CQC-WFF F1()),(Funcs (F2(),F3())):]
VERUM F1() is Element of CQC-WFF F1()
F4() . (VERUM F1()) is Relation-like Function-like Element of Funcs (F2(),F3())
F6() is non empty Relation-like F2() -defined F3() -valued Function-like total quasi_total Element of bool [:F2(),F3():]
bound_QC-variables F1() is non empty Element of bool (QC-variables F1())
QC-variables F1() is non empty set
bool (QC-variables F1()) is non empty cup-closed diff-closed preBoolean set
QC-pred_symbols F1() is non empty set
F5() is non empty Relation-like CQC-WFF F1() -defined Funcs (F2(),F3()) -valued Function-like total quasi_total Function-yielding V93() Element of bool [:(CQC-WFF F1()),(Funcs (F2(),F3())):]
F5() . (VERUM F1()) is Relation-like Function-like Element of Funcs (F2(),F3())
F4() . (VERUM F1()) is Relation-like Function-like set
F5() . (VERUM F1()) is Relation-like Function-like set
A is Element of CQC-WFF F1()

'not' A is Element of CQC-WFF F1()
F4() . () is Relation-like Function-like set
F5() . () is Relation-like Function-like set
p is Element of CQC-WFF F1()

A '&' p is Element of CQC-WFF F1()
F4() . (A '&' p) is Relation-like Function-like set
F5() . (A '&' p) is Relation-like Function-like set
q is Element of bound_QC-variables F1()
All (q,A) is Element of CQC-WFF F1()
F4() . (All (q,A)) is Relation-like Function-like set
F5() . (All (q,A)) is Relation-like Function-like set
r is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
r -ary_QC-pred_symbols F1() is non empty Element of bool (QC-pred_symbols F1())
bool (QC-pred_symbols F1()) is non empty cup-closed diff-closed preBoolean set

h is Element of r -ary_QC-pred_symbols F1()
h ! f is Element of CQC-WFF F1()
F4() . (h ! f) is Relation-like Function-like set
F5() . (h ! f) is Relation-like Function-like set
F4() . (h ! f) is Relation-like Function-like Element of Funcs (F2(),F3())
F7(r,h,f) is non empty Relation-like F2() -defined F3() -valued Function-like total quasi_total Element of bool [:F2(),F3():]
F5() . (h ! f) is Relation-like Function-like Element of Funcs (F2(),F3())
F4() . () is Relation-like Function-like Element of Funcs (F2(),F3())
F4() . A is Relation-like Function-like Element of Funcs (F2(),F3())
F8((F4() . A),A) is non empty Relation-like F2() -defined F3() -valued Function-like total quasi_total Element of bool [:F2(),F3():]
F5() . A is Relation-like Function-like Element of Funcs (F2(),F3())
F5() . () is Relation-like Function-like Element of Funcs (F2(),F3())
F4() . (A '&' p) is Relation-like Function-like Element of Funcs (F2(),F3())
F4() . p is Relation-like Function-like Element of Funcs (F2(),F3())
F9((F4() . A),(F4() . p),A,p) is non empty Relation-like F2() -defined F3() -valued Function-like total quasi_total Element of bool [:F2(),F3():]
F5() . p is Relation-like Function-like Element of Funcs (F2(),F3())
F5() . (A '&' p) is Relation-like Function-like Element of Funcs (F2(),F3())
F4() . (All (q,A)) is Relation-like Function-like Element of Funcs (F2(),F3())
F10(q,(F4() . A),A) is non empty Relation-like F2() -defined F3() -valued Function-like total quasi_total Element of bool [:F2(),F3():]
A is non empty Relation-like QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of bool ()

p is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
A is non empty Relation-like QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of bool ()

p is Element of CQC-WFF A
q is Element of CQC-WFF A
p '&' q is Element of CQC-WFF A
A is non empty Relation-like QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of bool ()

QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool ()

p is Element of CQC-WFF A

All (q,p) is Element of CQC-WFF A
A is non empty Relation-like QC-alphabet
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set

p is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT

len q is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
r is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
q . r is set
dom q is V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V80(p) Element of bool NAT

p is non empty set
A is non empty Relation-like QC-alphabet
CQC-WFF A is non empty Element of bool ()
QC-WFF A is non empty set

[:p,():] is non empty Relation-like set
bool [:p,():] is non empty cup-closed diff-closed preBoolean set
Funcs (p,()) is non empty functional FUNCTION_DOMAIN of p, CQC-WFF A

r is Element of p
q . r is set
q . r is Element of CQC-WFF A
f is Element of CQC-WFF A
'not' f is Element of CQC-WFF A
h is Element of CQC-WFF A
'not' h is Element of CQC-WFF A

h is Element of p
r . h is Element of CQC-WFF A
f . h is Element of CQC-WFF A
q . h is Element of CQC-WFF A
u is Element of CQC-WFF A
'not' u is Element of CQC-WFF A
A is non empty Relation-like QC-alphabet
QC-symbols A is non empty set
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set

[:(),(Funcs (,)):] is non empty Relation-like set
CQC-WFF A is non empty Element of bool ()
QC-WFF A is non empty set

[:[:(),(Funcs (,)):],():] is non empty Relation-like set
bool [:[:(),(Funcs (,)):],():] is non empty cup-closed diff-closed preBoolean set
Funcs ([:(),(Funcs (,)):],()) is non empty functional FUNCTION_DOMAIN of [:(),(Funcs (,)):], CQC-WFF A
p is non empty Relation-like [:(),(Funcs (,)):] -defined CQC-WFF A -valued Function-like total quasi_total Element of bool [:[:(),(Funcs (,)):],():]
q is non empty Relation-like [:(),(Funcs (,)):] -defined CQC-WFF A -valued Function-like total quasi_total Element of bool [:[:(),(Funcs (,)):],():]
r is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
f is Element of QC-symbols A
f + r is Element of QC-symbols A

[f,h] is V18() set
{f,h} is non empty finite set
{f} is non empty trivial finite V80(1) set
{{f,h},{f}} is non empty finite V67() set
p . [f,h] is set
[(f + r),h] is V18() set
{(f + r),h} is non empty finite set
{(f + r)} is non empty trivial finite V80(1) set
{{(f + r),h},{(f + r)}} is non empty finite V67() set
q . [(f + r),h] is set
[f,h] is V18() Element of [:(),(Funcs (,)):]
p . [f,h] is Element of CQC-WFF A
[(f + r),h] is V18() Element of [:(),(Funcs (,)):]
q . [(f + r),h] is Element of CQC-WFF A
u is Element of CQC-WFF A
K is Element of CQC-WFF A
u '&' K is Element of CQC-WFF A
f is Element of CQC-WFF A
r9 is Element of CQC-WFF A
f '&' r9 is Element of CQC-WFF A
f is non empty Relation-like [:(),(Funcs (,)):] -defined CQC-WFF A -valued Function-like total quasi_total Element of bool [:[:(),(Funcs (,)):],():]
h is Relation-like [:(),(Funcs (,)):] -defined CQC-WFF A -valued Function-like total quasi_total Element of Funcs ([:(),(Funcs (,)):],())
u is Element of QC-symbols A
u + r is Element of QC-symbols A

p . (u,K) is Element of CQC-WFF A
[u,K] is V18() set
{u,K} is non empty finite set
{u} is non empty trivial finite V80(1) set
{{u,K},{u}} is non empty finite V67() set
p . [u,K] is set
q . ((u + r),K) is Element of CQC-WFF A
[(u + r),K] is V18() set
{(u + r),K} is non empty finite set
{(u + r)} is non empty trivial finite V80(1) set
{{(u + r),K},{(u + r)}} is non empty finite V67() set
q . [(u + r),K] is set
h . (u,K) is Element of CQC-WFF A
h . [u,K] is set
f is Element of CQC-WFF A
r9 is Element of CQC-WFF A
f '&' r9 is Element of CQC-WFF A
f is Relation-like [:(),(Funcs (,)):] -defined CQC-WFF A -valued Function-like total quasi_total Element of Funcs ([:(),(Funcs (,)):],())
h is Relation-like [:(),(Funcs (,)):] -defined CQC-WFF A -valued Function-like total quasi_total Element of Funcs ([:(),(Funcs (,)):],())
u is Element of [:(),(Funcs (,)):]
f . u is Element of CQC-WFF A
h . u is Element of CQC-WFF A
K is Element of QC-symbols A

[K,f] is V18() Element of [:(),(Funcs (,)):]
{K,f} is non empty finite set
{K} is non empty trivial finite V80(1) set
{{K,f},{K}} is non empty finite V67() set
K + r is Element of QC-symbols A
q . ((K + r),f) is Element of CQC-WFF A
[(K + r),f] is V18() set
{(K + r),f} is non empty finite set
{(K + r)} is non empty trivial finite V80(1) set
{{(K + r),f},{(K + r)}} is non empty finite V67() set
q . [(K + r),f] is set
p . (K,f) is Element of CQC-WFF A
[K,f] is V18() set
p . [K,f] is set
f . (K,f) is Element of CQC-WFF A
f . [K,f] is set
s9 is Element of CQC-WFF A
r9 is Element of CQC-WFF A
s9 '&' r9 is Element of CQC-WFF A
h . (K,f) is Element of CQC-WFF A
h . [K,f] is set
A is non empty Relation-like QC-alphabet
QC-symbols A is non empty set
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool ()

is non empty Relation-like set

p is Element of QC-symbols A

4 is non empty ext-real positive non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V72() V73() V74() V75() V76() V78() Element of NAT
[4,p] is V18() set
{4,p} is non empty finite set
{4} is non empty trivial V56() V57() V58() V59() V60() V61() finite V67() V72() V73() V74() V75() V76() V80(1) set
{{4,p},{4}} is non empty finite V67() set

{q} is non empty trivial finite V80(1) set

{(x. p)} is non empty trivial finite V80(1) set
[:{q},{(x. p)}:] is non empty Relation-like finite set
bool [:{q},{(x. p)}:] is non empty cup-closed diff-closed preBoolean finite V67() set

r +* (q .--> (x. p)) is Relation-like Function-like set
proj2 (r +* (q .--> (x. p))) is set
proj2 r is set
proj2 (q .--> (x. p)) is finite set
() \/ (proj2 (q .--> (x. p))) is set
proj1 (r +* (q .--> (x. p))) is set
proj1 r is set
{q} is non empty trivial finite V80(1) Element of bool

[:{q},:] is non empty Relation-like set

[:{q},{(x. p)}:] is non empty Relation-like finite set
proj1 ({q} --> (x. p)) is non empty finite set
() \/ (proj1 ({q} --> (x. p))) is non empty set
() \/ {q} is non empty set
\/ {q} is non empty set
A is non empty Relation-like QC-alphabet
QC-symbols A is non empty set
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set

[:(),(Funcs (,)):] is non empty Relation-like set
CQC-WFF A is non empty Element of bool ()
QC-WFF A is non empty set

[:[:(),(Funcs (,)):],():] is non empty Relation-like set
bool [:[:(),(Funcs (,)):],():] is non empty cup-closed diff-closed preBoolean set
Funcs ([:(),(Funcs (,)):],()) is non empty functional FUNCTION_DOMAIN of [:(),(Funcs (,)):], CQC-WFF A
p is non empty Relation-like [:(),(Funcs (,)):] -defined CQC-WFF A -valued Function-like total quasi_total Element of bool [:[:(),(Funcs (,)):],():]

{q} is non empty trivial finite V80(1) Element of bool

r is Element of QC-symbols A
r ++ is Element of QC-symbols A

4 is non empty ext-real positive non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V72() V73() V74() V75() V76() V78() Element of NAT
[4,r] is V18() set
{4,r} is non empty finite set
{4} is non empty trivial V56() V57() V58() V59() V60() V61() finite V67() V72() V73() V74() V75() V76() V80(1) set
{{4,r},{4}} is non empty finite V67() set

[:{q},:] is non empty Relation-like set

{(x. r)} is non empty trivial finite V80(1) set
[:{q},{(x. r)}:] is non empty Relation-like finite set

f +* ({q} --> (x. r)) is Relation-like Function-like set
[(r ++),(f +* ({q} --> (x. r)))] is V18() set
{(r ++),(f +* ({q} --> (x. r)))} is non empty finite set
{(r ++)} is non empty trivial finite V80(1) set
{{(r ++),(f +* ({q} --> (x. r)))},{(r ++)}} is non empty finite V67() set
p . [(r ++),(f +* ({q} --> (x. r)))] is set
is non empty Relation-like set

{q} is non empty trivial finite V80(1) set

[:{q},{(x. r)}:] is non empty Relation-like finite set
bool [:{q},{(x. r)}:] is non empty cup-closed diff-closed preBoolean finite V67() set
f +* (q .--> (x. r)) is Relation-like Function-like set

[(r ++),u] is V18() Element of [:(),(Funcs (,)):]
{(r ++),u} is non empty finite set
{{(r ++),u},{(r ++)}} is non empty finite V67() set
p . [(r ++),u] is Element of CQC-WFF A
K is Element of CQC-WFF A
All ((x. r),K) is Element of CQC-WFF A
f is Element of CQC-WFF A
All ((x. r),f) is Element of CQC-WFF A
r is non empty Relation-like [:(),(Funcs (,)):] -defined CQC-WFF A -valued Function-like total quasi_total Element of bool [:[:(),(Funcs (,)):],():]
f is Relation-like [:(),(Funcs (,)):] -defined CQC-WFF A -valued Function-like total quasi_total Element of Funcs ([:(),(Funcs (,)):],())
h is Element of QC-symbols A
h ++ is Element of QC-symbols A

4 is non empty ext-real positive non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V72() V73() V74() V75() V76() V78() Element of NAT
[4,h] is V18() set
{4,h} is non empty finite set
{4} is non empty trivial V56() V57() V58() V59() V60() V61() finite V67() V72() V73() V74() V75() V76() V80(1) set
{{4,h},{4}} is non empty finite V67() set

{q} is non empty trivial finite V80(1) set

{(x. h)} is non empty trivial finite V80(1) set
[:{q},{(x. h)}:] is non empty Relation-like finite set
bool [:{q},{(x. h)}:] is non empty cup-closed diff-closed preBoolean finite V67() set

u +* (q .--> (x. h)) is Relation-like Function-like set
p . ((h ++),(u +* (q .--> (x. h)))) is set
[(h ++),(u +* (q .--> (x. h)))] is V18() set
{(h ++),(u +* (q .--> (x. h)))} is non empty finite set
{(h ++)} is non empty trivial finite V80(1) set
{{(h ++),(u +* (q .--> (x. h)))},{(h ++)}} is non empty finite V67() set
p . [(h ++),(u +* (q .--> (x. h)))] is set
f . (h,u) is Element of CQC-WFF A
[h,u] is V18() set
{h,u} is non empty finite set
{h} is non empty trivial finite V80(1) set
{{h,u},{h}} is non empty finite V67() set
f . [h,u] is set
K is Element of CQC-WFF A
All ((x. h),K) is Element of CQC-WFF A
r is Relation-like [:(),(Funcs (,)):] -defined CQC-WFF A -valued Function-like total quasi_total Element of Funcs ([:(),(Funcs (,)):],())
f is Relation-like [:(),(Funcs (,)):] -defined CQC-WFF A -valued Function-like total quasi_total Element of Funcs ([:(),(Funcs (,)):],())
h is Element of [:(),(Funcs (,)):]
r . h is Element of CQC-WFF A
f . h is Element of CQC-WFF A
u is Element of QC-symbols A

[u,K] is V18() Element of [:(),(Funcs (,)):]
{u,K} is non empty finite set
{u} is non empty trivial finite V80(1) set
{{u,K},{u}} is non empty finite V67() set
is non empty Relation-like set

4 is non empty ext-real positive non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V72() V73() V74()