:: 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

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

{ b

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

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

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

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

l is set

s | { b

@ 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

@ (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

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

QC-WFF F

CQC-WFF F

bool (QC-WFF F

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

QC-WFF F

CQC-WFF F

bool (QC-WFF F

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),(