:: SUBSTUT2 semantic presentation

REAL is set
NAT is non empty V21() V22() V23() V34() V39() V40() Element of bool REAL
bool REAL is non empty set
NAT is non empty V21() V22() V23() V34() V39() V40() set
bool NAT is non empty V34() set
bool NAT is non empty V34() set
K320() is set
{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ext-real non positive non negative V21() V22() V23() V25() V26() V27() V28() V32() V33() V34() V39() V41( {} ) Function-yielding V56() set
1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
0 is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ext-real non positive non negative V21() V22() V23() V25() V26() V27() V28() V32() V33() V34() V39() V41( {} ) Function-yielding V56() Element of NAT
[0,0] is V15() set
{0,0} is functional non empty set
{0} is functional non empty trivial V41(1) set
{{0,0},{0}} is non empty set
<*[0,0]*> is Relation-like Function-like set
[1,0] is V15() set
{1,0} is non empty set
{1} is non empty trivial V41(1) set
{{1,0},{1}} is non empty set
<*[1,0]*> is Relation-like Function-like set
2 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
[2,0] is V15() set
{2,0} is non empty set
{2} is non empty trivial V41(1) set
{{2,0},{2}} is non empty set
<*[2,0]*> is Relation-like Function-like set
[:NAT,NAT:] is Relation-like non empty V34() set
[:NAT,[:NAT,NAT:]:] is Relation-like non empty V34() set
bool [:NAT,[:NAT,NAT:]:] is non empty V34() set
[0,0] is V15() Element of [:NAT,NAT:]
<*[0,0]*> is Relation-like Function-like FinSequence-like FinSequence of [:NAT,NAT:]
[1,0] is V15() Element of [:NAT,NAT:]
<*[1,0]*> is Relation-like Function-like FinSequence-like FinSequence of [:NAT,NAT:]
[2,0] is V15() Element of [:NAT,NAT:]
<*[2,0]*> is Relation-like Function-like FinSequence-like FinSequence of [:NAT,NAT:]
3 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
[3,0] is V15() Element of [:NAT,NAT:]
{3,0} is non empty set
{3} is non empty trivial V41(1) set
{{3,0},{3}} is non empty set
<*[3,0]*> is Relation-like Function-like FinSequence-like FinSequence of [:NAT,NAT:]
Al is Relation-like non empty QC-alphabet
vSUB Al is functional non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
VERUM Al is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
p is Relation-like Function-like Element of vSUB Al
[(VERUM Al),p] is V15() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is Relation-like non empty set
{(VERUM Al),p} is non empty set
{(VERUM Al)} is non empty trivial V41(1) set
{{(VERUM Al),p},{(VERUM Al)}} is non empty set
r is Element of QC-Sub-WFF Al
r `1 is Element of CQC-WFF Al
r `2 is Relation-like Function-like Element of vSUB Al
{ b₁ where b₁ is Element of QC-Sub-WFF Al : b₁ `1 is Element of CQC-WFF Al } is set
s is Element of QC-Sub-WFF Al
s `1 is Element of QC-WFF Al
r `1 is Element of QC-WFF Al
s is Element of CQC-Sub-WFF Al
s `2 is Relation-like Function-like Element of vSUB Al
Al is Relation-like non empty QC-alphabet
QC-pred_symbols Al is non empty set
p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
p -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
bool (QC-pred_symbols Al) is non empty set
r is Element of p -ary_QC-pred_symbols Al
s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
{ b₁ where b₁ is Element of QC-pred_symbols Al : the_arity_of b₁ = s } is set
{ b₁ where b₁ is Element of QC-pred_symbols Al : the_arity_of b₁ = s } is set
m is Element of QC-pred_symbols Al
the_arity_of m is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
m is Element of QC-pred_symbols Al
the_arity_of m is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Al is Relation-like non empty QC-alphabet
QC-pred_symbols Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
vSUB Al is functional non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
p -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
bool (QC-pred_symbols Al) is non empty set
r is Element of p -ary_QC-pred_symbols Al
s is Relation-like bound_QC-variables Al -valued Function-like V41(p) FinSequence-like FinSequence of QC-variables Al
r ! s is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
s is Relation-like Function-like Element of vSUB Al
the_arity_of r is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(the_arity_of r) -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
<*r*> is Relation-like Function-like FinSequence-like FinSequence of p -ary_QC-pred_symbols Al
<*r*> ^ s is Relation-like Function-like FinSequence-like set
[(<*r*> ^ s),s] is V15() set
{(<*r*> ^ s),s} is functional non empty set
{(<*r*> ^ s)} is functional non empty trivial V41(1) set
{{(<*r*> ^ s),s},{(<*r*> ^ s)}} is non empty set
len s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
[(r ! s),s] is V15() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is Relation-like non empty set
{(r ! s),s} is non empty set
{(r ! s)} is non empty trivial V41(1) set
{{(r ! s),s},{(r ! s)}} is non empty set
{ b₁ where b₁ is Element of QC-Sub-WFF Al : b₁ `1 is Element of CQC-WFF Al } is set
l is Element of QC-Sub-WFF Al
l `1 is Element of QC-WFF Al
m is Element of QC-Sub-WFF Al
m `1 is Element of CQC-WFF Al
m `2 is Relation-like Function-like Element of vSUB Al
m `1 is Element of QC-WFF Al
l is Element of CQC-Sub-WFF Al
l `2 is Relation-like Function-like Element of vSUB Al
Al is Relation-like non empty QC-alphabet
QC-pred_symbols Al is non empty set
p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
p -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
bool (QC-pred_symbols Al) is non empty set
r is Element of p -ary_QC-pred_symbols Al
s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
vSUB Al is functional non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
p is Element of CQC-WFF Al
'not' p is Element of CQC-WFF Al
r is Relation-like Function-like Element of vSUB Al
s is Element of CQC-Sub-WFF Al
s `1 is Element of CQC-WFF Al
s `2 is Relation-like Function-like Element of vSUB Al
[p,r] is V15() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is Relation-like non empty set
{p,r} is non empty set
{p} is non empty trivial V41(1) set
{{p,r},{p}} is non empty set
QC-symbols Al is non empty set
[:NAT,(QC-symbols Al):] is Relation-like non empty V34() set
[:NAT,[:NAT,(QC-symbols Al):]:] is Relation-like non empty V34() set
bool [:NAT,[:NAT,(QC-symbols Al):]:] is non empty V34() set
@ p is Relation-like Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols Al):]
[(@ p),r] is V15() Element of [:(bool [:NAT,[:NAT,(QC-symbols Al):]:]),(vSUB Al):]
[:(bool [:NAT,[:NAT,(QC-symbols Al):]:]),(vSUB Al):] is Relation-like non empty V34() set
{(@ p),r} is functional non empty set
{(@ p)} is functional non empty trivial V41(1) set
{{(@ p),r},{(@ p)}} is non empty set
<*[1,0]*> ^ (@ p) is Relation-like Function-like FinSequence-like set
[(<*[1,0]*> ^ (@ p)),r] is V15() set
{(<*[1,0]*> ^ (@ p)),r} is functional non empty set
{(<*[1,0]*> ^ (@ p))} is functional non empty trivial V41(1) set
{{(<*[1,0]*> ^ (@ p)),r},{(<*[1,0]*> ^ (@ p))}} is non empty set
[('not' p),r] is V15() Element of [:(CQC-WFF Al),(vSUB Al):]
{('not' p),r} is non empty set
{('not' p)} is non empty trivial V41(1) set
{{('not' p),r},{('not' p)}} is non empty set
{ b₁ where b₁ is Element of QC-Sub-WFF Al : b₁ `1 is Element of CQC-WFF Al } is set
m is Element of QC-Sub-WFF Al
m `1 is Element of QC-WFF Al
s is Element of QC-Sub-WFF Al
s `1 is Element of CQC-WFF Al
s `2 is Relation-like Function-like Element of vSUB Al
s `1 is Element of QC-WFF Al
m is Element of CQC-Sub-WFF Al
m `2 is Relation-like Function-like Element of vSUB Al
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
vSUB Al is functional non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
p is Element of CQC-WFF Al
r is Element of CQC-WFF Al
p '&' r is Element of CQC-WFF Al
s is Relation-like Function-like Element of vSUB Al
s is Element of CQC-Sub-WFF Al
s `1 is Element of CQC-WFF Al
s `2 is Relation-like Function-like Element of vSUB Al
m is Element of CQC-Sub-WFF Al
m `1 is Element of CQC-WFF Al
m `2 is Relation-like Function-like Element of vSUB Al
[r,s] is V15() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is Relation-like non empty set
{r,s} is non empty set
{r} is non empty trivial V41(1) set
{{r,s},{r}} is non empty set
QC-symbols Al is non empty set
[:NAT,(QC-symbols Al):] is Relation-like non empty V34() set
[:NAT,[:NAT,(QC-symbols Al):]:] is Relation-like non empty V34() set
bool [:NAT,[:NAT,(QC-symbols Al):]:] is non empty V34() set
@ r is Relation-like Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols Al):]
[(@ r),s] is V15() Element of [:(bool [:NAT,[:NAT,(QC-symbols Al):]:]),(vSUB Al):]
[:(bool [:NAT,[:NAT,(QC-symbols Al):]:]),(vSUB Al):] is Relation-like non empty V34() set
{(@ r),s} is functional non empty set
{(@ r)} is functional non empty trivial V41(1) set
{{(@ r),s},{(@ r)}} is non empty set
[p,s] is V15() Element of [:(CQC-WFF Al),(vSUB Al):]
{p,s} is non empty set
{p} is non empty trivial V41(1) set
{{p,s},{p}} is non empty set
@ p is Relation-like Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols Al):]
[(@ p),s] is V15() Element of [:(bool [:NAT,[:NAT,(QC-symbols Al):]:]),(vSUB Al):]
{(@ p),s} is functional non empty set
{(@ p)} is functional non empty trivial V41(1) set
{{(@ p),s},{(@ p)}} is non empty set
<*[2,0]*> ^ (@ p) is Relation-like Function-like FinSequence-like set
(<*[2,0]*> ^ (@ p)) ^ (@ r) is Relation-like Function-like FinSequence-like set
[((<*[2,0]*> ^ (@ p)) ^ (@ r)),s] is V15() set
{((<*[2,0]*> ^ (@ p)) ^ (@ r)),s} is functional non empty set
{((<*[2,0]*> ^ (@ p)) ^ (@ r))} is functional non empty trivial V41(1) set
{{((<*[2,0]*> ^ (@ p)) ^ (@ r)),s},{((<*[2,0]*> ^ (@ p)) ^ (@ r))}} is non empty set
[(p '&' r),s] is V15() Element of [:(CQC-WFF Al),(vSUB Al):]
{(p '&' r),s} is non empty set
{(p '&' r)} is non empty trivial V41(1) set
{{(p '&' r),s},{(p '&' r)}} is non empty set
{ b₁ where b₁ is Element of QC-Sub-WFF Al : b₁ `1 is Element of CQC-WFF Al } is set
k is Element of QC-Sub-WFF Al
k `1 is Element of QC-WFF Al
m is Element of QC-Sub-WFF Al
m `1 is Element of CQC-WFF Al
m `2 is Relation-like Function-like Element of vSUB Al
m `1 is Element of QC-WFF Al
k is Element of CQC-Sub-WFF Al
k `2 is Relation-like Function-like Element of vSUB Al
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
vSUB Al is functional non empty set
p is Element of CQC-WFF Al
r is Relation-like Function-like Element of vSUB Al
[p,r] is V15() set
{p,r} is non empty set
{p} is non empty trivial V41(1) set
{{p,r},{p}} is non empty set
[:(QC-WFF Al),(vSUB Al):] is Relation-like non empty set
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
vSUB Al is functional non empty set
p is Element of CQC-WFF Al
r is Element of bound_QC-variables Al
All (r,p) is Element of CQC-WFF Al
{r} is non empty trivial V41(1) Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
s is Relation-like Function-like Element of vSUB Al
RestrictSub (r,(All (r,p)),s) is Relation-like Function-like V34() Element of vSUB Al
proj1 (RestrictSub (r,(All (r,p)),s)) is set
still_not-bound_in (All (r,p)) is Element of bool (bound_QC-variables Al)
proj1 s is set
{ b₁ where b₁ is Element of bound_QC-variables Al : ( b₁ in still_not-bound_in (All (r,p)) & b₁ is Element of proj1 s & not b₁ = r & not b₁ = s . b₁ ) } is set
l is set
s | { b₁ where b₁ is Element of bound_QC-variables Al : ( b₁ in still_not-bound_in (All (r,p)) & b₁ is Element of proj1 s & not b₁ = r & not b₁ = s . b₁ ) } is Relation-like Function-like Element of vSUB Al
@ s is Relation-like Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
[:(bound_QC-variables Al),(bound_QC-variables Al):] is Relation-like non empty set
bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set
(@ s) | { b₁ where b₁ is Element of bound_QC-variables Al : ( b₁ in still_not-bound_in (All (r,p)) & b₁ is Element of proj1 s & not b₁ = r & not b₁ = s . b₁ ) } is Relation-like Function-like set
@ (RestrictSub (r,(All (r,p)),s)) is Relation-like Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
proj1 (@ (RestrictSub (r,(All (r,p)),s))) is set
proj1 (@ s) is set
(proj1 (@ s)) /\ { b₁ where b₁ is Element of bound_QC-variables Al : ( b₁ in still_not-bound_in (All (r,p)) & b₁ is Element of proj1 s & not b₁ = r & not b₁ = s . b₁ ) } is set
k is Element of bound_QC-variables Al
s . k is set
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
vSUB Al is functional non empty set
p is Element of CQC-WFF Al
r is Element of bound_QC-variables Al
All (r,p) is Element of CQC-WFF Al
s is Relation-like Function-like Element of vSUB Al
RestrictSub (r,(All (r,p)),s) is Relation-like Function-like V34() Element of vSUB Al
proj2 (RestrictSub (r,(All (r,p)),s)) is set
(Al,(All (r,p)),s) is V15() Element of [:(QC-WFF Al),(vSUB Al):]
[:(QC-WFF Al),(vSUB Al):] is Relation-like non empty set
{(All (r,p)),s} is non empty set
{(All (r,p))} is non empty trivial V41(1) set
{{(All (r,p)),s},{(All (r,p))}} is non empty set
S_Bound (Al,(All (r,p)),s) is Element of bound_QC-variables Al
upVar ((RestrictSub (r,(All (r,p)),s)),p) is Element of QC-symbols Al
QC-symbols Al is non empty set
x. (upVar ((RestrictSub (r,(All (r,p)),s)),p)) is Element of bound_QC-variables Al
(Al,(All (r,p)),s) `1 is Element of QC-WFF Al
(Al,(All (r,p)),s) `2 is Relation-like Function-like Element of vSUB Al
m is Element of CQC-WFF Al
bound_in m is Element of bound_QC-variables Al
the_scope_of m is Element of QC-WFF Al
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
vSUB Al is functional non empty set
p is Element of CQC-WFF Al
r is Element of bound_QC-variables Al
All (r,p) is Element of CQC-WFF Al
s is Relation-like Function-like Element of vSUB Al
RestrictSub (r,(All (r,p)),s) is Relation-like Function-like V34() Element of vSUB Al
proj2 (RestrictSub (r,(All (r,p)),s)) is set
(Al,(All (r,p)),s) is V15() Element of [:(QC-WFF Al),(vSUB Al):]
[:(QC-WFF Al),(vSUB Al):] is Relation-like non empty set
{(All (r,p)),s} is non empty set
{(All (r,p))} is non empty trivial V41(1) set
{{(All (r,p)),s},{(All (r,p))}} is non empty set
S_Bound (Al,(All (r,p)),s) is Element of bound_QC-variables Al
(Al,(All (r,p)),s) `1 is Element of QC-WFF Al
(Al,(All (r,p)),s) `2 is Relation-like Function-like Element of vSUB Al
m is Element of CQC-WFF Al
bound_in m is Element of bound_QC-variables Al
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
vSUB Al is functional non empty set
p is Element of CQC-WFF Al
r is Element of bound_QC-variables Al
All (r,p) is Element of CQC-WFF Al
s is Relation-like Function-like Element of vSUB Al
RestrictSub (r,(All (r,p)),s) is Relation-like Function-like V34() Element of vSUB Al
ExpandSub (r,p,(RestrictSub (r,(All (r,p)),s))) is Relation-like Function-like Element of vSUB Al
@ (RestrictSub (r,(All (r,p)),s)) is Relation-like Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
[:(bound_QC-variables Al),(bound_QC-variables Al):] is Relation-like non empty set
bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set
(Al,(All (r,p)),s) is V15() Element of [:(QC-WFF Al),(vSUB Al):]
[:(QC-WFF Al),(vSUB Al):] is Relation-like non empty set
{(All (r,p)),s} is non empty set
{(All (r,p))} is non empty trivial V41(1) set
{{(All (r,p)),s},{(All (r,p))}} is non empty set
S_Bound (Al,(All (r,p)),s) is Element of bound_QC-variables Al
r | (S_Bound (Al,(All (r,p)),s)) is Relation-like bound_QC-variables Al -defined {r} -defined bound_QC-variables Al -valued Function-like one-to-one Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
{r} is non empty trivial V41(1) set
{r} --> (S_Bound (Al,(All (r,p)),s)) is Relation-like {r} -defined bound_QC-variables Al -valued Function-like constant non empty total V29({r},{(S_Bound (Al,(All (r,p)),s))}) Element of bool [:{r},{(S_Bound (Al,(All (r,p)),s))}:]
{(S_Bound (Al,(All (r,p)),s))} is non empty trivial V41(1) set
[:{r},{(S_Bound (Al,(All (r,p)),s))}:] is Relation-like non empty set
bool [:{r},{(S_Bound (Al,(All (r,p)),s))}:] is non empty set
(@ (RestrictSub (r,(All (r,p)),s))) +* (r | (S_Bound (Al,(All (r,p)),s))) is Relation-like Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
upVar ((RestrictSub (r,(All (r,p)),s)),p) is Element of QC-symbols Al
QC-symbols Al is non empty set
x. (upVar ((RestrictSub (r,(All (r,p)),s)),p)) is Element of bound_QC-variables Al
[r,(x. (upVar ((RestrictSub (r,(All (r,p)),s)),p)))] is V15() Element of [:(bound_QC-variables Al),(bound_QC-variables Al):]
{r,(x. (upVar ((RestrictSub (r,(All (r,p)),s)),p)))} is non empty set
{{r,(x. (upVar ((RestrictSub (r,(All (r,p)),s)),p)))},{r}} is non empty set
{[r,(x. (upVar ((RestrictSub (r,(All (r,p)),s)),p)))]} is Relation-like Function-like constant non empty trivial V41(1) Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
m is Relation-like Function-like set
proj1 m is set
{r} is non empty trivial V41(1) Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
proj1 (RestrictSub (r,(All (r,p)),s)) is set
proj1 (@ (RestrictSub (r,(All (r,p)),s))) is set
(@ (RestrictSub (r,(All (r,p)),s))) \/ m is Relation-like set
(@ (RestrictSub (r,(All (r,p)),s))) +* m is Relation-like Function-like set
proj2 (RestrictSub (r,(All (r,p)),s)) is set
(RestrictSub (r,(All (r,p)),s)) \/ m is Relation-like set
r .--> (x. (upVar ((RestrictSub (r,(All (r,p)),s)),p))) is Relation-like bound_QC-variables Al -defined {r} -defined bound_QC-variables Al -valued Function-like one-to-one set
{r} --> (x. (upVar ((RestrictSub (r,(All (r,p)),s)),p))) is Relation-like {r} -defined bound_QC-variables Al -valued Function-like constant non empty total V29({r},{(x. (upVar ((RestrictSub (r,(All (r,p)),s)),p)))}) Element of bool [:{r},{(x. (upVar ((RestrictSub (r,(All (r,p)),s)),p)))}:]
{(x. (upVar ((RestrictSub (r,(All (r,p)),s)),p)))} is non empty trivial V41(1) set
[:{r},{(x. (upVar ((RestrictSub (r,(All (r,p)),s)),p)))}:] is Relation-like non empty set
bool [:{r},{(x. (upVar ((RestrictSub (r,(All (r,p)),s)),p)))}:] is non empty set
[r,r] is V15() Element of [:(bound_QC-variables Al),(bound_QC-variables Al):]
{r,r} is non empty set
{{r,r},{r}} is non empty set
{[r,r]} is Relation-like Function-like constant non empty trivial V41(1) Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
m is Relation-like Function-like set
proj1 m is set
(@ (RestrictSub (r,(All (r,p)),s))) \/ m is Relation-like set
(@ (RestrictSub (r,(All (r,p)),s))) +* m is Relation-like Function-like set
(RestrictSub (r,(All (r,p)),s)) \/ m is Relation-like set
r .--> r is Relation-like bound_QC-variables Al -defined {r} -defined bound_QC-variables Al -valued Function-like one-to-one set
{r} --> r is Relation-like {r} -defined bound_QC-variables Al -valued Function-like constant non empty total V29({r},{r}) Element of bool [:{r},{r}:]
[:{r},{r}:] is Relation-like non empty set
bool [:{r},{r}:] is non empty set
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
vSUB Al is functional non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
p is Element of CQC-WFF Al
r is Element of bound_QC-variables Al
All (r,p) is Element of CQC-WFF Al
s is Relation-like Function-like Element of vSUB Al
RestrictSub (r,(All (r,p)),s) is Relation-like Function-like V34() Element of vSUB Al
@ (RestrictSub (r,(All (r,p)),s)) is Relation-like Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
[:(bound_QC-variables Al),(bound_QC-variables Al):] is Relation-like non empty set
bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set
(Al,(All (r,p)),s) is V15() Element of [:(QC-WFF Al),(vSUB Al):]
[:(QC-WFF Al),(vSUB Al):] is Relation-like non empty set
{(All (r,p)),s} is non empty set
{(All (r,p))} is non empty trivial V41(1) set
{{(All (r,p)),s},{(All (r,p))}} is non empty set
S_Bound (Al,(All (r,p)),s) is Element of bound_QC-variables Al
r | (S_Bound (Al,(All (r,p)),s)) is Relation-like bound_QC-variables Al -defined {r} -defined bound_QC-variables Al -valued Function-like one-to-one Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
{r} is non empty trivial V41(1) set
{r} --> (S_Bound (Al,(All (r,p)),s)) is Relation-like {r} -defined bound_QC-variables Al -valued Function-like constant non empty total V29({r},{(S_Bound (Al,(All (r,p)),s))}) Element of bool [:{r},{(S_Bound (Al,(All (r,p)),s))}:]
{(S_Bound (Al,(All (r,p)),s))} is non empty trivial V41(1) set
[:{r},{(S_Bound (Al,(All (r,p)),s))}:] is Relation-like non empty set
bool [:{r},{(S_Bound (Al,(All (r,p)),s))}:] is non empty set
(@ (RestrictSub (r,(All (r,p)),s))) +* (r | (S_Bound (Al,(All (r,p)),s))) is Relation-like Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
s is Element of CQC-Sub-WFF Al
s `2 is Relation-like Function-like Element of vSUB Al
s `1 is Element of CQC-WFF Al
[s,r] is V15() CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
[:(QC-Sub-WFF Al),(bound_QC-variables Al):] is Relation-like non empty set
{s,r} is non empty set
{s} is non empty trivial V41(1) set
{{s,r},{s}} is non empty set
[s,r] `2 is Element of bound_QC-variables Al
[s,r] `1 is Element of CQC-Sub-WFF Al
([s,r] `1) `1 is Element of CQC-WFF Al
the_scope_of (All (r,p)) is Element of QC-WFF Al
m is Relation-like Function-like Element of vSUB Al
RestrictSub (r,(All (r,p)),m) is Relation-like Function-like V34() Element of vSUB Al
ExpandSub (r,p,(RestrictSub (r,(All (r,p)),m))) is Relation-like Function-like Element of vSUB Al
bound_in (All (r,p)) is Element of bound_QC-variables Al
(Al,(All (r,p)),m) is V15() Element of [:(QC-WFF Al),(vSUB Al):]
{(All (r,p)),m} is non empty set
{{(All (r,p)),m},{(All (r,p))}} is non empty set
[(Al,(All (r,p)),m),((@ (RestrictSub (r,(All (r,p)),s))) +* (r | (S_Bound (Al,(All (r,p)),s))))] is V15() Element of [:[:(QC-WFF Al),(vSUB Al):],(bool [:(bound_QC-variables Al),(bound_QC-variables Al):]):]
[:[:(QC-WFF Al),(vSUB Al):],(bool [:(bound_QC-variables Al),(bound_QC-variables Al):]):] is Relation-like non empty set
{(Al,(All (r,p)),m),((@ (RestrictSub (r,(All (r,p)),s))) +* (r | (S_Bound (Al,(All (r,p)),s))))} is non empty set
{(Al,(All (r,p)),m)} is Relation-like Function-like constant non empty trivial V41(1) set
{{(Al,(All (r,p)),m),((@ (RestrictSub (r,(All (r,p)),s))) +* (r | (S_Bound (Al,(All (r,p)),s))))},{(Al,(All (r,p)),m)}} is non empty set
l is set
QSub Al is Relation-like Function-like set
(QSub Al) . (Al,(All (r,p)),m) is set
([s,r] `1) `2 is Relation-like Function-like Element of vSUB Al
k is Relation-like Function-like second_Q_comp of [s,r]
CQCSub_All ([s,r],k) is Element of CQC-Sub-WFF Al
j is Element of CQC-Sub-WFF Al
Sub_All ([s,r],k) is Element of QC-Sub-WFF Al
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
vSUB Al is functional non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
p is Element of CQC-WFF Al
r is Element of bound_QC-variables Al
All (r,p) is Element of CQC-WFF Al
s is Relation-like Function-like Element of vSUB Al
RestrictSub (r,(All (r,p)),s) is Relation-like Function-like V34() Element of vSUB Al
@ (RestrictSub (r,(All (r,p)),s)) is Relation-like Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
[:(bound_QC-variables Al),(bound_QC-variables Al):] is Relation-like non empty set
bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set
(Al,(All (r,p)),s) is V15() Element of [:(QC-WFF Al),(vSUB Al):]
[:(QC-WFF Al),(vSUB Al):] is Relation-like non empty set
{(All (r,p)),s} is non empty set
{(All (r,p))} is non empty trivial V41(1) set
{{(All (r,p)),s},{(All (r,p))}} is non empty set
S_Bound (Al,(All (r,p)),s) is Element of bound_QC-variables Al
r | (S_Bound (Al,(All (r,p)),s)) is Relation-like bound_QC-variables Al -defined {r} -defined bound_QC-variables Al -valued Function-like one-to-one Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
{r} is non empty trivial V41(1) set
{r} --> (S_Bound (Al,(All (r,p)),s)) is Relation-like {r} -defined bound_QC-variables Al -valued Function-like constant non empty total V29({r},{(S_Bound (Al,(All (r,p)),s))}) Element of bool [:{r},{(S_Bound (Al,(All (r,p)),s))}:]
{(S_Bound (Al,(All (r,p)),s))} is non empty trivial V41(1) set
[:{r},{(S_Bound (Al,(All (r,p)),s))}:] is Relation-like non empty set
bool [:{r},{(S_Bound (Al,(All (r,p)),s))}:] is non empty set
(@ (RestrictSub (r,(All (r,p)),s))) +* (r | (S_Bound (Al,(All (r,p)),s))) is Relation-like Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
PFuncs ((bound_QC-variables Al),(bound_QC-variables Al)) is set
m is Relation-like Function-like Element of vSUB Al
m is Element of CQC-Sub-WFF Al
m `1 is Element of CQC-WFF Al
m `2 is Relation-like Function-like Element of vSUB Al
m is Element of CQC-Sub-WFF Al
m `1 is Element of CQC-WFF Al
m `2 is Relation-like Function-like Element of vSUB Al
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
vSUB Al is functional non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
QC-pred_symbols Al is non empty set
VERUM Al is Element of CQC-WFF Al
r is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
bool (QC-pred_symbols Al) is non empty set
p is Relation-like Function-like Element of vSUB Al
s is Element of r -ary_QC-pred_symbols Al
s is Relation-like bound_QC-variables Al -valued Function-like V41(r) FinSequence-like FinSequence of QC-variables Al
s ! s is Element of CQC-WFF Al
m is Relation-like Function-like Element of vSUB Al
m is Element of CQC-WFF Al
'not' m is Element of CQC-WFF Al
l is Relation-like Function-like Element of vSUB Al
k is Element of CQC-WFF Al
j is Element of CQC-WFF Al
k '&' j is Element of CQC-WFF Al
j1 is Relation-like Function-like Element of vSUB Al
G1 is Element of CQC-WFF Al
H1 is Element of bound_QC-variables Al
All (H1,G1) is Element of CQC-WFF Al
r is Relation-like Function-like Element of vSUB Al
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
vSUB Al is functional non empty set
p is Element of CQC-WFF Al
r is Relation-like Function-like Element of vSUB Al
[p,r] is V15() set
{p,r} is non empty set
{p} is non empty trivial V41(1) set
{{p,r},{p}} is non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
s is Element of CQC-Sub-WFF Al
s `1 is Element of CQC-WFF Al
s `2 is Relation-like Function-like Element of vSUB Al
Al is Relation-like non empty QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
Al is Relation-like non empty QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
p is Element of bound_QC-variables Al
r is Element of bound_QC-variables Al
p .--> r is Relation-like bound_QC-variables Al -defined {p} -defined bound_QC-variables Al -valued Function-like one-to-one set
{p} is non empty trivial V41(1) set
{p} --> r is Relation-like {p} -defined bound_QC-variables Al -valued Function-like constant non empty total V29({p},{r}) Element of bool [:{p},{r}:]
{r} is non empty trivial V41(1) set
[:{p},{r}:] is Relation-like non empty set
bool [:{p},{r}:] is non empty set
vSUB Al is functional non empty set
PFuncs ((bound_QC-variables Al),(bound_QC-variables Al)) is set
proj1 (p .--> r) is set
{p} is non empty trivial V41(1) Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
proj2 (p .--> r) is set
{r} is non empty trivial V41(1) Element of bool (bound_QC-variables Al)
[:(bound_QC-variables Al),(bound_QC-variables Al):] is Relation-like non empty set
bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
p is Element of CQC-WFF Al
r is Element of bound_QC-variables Al
s is Element of bound_QC-variables Al
(Al,r,s) is Relation-like bound_QC-variables Al -defined {r} -defined bound_QC-variables Al -valued Function-like one-to-one Element of vSUB Al
{r} is non empty trivial V41(1) set
vSUB Al is functional non empty set
{r} --> s is Relation-like {r} -defined bound_QC-variables Al -valued Function-like constant non empty total V29({r},{s}) Element of bool [:{r},{s}:]
{s} is non empty trivial V41(1) set
[:{r},{s}:] is Relation-like non empty set
bool [:{r},{s}:] is non empty set
(Al,p,(Al,r,s)) is V15() Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
{p,(Al,r,s)} is non empty set
{p} is non empty trivial V41(1) set
{{p,(Al,r,s)},{p}} is non empty set
CQC_Sub (Al,p,(Al,r,s)) is Element of CQC-WFF Al
F₁() is Relation-like non empty QC-alphabet
QC-WFF F₁() is non empty set
CQC-WFF F₁() is non empty Element of bool (QC-WFF F₁())
bool (QC-WFF F₁()) is non empty set
Al is Element of CQC-WFF F₁()
p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r is Element of CQC-WFF F₁()
QuantNbr r is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
p + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
p is Element of CQC-WFF F₁()
QuantNbr p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
QuantNbr Al is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
p is Element of CQC-WFF F₁()
QuantNbr p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
F₁() is Relation-like non empty QC-alphabet
QC-WFF F₁() is non empty set
CQC-WFF F₁() is non empty Element of bool (QC-WFF F₁())
bool (QC-WFF F₁()) is non empty set
Al is Element of CQC-WFF F₁()
p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r is Element of CQC-WFF F₁()
QuantNbr r is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
p + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
p is Element of CQC-WFF F₁()
QuantNbr p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
QuantNbr Al is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
p is Element of CQC-WFF F₁()
QuantNbr p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Al is Relation-like non empty QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
VERUM Al is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
p is Element of bound_QC-variables Al
r is Element of bound_QC-variables Al
(Al,(VERUM Al),p,r) is Element of CQC-WFF Al
(Al,p,r) is Relation-like bound_QC-variables Al -defined {p} -defined bound_QC-variables Al -valued Function-like one-to-one Element of vSUB Al
{p} is non empty trivial V41(1) set
vSUB Al is functional non empty set
{p} --> r is Relation-like {p} -defined bound_QC-variables Al -valued Function-like constant non empty total V29({p},{r}) Element of bool [:{p},{r}:]
{r} is non empty trivial V41(1) set
[:{p},{r}:] is Relation-like non empty set
bool [:{p},{r}:] is non empty set
(Al,(VERUM Al),(Al,p,r)) is V15() Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
{(VERUM Al),(Al,p,r)} is non empty set
{(VERUM Al)} is non empty trivial V41(1) set
{{(VERUM Al),(Al,p,r)},{(VERUM Al)}} is non empty set
CQC_Sub (Al,(VERUM Al),(Al,p,r)) is Element of CQC-WFF Al
Al is Relation-like non empty QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
QC-pred_symbols Al is non empty set
p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
p -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
bool (QC-pred_symbols Al) is non empty set
r is Element of bound_QC-variables Al
s is Element of bound_QC-variables Al
(Al,r,s) is Relation-like bound_QC-variables Al -defined {r} -defined bound_QC-variables Al -valued Function-like one-to-one Element of vSUB Al
{r} is non empty trivial V41(1) set
vSUB Al is functional non empty set
{r} --> s is Relation-like {r} -defined bound_QC-variables Al -valued Function-like constant non empty total V29({r},{s}) Element of bool [:{r},{s}:]
{s} is non empty trivial V41(1) set
[:{r},{s}:] is Relation-like non empty set
bool [:{r},{s}:] is non empty set
s is Element of p -ary_QC-pred_symbols Al
m is Relation-like bound_QC-variables Al -valued Function-like V41(p) FinSequence-like FinSequence of QC-variables Al
s ! m is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
(Al,(s ! m),r,s) is Element of CQC-WFF Al
(Al,(s ! m),(Al,r,s)) is V15() Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
{(s ! m),(Al,r,s)} is non empty set
{(s ! m)} is non empty trivial V41(1) set
{{(s ! m),(Al,r,s)},{(s ! m)}} is non empty set
CQC_Sub (Al,(s ! m),(Al,r,s)) is Element of CQC-WFF Al
CQC_Subst (m,(Al,r,s)) is Relation-like bound_QC-variables Al -valued Function-like V41(p) FinSequence-like FinSequence of QC-variables Al
s ! (CQC_Subst (m,(Al,r,s))) is Element of CQC-WFF Al
QuantNbr (s ! m) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
QuantNbr (Al,(s ! m),r,s) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Sub_P (s,m,(Al,r,s)) is Sub_atomic Element of CQC-Sub-WFF Al
QuantNbr (s ! (CQC_Subst (m,(Al,r,s)))) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Al is Relation-like non empty QC-alphabet
QC-pred_symbols Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
vSUB Al is functional non empty set
p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
p -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
bool (QC-pred_symbols Al) is non empty set
r is Element of p -ary_QC-pred_symbols Al
s is Relation-like bound_QC-variables Al -valued Function-like V41(p) FinSequence-like FinSequence of QC-variables Al
r ! s is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QuantNbr (r ! s) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s is Relation-like Function-like Element of vSUB Al
(Al,(r ! s),s) is V15() Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
{(r ! s),s} is non empty set
{(r ! s)} is non empty trivial V41(1) set
{{(r ! s),s},{(r ! s)}} is non empty set
CQC_Sub (Al,(r ! s),s) is Element of CQC-WFF Al
QuantNbr (CQC_Sub (Al,(r ! s),s)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Sub_P (r,s,s) is Sub_atomic Element of CQC-Sub-WFF Al
CQC_Subst (s,s) is Relation-like bound_QC-variables Al -valued Function-like V41(p) FinSequence-like FinSequence of QC-variables Al
r ! (CQC_Subst (s,s)) is Element of CQC-WFF Al
QuantNbr (r ! (CQC_Subst (s,s))) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Al is Relation-like non empty QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
p is Element of QC-Sub-WFF Al
p `2 is set
vSUB Al is functional non empty set
QC-WFF Al is non empty set
r is Element of QC-WFF Al
s is Relation-like Function-like Element of vSUB Al
[r,s] is V15() Element of [:(QC-WFF Al),(vSUB Al):]
[:(QC-WFF Al),(vSUB Al):] is Relation-like non empty set
{r,s} is non empty set
{r} is non empty trivial V41(1) set
{{r,s},{r}} is non empty set
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
vSUB Al is functional non empty set
p is Element of CQC-WFF Al
'not' p is Element of CQC-WFF Al
r is Relation-like Function-like Element of vSUB Al
(Al,('not' p),r) is V15() Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
{('not' p),r} is non empty set
{('not' p)} is non empty trivial V41(1) set
{{('not' p),r},{('not' p)}} is non empty set
(Al,p,r) is V15() Element of CQC-Sub-WFF Al
{p,r} is non empty set
{p} is non empty trivial V41(1) set
{{p,r},{p}} is non empty set
Sub_not (Al,p,r) is Sub_negative Element of CQC-Sub-WFF Al
(Al,p,r) `1 is Element of CQC-WFF Al
'not' ((Al,p,r) `1) is Element of CQC-WFF Al
(Al,(Al,p,r)) is Relation-like Function-like Element of vSUB Al
(Al,('not' ((Al,p,r) `1)),(Al,(Al,p,r))) is V15() Element of CQC-Sub-WFF Al
{('not' ((Al,p,r) `1)),(Al,(Al,p,r))} is non empty set
{('not' ((Al,p,r) `1))} is non empty trivial V41(1) set
{{('not' ((Al,p,r) `1)),(Al,(Al,p,r))},{('not' ((Al,p,r) `1))}} is non empty set
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
p is Element of CQC-WFF Al
QuantNbr p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
'not' p is Element of CQC-WFF Al
QuantNbr ('not' p) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r is Element of bound_QC-variables Al
s is Element of bound_QC-variables Al
(Al,p,r,s) is Element of CQC-WFF Al
(Al,r,s) is Relation-like bound_QC-variables Al -defined {r} -defined bound_QC-variables Al -valued Function-like one-to-one Element of vSUB Al
{r} is non empty trivial V41(1) set
vSUB Al is functional non empty set
{r} --> s is Relation-like {r} -defined bound_QC-variables Al -valued Function-like constant non empty total V29({r},{s}) Element of bool [:{r},{s}:]
{s} is non empty trivial V41(1) set
[:{r},{s}:] is Relation-like non empty set
bool [:{r},{s}:] is non empty set
(Al,p,(Al,r,s)) is V15() Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
{p,(Al,r,s)} is non empty set
{p} is non empty trivial V41(1) set
{{p,(Al,r,s)},{p}} is non empty set
CQC_Sub (Al,p,(Al,r,s)) is Element of CQC-WFF Al
'not' (Al,p,r,s) is Element of CQC-WFF Al
QuantNbr (Al,p,r,s) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
QuantNbr ('not' (Al,p,r,s)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(Al,('not' p),(Al,r,s)) is V15() Element of CQC-Sub-WFF Al
{('not' p),(Al,r,s)} is non empty set
{('not' p)} is non empty trivial V41(1) set
{{('not' p),(Al,r,s)},{('not' p)}} is non empty set
Sub_not (Al,p,(Al,r,s)) is Sub_negative Element of CQC-Sub-WFF Al
(Al,('not' p),r,s) is Element of CQC-WFF Al
CQC_Sub (Al,('not' p),(Al,r,s)) is Element of CQC-WFF Al
'not' (CQC_Sub (Al,p,(Al,r,s))) is Element of CQC-WFF Al
QuantNbr (Al,('not' p),r,s) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
vSUB Al is functional non empty set
p is Element of CQC-WFF Al
QuantNbr p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
'not' p is Element of CQC-WFF Al
QuantNbr ('not' p) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r is Relation-like Function-like Element of vSUB Al
(Al,('not' p),r) is V15() Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
{('not' p),r} is non empty set
{('not' p)} is non empty trivial V41(1) set
{{('not' p),r},{('not' p)}} is non empty set
CQC_Sub (Al,('not' p),r) is Element of CQC-WFF Al
QuantNbr (CQC_Sub (Al,('not' p),r)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(Al,p,r) is V15() Element of CQC-Sub-WFF Al
{p,r} is non empty set
{p} is non empty trivial V41(1) set
{{p,r},{p}} is non empty set
Sub_not (Al,p,r) is Sub_negative Element of CQC-Sub-WFF Al
CQC_Sub (Al,p,r) is Element of CQC-WFF Al
'not' (CQC_Sub (Al,p,r)) is Element of CQC-WFF Al
QuantNbr ('not' (CQC_Sub (Al,p,r))) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
QuantNbr (CQC_Sub (Al,p,r)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
vSUB Al is functional non empty set
p is Element of CQC-WFF Al
r is Element of CQC-WFF Al
p '&' r is Element of CQC-WFF Al
s is Relation-like Function-like Element of vSUB Al
(Al,(p '&' r),s) is V15() Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
{(p '&' r),s} is non empty set
{(p '&' r)} is non empty trivial V41(1) set
{{(p '&' r),s},{(p '&' r)}} is non empty set
(Al,p,s) is V15() Element of CQC-Sub-WFF Al
{p,s} is non empty set
{p} is non empty trivial V41(1) set
{{p,s},{p}} is non empty set
(Al,r,s) is V15() Element of CQC-Sub-WFF Al
{r,s} is non empty set
{r} is non empty trivial V41(1) set
{{r,s},{r}} is non empty set
CQCSub_& ((Al,p,s),(Al,r,s)) is Element of CQC-Sub-WFF Al
(Al,p,s) `1 is Element of CQC-WFF Al
(Al,r,s) `1 is Element of CQC-WFF Al
(Al,(Al,p,s)) is Relation-like Function-like Element of vSUB Al
(Al,(Al,r,s)) is Relation-like Function-like Element of vSUB Al
Sub_& ((Al,p,s),(Al,r,s)) is Element of QC-Sub-WFF Al
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
p is Element of CQC-WFF Al
QuantNbr p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r is Element of CQC-WFF Al
p '&' r is Element of CQC-WFF Al
QuantNbr r is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
QuantNbr (p '&' r) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s is Element of bound_QC-variables Al
s is Element of bound_QC-variables Al
(Al,(p '&' r),s,s) is Element of CQC-WFF Al
(Al,s,s) is Relation-like bound_QC-variables Al -defined {s} -defined bound_QC-variables Al -valued Function-like one-to-one Element of vSUB Al
{s} is non empty trivial V41(1) set
vSUB Al is functional non empty set
{s} --> s is Relation-like {s} -defined bound_QC-variables Al -valued Function-like constant non empty total V29({s},{s}) Element of bool [:{s},{s}:]
{s} is non empty trivial V41(1) set
[:{s},{s}:] is Relation-like non empty set
bool [:{s},{s}:] is non empty set
(Al,(p '&' r),(Al,s,s)) is V15() Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
{(p '&' r),(Al,s,s)} is non empty set
{(p '&' r)} is non empty trivial V41(1) set
{{(p '&' r),(Al,s,s)},{(p '&' r)}} is non empty set
CQC_Sub (Al,(p '&' r),(Al,s,s)) is Element of CQC-WFF Al
(Al,p,s,s) is Element of CQC-WFF Al
(Al,p,(Al,s,s)) is V15() Element of CQC-Sub-WFF Al
{p,(Al,s,s)} is non empty set
{p} is non empty trivial V41(1) set
{{p,(Al,s,s)},{p}} is non empty set
CQC_Sub (Al,p,(Al,s,s)) is Element of CQC-WFF Al
(Al,r,s,s) is Element of CQC-WFF Al
(Al,r,(Al,s,s)) is V15() Element of CQC-Sub-WFF Al
{r,(Al,s,s)} is non empty set
{r} is non empty trivial V41(1) set
{{r,(Al,s,s)},{r}} is non empty set
CQC_Sub (Al,r,(Al,s,s)) is Element of CQC-WFF Al
(Al,p,s,s) '&' (Al,r,s,s) is Element of CQC-WFF Al
QuantNbr (Al,p,s,s) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
QuantNbr (Al,r,s,s) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
QuantNbr (Al,(p '&' r),s,s) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(Al,(Al,p,(Al,s,s))) is Relation-like Function-like Element of vSUB Al
(Al,(Al,r,(Al,s,s))) is Relation-like Function-like Element of vSUB Al
CQCSub_& ((Al,p,(Al,s,s)),(Al,r,(Al,s,s))) is Element of CQC-Sub-WFF Al
Sub_& ((Al,p,(Al,s,s)),(Al,r,(Al,s,s))) is Element of QC-Sub-WFF Al
(CQC_Sub (Al,p,(Al,s,s))) '&' (CQC_Sub (Al,r,(Al,s,s))) is Element of CQC-WFF Al
(QuantNbr (Al,p,s,s)) + (QuantNbr (Al,r,s,s)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
vSUB Al is functional non empty set
p is Element of CQC-WFF Al
QuantNbr p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r is Element of CQC-WFF Al
QuantNbr r is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
p '&' r is Element of CQC-WFF Al
QuantNbr (p '&' r) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s is Relation-like Function-like Element of vSUB Al
(Al,(p '&' r),s) is V15() Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
{(p '&' r),s} is non empty set
{(p '&' r)} is non empty trivial V41(1) set
{{(p '&' r),s},{(p '&' r)}} is non empty set
CQC_Sub (Al,(p '&' r),s) is Element of CQC-WFF Al
QuantNbr (CQC_Sub (Al,(p '&' r),s)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(Al,p,s) is V15() Element of CQC-Sub-WFF Al
{p,s} is non empty set
{p} is non empty trivial V41(1) set
{{p,s},{p}} is non empty set
(Al,r,s) is V15() Element of CQC-Sub-WFF Al
{r,s} is non empty set
{r} is non empty trivial V41(1) set
{{r,s},{r}} is non empty set
(Al,(Al,p,s)) is Relation-like Function-like Element of vSUB Al
(Al,(Al,r,s)) is Relation-like Function-like Element of vSUB Al
CQCSub_& ((Al,p,s),(Al,r,s)) is Element of CQC-Sub-WFF Al
Sub_& ((Al,p,s),(Al,r,s)) is Element of QC-Sub-WFF Al
CQC_Sub (Al,p,s) is Element of CQC-WFF Al
CQC_Sub (Al,r,s) is Element of CQC-WFF Al
(CQC_Sub (Al,p,s)) '&' (CQC_Sub (Al,r,s)) is Element of CQC-WFF Al
QuantNbr (CQC_Sub (Al,p,s)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
QuantNbr (CQC_Sub (Al,r,s)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(QuantNbr (CQC_Sub (Al,p,s))) + (QuantNbr (CQC_Sub (Al,r,s))) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(QuantNbr p) + (QuantNbr (CQC_Sub (Al,r,s))) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(QuantNbr p) + (QuantNbr r) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Al is Relation-like non empty QC-alphabet
QSub Al is Relation-like Function-like set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
QC-Sub-WFF Al is non empty Al -Sub-closed set
bool (QC-Sub-WFF Al) is non empty set
(QSub Al) | (CQC-Sub-WFF Al) is Relation-like Function-like set
vSUB Al is functional non empty set
[:(CQC-Sub-WFF Al),(vSUB Al):] is Relation-like non empty set
bool [:(CQC-Sub-WFF Al),(vSUB Al):] is non empty set
p is set
QC-WFF Al is non empty set
r is Element of QC-WFF Al
s is Relation-like Function-like Element of vSUB Al
[r,s] is V15() Element of [:(QC-WFF Al),(vSUB Al):]
[:(QC-WFF Al),(vSUB Al):] is Relation-like non empty set
{r,s} is non empty set
{r} is non empty trivial V41(1) set
{{r,s},{r}} is non empty set
[[r,s],{}] is V15() set
{[r,s],{}} is non empty set
{[r,s]} is Relation-like Function-like constant non empty trivial V41(1) set
{{[r,s],{}},{[r,s]}} is non empty set
proj1 (QSub Al) is set
bound_in r is Element of bound_QC-variables Al
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
the_scope_of r is Element of QC-WFF Al
RestrictSub ((bound_in r),r,s) is Relation-like Function-like V34() Element of vSUB Al
ExpandSub ((bound_in r),(the_scope_of r),(RestrictSub ((bound_in r),r,s))) is Relation-like Function-like Element of vSUB Al
[[r,s],(ExpandSub ((bound_in r),(the_scope_of r),(RestrictSub ((bound_in r),r,s))))] is V15() Element of [:[:(QC-WFF Al),(vSUB Al):],(vSUB Al):]
[:[:(QC-WFF Al),(vSUB Al):],(vSUB Al):] is Relation-like non empty set
{[r,s],(ExpandSub ((bound_in r),(the_scope_of r),(RestrictSub ((bound_in r),r,s))))} is non empty set
{{[r,s],(ExpandSub ((bound_in r),(the_scope_of r),(RestrictSub ((bound_in r),r,s))))},{[r,s]}} is non empty set
proj1 ((QSub Al) | (CQC-Sub-WFF Al)) is set
proj2 ((QSub Al) | (CQC-Sub-WFF Al)) is set
p is set
r is set
((QSub Al) | (CQC-Sub-WFF Al)) . r is set
[r,p] is V15() set
{r,p} is non empty set
{r} is non empty trivial V41(1) set
{{r,p},{r}} is non empty set
s is Element of QC-WFF Al
s is Relation-like Function-like Element of vSUB Al
[s,s] is V15() Element of [:(QC-WFF Al),(vSUB Al):]
{s,s} is non empty set
{s} is non empty trivial V41(1) set
{{s,s},{s}} is non empty set
m is set
[[s,s],m] is V15() set
{[s,s],m} is non empty set
{[s,s]} is Relation-like Function-like constant non empty trivial V41(1) set
{{[s,s],m},{[s,s]}} is non empty set
PFuncs ((bound_QC-variables Al),(bound_QC-variables Al)) is set
[:(bound_QC-variables Al),(bound_QC-variables Al):] is Relation-like non empty set
bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set
bound_in s is Element of bound_QC-variables Al
the_scope_of s is Element of QC-WFF Al
RestrictSub ((bound_in s),s,s) is Relation-like Function-like V34() Element of vSUB Al
ExpandSub ((bound_in s),(the_scope_of s),(RestrictSub ((bound_in s),s,s))) is Relation-like Function-like Element of vSUB Al
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
vSUB Al is functional non empty set
p is Element of CQC-WFF Al
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
QC-Sub-WFF Al is non empty Al -Sub-closed set
bool (QC-Sub-WFF Al) is non empty set
(Al) is Relation-like Function-like V29( CQC-Sub-WFF Al, vSUB Al) Element of bool [:(CQC-Sub-WFF Al),(vSUB Al):]
[:(CQC-Sub-WFF Al),(vSUB Al):] is Relation-like non empty set
bool [:(CQC-Sub-WFF Al),(vSUB Al):] is non empty set
QSub Al is Relation-like Function-like set
(QSub Al) | (CQC-Sub-WFF Al) is Relation-like Function-like set
r is Element of bound_QC-variables Al
All (r,p) is Element of CQC-WFF Al
s is Relation-like Function-like Element of vSUB Al
(Al,(All (r,p)),s) is V15() Element of CQC-Sub-WFF Al
{(All (r,p)),s} is non empty set
{(All (r,p))} is non empty trivial V41(1) set
{{(All (r,p)),s},{(All (r,p))}} is non empty set
(Al) . (Al,(All (r,p)),s) is Relation-like Function-like Element of vSUB Al
(Al,p,((Al) . (Al,(All (r,p)),s))) is V15() Element of CQC-Sub-WFF Al
{p,((Al) . (Al,(All (r,p)),s))} is non empty set
{p} is non empty trivial V41(1) set
{{p,((Al) . (Al,(All (r,p)),s))},{p}} is non empty set
[(Al,p,((Al) . (Al,(All (r,p)),s))),r] is V15() CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
[:(QC-Sub-WFF Al),(bound_QC-variables Al):] is Relation-like non empty set
{(Al,p,((Al) . (Al,(All (r,p)),s))),r} is non empty set
{(Al,p,((Al) . (Al,(All (r,p)),s)))} is Relation-like Function-like constant non empty trivial V41(1) set
{{(Al,p,((Al) . (Al,(All (r,p)),s))),r},{(Al,p,((Al) . (Al,(All (r,p)),s)))}} is non empty set
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
vSUB Al is functional non empty set
s is Relation-like Function-like Element of vSUB Al
p is Element of CQC-WFF Al
r is Element of bound_QC-variables Al
(Al,p,r,s) is CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
QC-Sub-WFF Al is non empty Al -Sub-closed set
[:(QC-Sub-WFF Al),(bound_QC-variables Al):] is Relation-like non empty set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
(Al) is Relation-like Function-like V29( CQC-Sub-WFF Al, vSUB Al) Element of bool [:(CQC-Sub-WFF Al),(vSUB Al):]
[:(CQC-Sub-WFF Al),(vSUB Al):] is Relation-like non empty set
bool [:(CQC-Sub-WFF Al),(vSUB Al):] is non empty set
QSub Al is Relation-like Function-like set
(QSub Al) | (CQC-Sub-WFF Al) is Relation-like Function-like set
All (r,p) is Element of CQC-WFF Al
(Al,(All (r,p)),s) is V15() Element of CQC-Sub-WFF Al
{(All (r,p)),s} is non empty set
{(All (r,p))} is non empty trivial V41(1) set
{{(All (r,p)),s},{(All (r,p))}} is non empty set
(Al) . (Al,(All (r,p)),s) is Relation-like Function-like Element of vSUB Al
(Al,p,((Al) . (Al,(All (r,p)),s))) is V15() Element of CQC-Sub-WFF Al
{p,((Al) . (Al,(All (r,p)),s))} is non empty set
{p} is non empty trivial V41(1) set
{{p,((Al) . (Al,(All (r,p)),s))},{p}} is non empty set
[(Al,p,((Al) . (Al,(All (r,p)),s))),r] is V15() CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
{(Al,p,((Al) . (Al,(All (r,p)),s))),r} is non empty set
{(Al,p,((Al) . (Al,(All (r,p)),s)))} is Relation-like Function-like constant non empty trivial V41(1) set
{{(Al,p,((Al) . (Al,(All (r,p)),s))),r},{(Al,p,((Al) . (Al,(All (r,p)),s)))}} is non empty set
(Al,p,r,s) `1 is Element of CQC-Sub-WFF Al
(Al,((Al,p,r,s) `1)) is Relation-like Function-like Element of vSUB Al
((QSub Al) | (CQC-Sub-WFF Al)) . (Al,(All (r,p)),s) is set
(QSub Al) . (Al,(All (r,p)),s) is set
(Al,p,r,s) `2 is Element of bound_QC-variables Al
((Al,p,r,s) `1) `1 is Element of CQC-WFF Al
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
vSUB Al is functional non empty set
p is Element of CQC-WFF Al
r is Element of bound_QC-variables Al
All (r,p) is Element of CQC-WFF Al
s is Relation-like Function-like Element of vSUB Al
(Al,(All (r,p)),s) is V15() Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
{(All (r,p)),s} is non empty set
{(All (r,p))} is non empty trivial V41(1) set
{{(All (r,p)),s},{(All (r,p))}} is non empty set
(Al,p,r,s) is CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
[:(QC-Sub-WFF Al),(bound_QC-variables Al):] is Relation-like non empty set
(Al) is Relation-like Function-like V29( CQC-Sub-WFF Al, vSUB Al) Element of bool [:(CQC-Sub-WFF Al),(vSUB Al):]
[:(CQC-Sub-WFF Al),(vSUB Al):] is Relation-like non empty set
bool [:(CQC-Sub-WFF Al),(vSUB Al):] is non empty set
QSub Al is Relation-like Function-like set
(QSub Al) | (CQC-Sub-WFF Al) is Relation-like Function-like set
(Al) . (Al,(All (r,p)),s) is Relation-like Function-like Element of vSUB Al
(Al,p,((Al) . (Al,(All (r,p)),s))) is V15() Element of CQC-Sub-WFF Al
{p,((Al) . (Al,(All (r,p)),s))} is non empty set
{p} is non empty trivial V41(1) set
{{p,((Al) . (Al,(All (r,p)),s))},{p}} is non empty set
[(Al,p,((Al) . (Al,(All (r,p)),s))),r] is V15() CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
{(Al,p,((Al) . (Al,(All (r,p)),s))),r} is non empty set
{(Al,p,((Al) . (Al,(All (r,p)),s)))} is Relation-like Function-like constant non empty trivial V41(1) set
{{(Al,p,((Al) . (Al,(All (r,p)),s))),r},{(Al,p,((Al) . (Al,(All (r,p)),s)))}} is non empty set
(Al,p,r,s) is Relation-like Function-like second_Q_comp of (Al,p,r,s)
CQCSub_All ((Al,p,r,s),(Al,p,r,s)) is Element of CQC-Sub-WFF Al
[(Al,p,((Al) . (Al,(All (r,p)),s))),r] `2 is Element of bound_QC-variables Al
[(Al,p,((Al) . (Al,(All (r,p)),s))),r] `1 is Element of CQC-Sub-WFF Al
([(Al,p,((Al) . (Al,(All (r,p)),s))),r] `1) `1 is Element of CQC-WFF Al
proj1 (Al) is set
(Al,([(Al,p,((Al) . (Al,(All (r,p)),s))),r] `1)) is Relation-like Function-like Element of vSUB Al
All (([(Al,p,((Al) . (Al,(All (r,p)),s))),r] `2),(([(Al,p,((Al) . (Al,(All (r,p)),s))),r] `1) `1)) is Element of CQC-WFF Al
(Al,(All (([(Al,p,((Al) . (Al,(All (r,p)),s))),r] `2),(([(Al,p,((Al) . (Al,(All (r,p)),s))),r] `1) `1))),s) is V15() Element of CQC-Sub-WFF Al
{(All (([(Al,p,((Al) . (Al,(All (r,p)),s))),r] `2),(([(Al,p,((Al) . (Al,(All (r,p)),s))),r] `1) `1))),s} is non empty set
{(All (([(Al,p,((Al) . (Al,(All (r,p)),s))),r] `2),(([(Al,p,((Al) . (Al,(All (r,p)),s))),r] `1) `1)))} is non empty trivial V41(1) set
{{(All (([(Al,p,((Al) . (Al,(All (r,p)),s))),r] `2),(([(Al,p,((Al) . (Al,(All (r,p)),s))),r] `1) `1))),s},{(All (([(Al,p,((Al) . (Al,(All (r,p)),s))),r] `2),(([(Al,p,((Al) . (Al,(All (r,p)),s))),r] `1) `1)))}} is non empty set
(QSub Al) . (Al,(All (([(Al,p,((Al) . (Al,(All (r,p)),s))),r] `2),(([(Al,p,((Al) . (Al,(All (r,p)),s))),r] `1) `1))),s) is set
Sub_All ((Al,p,r,s),(Al,p,r,s)) is Element of QC-Sub-WFF Al
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
vSUB Al is functional non empty set
p is Element of CQC-WFF Al
QuantNbr p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r is Element of bound_QC-variables Al
All (r,p) is Element of CQC-WFF Al
QuantNbr (All (r,p)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s is Relation-like Function-like Element of vSUB Al
(Al,(All (r,p)),s) is V15() Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
{(All (r,p)),s} is non empty set
{(All (r,p))} is non empty trivial V41(1) set
{{(All (r,p)),s},{(All (r,p))}} is non empty set
CQC_Sub (Al,(All (r,p)),s) is Element of CQC-WFF Al
QuantNbr (CQC_Sub (Al,(All (r,p)),s)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(Al) is Relation-like Function-like V29( CQC-Sub-WFF Al, vSUB Al) Element of bool [:(CQC-Sub-WFF Al),(vSUB Al):]
[:(CQC-Sub-WFF Al),(vSUB Al):] is Relation-like non empty set
bool [:(CQC-Sub-WFF Al),(vSUB Al):] is non empty set
QSub Al is Relation-like Function-like set
(QSub Al) | (CQC-Sub-WFF Al) is Relation-like Function-like set
(Al) . (Al,(All (r,p)),s) is Relation-like Function-like Element of vSUB Al
(Al,p,((Al) . (Al,(All (r,p)),s))) is V15() Element of CQC-Sub-WFF Al
{p,((Al) . (Al,(All (r,p)),s))} is non empty set
{p} is non empty trivial V41(1) set
{{p,((Al) . (Al,(All (r,p)),s))},{p}} is non empty set
(Al,p,r,s) is CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
[:(QC-Sub-WFF Al),(bound_QC-variables Al):] is Relation-like non empty set
[(Al,p,((Al) . (Al,(All (r,p)),s))),r] is V15() CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
{(Al,p,((Al) . (Al,(All (r,p)),s))),r} is non empty set
{(Al,p,((Al) . (Al,(All (r,p)),s)))} is Relation-like Function-like constant non empty trivial V41(1) set
{{(Al,p,((Al) . (Al,(All (r,p)),s))),r},{(Al,p,((Al) . (Al,(All (r,p)),s)))}} is non empty set
(Al,p,r,s) is Relation-like Function-like second_Q_comp of (Al,p,r,s)
CQCSub_All ((Al,p,r,s),(Al,p,r,s)) is Element of CQC-Sub-WFF Al
@ (CQCSub_All ((Al,p,r,s),(Al,p,r,s))) is Element of [:(QC-WFF Al),(vSUB Al):]
[:(QC-WFF Al),(vSUB Al):] is Relation-like non empty set
S_Bound (@ (CQCSub_All ((Al,p,r,s),(Al,p,r,s)))) is Element of bound_QC-variables Al
Sub_All ((Al,p,r,s),(Al,p,r,s)) is Element of QC-Sub-WFF Al
CQCSub_the_scope_of (Al,(All (r,p)),s) is Element of CQC-Sub-WFF Al
CQC_Sub (CQCSub_the_scope_of (Al,(All (r,p)),s)) is Element of CQC-WFF Al
CQCQuant ((Al,(All (r,p)),s),(CQC_Sub (CQCSub_the_scope_of (Al,(All (r,p)),s)))) is Element of CQC-WFF Al
Sub_the_scope_of (Sub_All ((Al,p,r,s),(Al,p,r,s))) is Element of QC-Sub-WFF Al
[(Al,p,((Al) . (Al,(All (r,p)),s))),r] `1 is Element of CQC-Sub-WFF Al
CQC_Sub (Al,p,((Al) . (Al,(All (r,p)),s))) is Element of CQC-WFF Al
CQCQuant ((CQCSub_All ((Al,p,r,s),(Al,p,r,s))),(CQC_Sub (Al,p,((Al) . (Al,(All (r,p)),s))))) is Element of CQC-WFF Al
All ((S_Bound (@ (CQCSub_All ((Al,p,r,s),(Al,p,r,s))))),(CQC_Sub (Al,p,((Al) . (Al,(All (r,p)),s))))) is Element of CQC-WFF Al
QuantNbr (All ((S_Bound (@ (CQCSub_All ((Al,p,r,s),(Al,p,r,s))))),(CQC_Sub (Al,p,((Al) . (Al,(All (r,p)),s)))))) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
QuantNbr (CQC_Sub (Al,p,((Al) . (Al,(All (r,p)),s)))) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(QuantNbr (CQC_Sub (Al,p,((Al) . (Al,(All (r,p)),s))))) + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(QuantNbr p) + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Al is Relation-like non empty QC-alphabet
vSUB Al is functional non empty set
VERUM Al is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QuantNbr (VERUM Al) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
p is Relation-like Function-like Element of vSUB Al
(Al,(VERUM Al),p) is V15() Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
{(VERUM Al),p} is non empty set
{(VERUM Al)} is non empty trivial V41(1) set
{{(VERUM Al),p},{(VERUM Al)}} is non empty set
CQC_Sub (Al,(VERUM Al),p) is Element of CQC-WFF Al
QuantNbr (CQC_Sub (Al,(VERUM Al),p)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
vSUB Al is functional non empty set
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
QC-pred_symbols Al is non empty set
VERUM Al is Element of CQC-WFF Al
QuantNbr (VERUM Al) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
bool (QC-pred_symbols Al) is non empty set
p is Relation-like Function-like Element of vSUB Al
(Al,(VERUM Al),p) is V15() Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
{(VERUM Al),p} is non empty set
{(VERUM Al)} is non empty trivial V41(1) set
{{(VERUM Al),p},{(VERUM Al)}} is non empty set
CQC_Sub (Al,(VERUM Al),p) is Element of CQC-WFF Al
QuantNbr (CQC_Sub (Al,(VERUM Al),p)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s is Element of r -ary_QC-pred_symbols Al
s is Relation-like bound_QC-variables Al -valued Function-like V41(r) FinSequence-like FinSequence of QC-variables Al
s ! s is Element of CQC-WFF Al
QuantNbr (s ! s) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
m is Relation-like Function-like Element of vSUB Al
(Al,(s ! s),m) is V15() Element of CQC-Sub-WFF Al
{(s ! s),m} is non empty set
{(s ! s)} is non empty trivial V41(1) set
{{(s ! s),m},{(s ! s)}} is non empty set
CQC_Sub (Al,(s ! s),m) is Element of CQC-WFF Al
QuantNbr (CQC_Sub (Al,(s ! s),m)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
m is Element of CQC-WFF Al
QuantNbr m is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
'not' m is Element of CQC-WFF Al
QuantNbr ('not' m) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
l is Relation-like Function-like Element of vSUB Al
(Al,('not' m),l) is V15() Element of CQC-Sub-WFF Al
{('not' m),l} is non empty set
{('not' m)} is non empty trivial V41(1) set
{{('not' m),l},{('not' m)}} is non empty set
CQC_Sub (Al,('not' m),l) is Element of CQC-WFF Al
QuantNbr (CQC_Sub (Al,('not' m),l)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
k is Element of CQC-WFF Al
QuantNbr k is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
j is Element of CQC-WFF Al
QuantNbr j is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
k '&' j is Element of CQC-WFF Al
QuantNbr (k '&' j) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
j1 is Relation-like Function-like Element of vSUB Al
(Al,(k '&' j),j1) is V15() Element of CQC-Sub-WFF Al
{(k '&' j),j1} is non empty set
{(k '&' j)} is non empty trivial V41(1) set
{{(k '&' j),j1},{(k '&' j)}} is non empty set
CQC_Sub (Al,(k '&' j),j1) is Element of CQC-WFF Al
QuantNbr (CQC_Sub (Al,(k '&' j),j1)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
G1 is Element of CQC-WFF Al
QuantNbr G1 is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
H1 is Element of bound_QC-variables Al
All (H1,G1) is Element of CQC-WFF Al
QuantNbr (All (H1,G1)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r is Relation-like Function-like Element of vSUB Al
(Al,(All (H1,G1)),r) is V15() Element of CQC-Sub-WFF Al
{(All (H1,G1)),r} is non empty set
{(All (H1,G1))} is non empty trivial V41(1) set
{{(All (H1,G1)),r},{(All (H1,G1))}} is non empty set
CQC_Sub (Al,(All (H1,G1)),r) is Element of CQC-WFF Al
QuantNbr (CQC_Sub (Al,(All (H1,G1)),r)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-pred_symbols Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
p is Element of CQC-WFF Al
r is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
bool (QC-pred_symbols Al) is non empty set
s is Element of r -ary_QC-pred_symbols Al
s is Relation-like Function-like V41(r) FinSequence-like FinSequence of QC-variables Al
s ! s is Element of QC-WFF Al
len s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
fixed_QC-variables Al is non empty Element of bool (QC-variables Al)
{ (s . b₁) where b₁ is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= len s & s . b₁ in fixed_QC-variables Al ) } is set
free_QC-variables Al is non empty Element of bool (QC-variables Al)
{ (s . b₁) where b₁ is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= len s & s . b₁ in free_QC-variables Al ) } is set
m is Relation-like bound_QC-variables Al -valued Function-like V41(r) FinSequence-like FinSequence of QC-variables Al
s ! m is Element of CQC-WFF Al
F₁() is Relation-like non empty QC-alphabet
QC-WFF F₁() is non empty set
CQC-WFF F₁() is non empty Element of bool (QC-WFF F₁())
bool (QC-WFF F₁()) is non empty set
QC-variables F₁() is non empty set
bound_QC-variables F₁() is non empty Element of bool (QC-variables F₁())
bool (QC-variables F₁()) is non empty set
QC-pred_symbols F₁() is non empty set
VERUM F₁() is Element of CQC-WFF F₁()
Al is Element of bound_QC-variables F₁()
p is Element of CQC-WFF F₁()
QuantNbr p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
All (Al,p) is Element of CQC-WFF F₁()
QuantNbr (All (Al,p)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(QuantNbr p) + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Al is Element of CQC-WFF F₁()
QuantNbr Al is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
p is Element of CQC-WFF F₁()
QuantNbr p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Al '&' p is Element of CQC-WFF F₁()
QuantNbr (Al '&' p) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(QuantNbr Al) + (QuantNbr p) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
QuantNbr (VERUM F₁()) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Al is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Al -ary_QC-pred_symbols F₁() is non empty Element of bool (QC-pred_symbols F₁())
bool (QC-pred_symbols F₁()) is non empty set
r is Element of Al -ary_QC-pred_symbols F₁()
p is Relation-like bound_QC-variables F₁() -valued Function-like V41(Al) FinSequence-like FinSequence of QC-variables F₁()
r ! p is Element of CQC-WFF F₁()
QuantNbr (r ! p) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s is Element of CQC-WFF F₁()
QuantNbr s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
'not' s is Element of CQC-WFF F₁()
QuantNbr ('not' s) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s is Element of CQC-WFF F₁()
QuantNbr s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
m is Element of CQC-WFF F₁()
QuantNbr m is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s '&' m is Element of CQC-WFF F₁()
QuantNbr (s '&' m) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
m is Element of CQC-WFF F₁()
QuantNbr m is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
l is Element of bound_QC-variables F₁()
All (l,m) is Element of CQC-WFF F₁()
QuantNbr (All (l,m)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Al is Element of CQC-WFF F₁()
QuantNbr Al is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
p is Element of QC-WFF Al
r is Element of QC-WFF Al
s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s is Relation-like Function-like FinSequence-like set
len s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s . 1 is set
s . s is set
s is Relation-like Function-like FinSequence-like set
len s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s . 1 is set
s . (len s) is set
s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s . s is set
s + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s . (s + 1) is set
m is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s . m is set
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r is Element of QC-WFF Al
s is Element of QC-WFF Al
s is Relation-like Function-like FinSequence-like (Al,r,s)
len s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s . p is set
(len s) + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(len s) + p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
- 1 is ext-real non positive V28() V32() V33() set
((len s) + 1) + (- 1) is ext-real V28() V32() V33() set
((len s) + p) + (- 1) is ext-real V28() V32() V33() set
- p is ext-real non positive V28() V32() V33() set
(len s) + (- p) is ext-real V28() V32() V33() set
(len s) - 1 is ext-real V28() V32() V33() set
((len s) - 1) + p is ext-real V28() V32() V33() set
(((len s) - 1) + p) + (- p) is ext-real V28() V32() V33() set
p + (- p) is ext-real V28() V32() V33() set
(len s) - p is ext-real V28() V32() V33() set
l is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(len s) - l is ext-real V28() V32() V33() set
s . ((len s) - l) is set
l + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(len s) - (l + 1) is ext-real V28() V32() V33() set
s . ((len s) - (l + 1)) is set
(l + 1) + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
((len s) - 1) + 1 is ext-real V28() V32() V33() set
2 + l is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
- l is ext-real non positive V28() V32() V33() set
(2 + l) + (- l) is ext-real V28() V32() V33() set
(len s) + (- l) is ext-real V28() V32() V33() set
(len s) + l is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
((len s) + l) + (- l) is ext-real V28() V32() V33() set
k is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
k - 1 is ext-real V28() V32() V33() set
1 + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(1 + 1) + (- 1) is ext-real V28() V32() V33() set
k + (- 1) is ext-real V28() V32() V33() set
j is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
j + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s . j is set
s . k is set
G1 is Element of QC-WFF Al
H1 is Element of QC-WFF Al
j1 is Element of QC-WFF Al
G1 is Element of QC-WFF Al
H1 is Element of QC-WFF Al
r is Element of QC-WFF Al
s . (len s) is set
(len s) - 0 is ext-real non negative V28() V32() V33() set
s . ((len s) - 0) is set
m is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(len s) - m is ext-real V28() V32() V33() set
s . ((len s) - m) is set
l is Element of QC-WFF Al
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r is Element of CQC-WFF Al
s is Element of QC-WFF Al
s is Relation-like Function-like FinSequence-like (Al,s,r)
len s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s . p is set
(len s) + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(len s) + p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
- 1 is ext-real non positive V28() V32() V33() set
((len s) + 1) + (- 1) is ext-real V28() V32() V33() set
((len s) + p) + (- 1) is ext-real V28() V32() V33() set
- p is ext-real non positive V28() V32() V33() set
(len s) + (- p) is ext-real V28() V32() V33() set
(len s) - 1 is ext-real V28() V32() V33() set
((len s) - 1) + p is ext-real V28() V32() V33() set
(((len s) - 1) + p) + (- p) is ext-real V28() V32() V33() set
p + (- p) is ext-real V28() V32() V33() set
(len s) - p is ext-real V28() V32() V33() set
l is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(len s) - l is ext-real V28() V32() V33() set
s . ((len s) - l) is set
l + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(len s) - (l + 1) is ext-real V28() V32() V33() set
s . ((len s) - (l + 1)) is set
(l + 1) + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
((len s) - 1) + 1 is ext-real V28() V32() V33() set
2 + l is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
- l is ext-real non positive V28() V32() V33() set
(2 + l) + (- l) is ext-real V28() V32() V33() set
(len s) + (- l) is ext-real V28() V32() V33() set
k is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s . k is set
(len s) + l is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
((len s) + l) + (- l) is ext-real V28() V32() V33() set
k - 1 is ext-real V28() V32() V33() set
1 + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(1 + 1) + (- 1) is ext-real V28() V32() V33() set
k + (- 1) is ext-real V28() V32() V33() set
j1 is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
j1 + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s . j1 is set
j is Element of CQC-WFF Al
G1 is Element of QC-WFF Al
H1 is Element of QC-WFF Al
r is Element of QC-WFF Al
G1 '&' r is Element of QC-WFF Al
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
r is Element of bound_QC-variables Al
All (r,G1) is Element of QC-WFF Al
r is Element of QC-WFF Al
r '&' G1 is Element of QC-WFF Al
'not' G1 is Element of QC-WFF Al
(len s) - 0 is ext-real non negative V28() V32() V33() set
s . ((len s) - 0) is set
m is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(len s) - m is ext-real V28() V32() V33() set
s . ((len s) - m) is set
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s is Element of CQC-WFF Al
s is Element of CQC-WFF Al
QuantNbr s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
m is Relation-like Function-like FinSequence-like (Al,s,s)
len m is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
m . r is set
- r is ext-real non positive V28() V32() V33() set
r + (- r) is ext-real V28() V32() V33() set
(len m) + (- r) is ext-real V28() V32() V33() set
(len m) - r is ext-real V28() V32() V33() set
(len m) + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(len m) + r is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
- 1 is ext-real non positive V28() V32() V33() set
((len m) + 1) + (- 1) is ext-real V28() V32() V33() set
((len m) + r) + (- 1) is ext-real V28() V32() V33() set
(len m) - 1 is ext-real V28() V32() V33() set
((len m) - 1) + r is ext-real V28() V32() V33() set
(((len m) - 1) + r) + (- r) is ext-real V28() V32() V33() set
k is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(len m) - k is ext-real V28() V32() V33() set
m . ((len m) - k) is set
k + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(len m) - (k + 1) is ext-real V28() V32() V33() set
m . ((len m) - (k + 1)) is set
(k + 1) + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
((len m) - 1) + 1 is ext-real V28() V32() V33() set
2 + k is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
- k is ext-real non positive V28() V32() V33() set
(2 + k) + (- k) is ext-real V28() V32() V33() set
(len m) + (- k) is ext-real V28() V32() V33() set
1 + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(1 + 1) + (- 1) is ext-real V28() V32() V33() set
j is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
j + (- 1) is ext-real V28() V32() V33() set
j - 1 is ext-real V28() V32() V33() set
(len m) + k is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
((len m) + k) + (- k) is ext-real V28() V32() V33() set
j1 is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
j1 + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
m . j1 is set
m . j is set
G1 is Element of QC-WFF Al
H1 is Element of QC-WFF Al
q is Element of CQC-WFF Al
QuantNbr q is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
q is Element of CQC-WFF Al
QuantNbr q is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
r is Element of bound_QC-variables Al
All (r,G1) is Element of QC-WFF Al
r is Element of CQC-WFF Al
F is Element of CQC-WFF Al
QuantNbr F is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(QuantNbr F) + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r is Element of QC-WFF Al
r '&' G1 is Element of QC-WFF Al
F is Element of CQC-WFF Al
QuantNbr F is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
p + (QuantNbr F) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
- (QuantNbr F) is ext-real non positive V28() V32() V33() set
p + (- (QuantNbr F)) is ext-real V28() V32() V33() set
(p + (QuantNbr F)) + (- (QuantNbr F)) is ext-real V28() V32() V33() set
r is Element of CQC-WFF Al
QuantNbr r is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(QuantNbr r) + (QuantNbr F) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
((QuantNbr r) + (QuantNbr F)) + (- (QuantNbr F)) is ext-real V28() V32() V33() set
r is Element of QC-WFF Al
G1 '&' r is Element of QC-WFF Al
F is Element of CQC-WFF Al
QuantNbr F is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
p + (QuantNbr F) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
- (QuantNbr F) is ext-real non positive V28() V32() V33() set
p + (- (QuantNbr F)) is ext-real V28() V32() V33() set
(p + (QuantNbr F)) + (- (QuantNbr F)) is ext-real V28() V32() V33() set
r is Element of CQC-WFF Al
QuantNbr r is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(QuantNbr r) + (QuantNbr F) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
((QuantNbr r) + (QuantNbr F)) + (- (QuantNbr F)) is ext-real V28() V32() V33() set
'not' G1 is Element of QC-WFF Al
r is Element of CQC-WFF Al
QuantNbr r is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
F is Element of CQC-WFF Al
QuantNbr F is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
c₁₉ is Element of CQC-WFF Al
QuantNbr c₁₉ is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
c₂₁ is Element of CQC-WFF Al
QuantNbr c₂₁ is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
c₂₃ is Element of CQC-WFF Al
QuantNbr c₂₃ is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
m . (len m) is set
(len m) - 0 is ext-real non negative V28() V32() V33() set
m . ((len m) - 0) is set
l is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(len m) - l is ext-real V28() V32() V33() set
m . ((len m) - l) is set
k is Element of CQC-WFF Al
QuantNbr k is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r is Element of CQC-WFF Al
QuantNbr r is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s is Element of CQC-WFF Al
QuantNbr s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
the Relation-like Function-like FinSequence-like (Al,s,r) is Relation-like Function-like FinSequence-like (Al,s,r)
len the Relation-like Function-like FinSequence-like (Al,s,r) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
the Relation-like Function-like FinSequence-like (Al,s,r) . 1 is set
m is Element of CQC-WFF Al
QuantNbr m is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r is Element of CQC-WFF Al
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
s is Element of bound_QC-variables Al
s is Element of CQC-WFF Al
QuantNbr s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
All (s,s) is Element of CQC-WFF Al
QuantNbr (All (s,s)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
- p is ext-real non positive V28() V32() V33() set
p + (- p) is ext-real V28() V32() V33() set
1 + p is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
(1 + p) + (- p) is ext-real V28() V32() V33() set
s is Element of CQC-WFF Al
QuantNbr s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s is Element of CQC-WFF Al
QuantNbr s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s '&' s is Element of CQC-WFF Al
QuantNbr (s '&' s) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
0 + 0 is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ext-real non positive non negative V21() V22() V23() V25() V26() V27() V28() V32() V33() V34() V39() V41( {} ) Function-yielding V56() Element of NAT
s is Element of CQC-WFF Al
QuantNbr s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
'not' s is Element of CQC-WFF Al
QuantNbr ('not' s) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
QC-pred_symbols Al is non empty set
VERUM Al is Element of CQC-WFF Al
QuantNbr (VERUM Al) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
bool (QC-pred_symbols Al) is non empty set
m is Element of s -ary_QC-pred_symbols Al
s is Relation-like bound_QC-variables Al -valued Function-like V41(s) FinSequence-like FinSequence of QC-variables Al
m ! s is Element of CQC-WFF Al
QuantNbr (m ! s) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
m is Element of CQC-WFF Al
QuantNbr m is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
'not' m is Element of CQC-WFF Al
QuantNbr ('not' m) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
l is Element of CQC-WFF Al
QuantNbr l is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
k is Element of CQC-WFF Al
QuantNbr k is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
l '&' k is Element of CQC-WFF Al
QuantNbr (l '&' k) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
j is Element of CQC-WFF Al
QuantNbr j is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
j1 is Element of bound_QC-variables Al
All (j1,j) is Element of CQC-WFF Al
QuantNbr (All (j1,j)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
QuantNbr r is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
p is Element of CQC-WFF Al
QuantNbr p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r is Element of CQC-WFF Al
QuantNbr r is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s is Element of CQC-WFF Al
QuantNbr s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r '&' s is Element of CQC-WFF Al
QuantNbr (r '&' s) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
0 + 0 is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ext-real non positive non negative V21() V22() V23() V25() V26() V27() V28() V32() V33() V34() V39() V41( {} ) Function-yielding V56() Element of NAT
r is Element of CQC-WFF Al
QuantNbr r is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
'not' r is Element of CQC-WFF Al
QuantNbr ('not' r) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
QC-pred_symbols Al is non empty set
VERUM Al is Element of CQC-WFF Al
QuantNbr (VERUM Al) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
bool (QC-pred_symbols Al) is non empty set
s is Element of r -ary_QC-pred_symbols Al
s is Relation-like bound_QC-variables Al -valued Function-like V41(r) FinSequence-like FinSequence of QC-variables Al
s ! s is Element of CQC-WFF Al
QuantNbr (s ! s) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
m is Element of CQC-WFF Al
QuantNbr m is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
'not' m is Element of CQC-WFF Al
QuantNbr ('not' m) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
m is Element of CQC-WFF Al
QuantNbr m is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
l is Element of CQC-WFF Al
QuantNbr l is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
m '&' l is Element of CQC-WFF Al
QuantNbr (m '&' l) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
k is Element of CQC-WFF Al
QuantNbr k is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
j is Element of bound_QC-variables Al
All (j,k) is Element of CQC-WFF Al
QuantNbr (All (j,k)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
p is Element of CQC-WFF Al
QuantNbr p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
r is Element of bound_QC-variables Al
s is Element of CQC-WFF Al
QuantNbr s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
All (r,s) is Element of CQC-WFF Al
QuantNbr (All (r,s)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
0 + 1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r is Element of CQC-WFF Al
QuantNbr r is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
s is Element of CQC-WFF Al
QuantNbr s is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r '&' s is Element of CQC-WFF Al
QuantNbr (r '&' s) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
0 + 0 is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ext-real non positive non negative V21() V22() V23() V25() V26() V27() V28() V32() V33() V34() V39() V41( {} ) Function-yielding V56() Element of NAT
r is Element of CQC-WFF Al
QuantNbr r is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
'not' r is Element of CQC-WFF Al
QuantNbr ('not' r) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
QC-pred_symbols Al is non empty set
VERUM Al is Element of CQC-WFF Al
QuantNbr (VERUM Al) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
r -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
bool (QC-pred_symbols Al) is non empty set
s is Element of r -ary_QC-pred_symbols Al
s is Relation-like bound_QC-variables Al -valued Function-like V41(r) FinSequence-like FinSequence of QC-variables Al
s ! s is Element of CQC-WFF Al
QuantNbr (s ! s) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
m is Element of CQC-WFF Al
QuantNbr m is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
'not' m is Element of CQC-WFF Al
QuantNbr ('not' m) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
m is Element of CQC-WFF Al
QuantNbr m is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
l is Element of CQC-WFF Al
QuantNbr l is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
m '&' l is Element of CQC-WFF Al
QuantNbr (m '&' l) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
k is Element of CQC-WFF Al
QuantNbr k is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
j is Element of bound_QC-variables Al
All (j,k) is Element of CQC-WFF Al
QuantNbr (All (j,k)) is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
p is Element of CQC-WFF Al
QuantNbr p is ext-real non negative V21() V22() V23() V27() V28() V32() V33() V34() V39() Element of NAT