:: CQC_LANG semantic presentation

REAL is V29() V30() V31() V35() set
NAT is V29() V30() V31() V32() V33() V34() V35() ordinal V43() cardinal limit_cardinal Element of bool REAL
bool REAL is set
NAT is V29() V30() V31() V32() V33() V34() V35() ordinal V43() cardinal limit_cardinal set
bool NAT is V43() set
bool NAT is V43() set
{} is empty V29() V30() V31() V32() V33() V34() V35() ordinal cardinal {} -element set
1 is non empty ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
0 is empty ext-real non positive non negative V29() V30() V31() V32() V33() V34() V35() ordinal natural V43() cardinal {} -element Element of NAT
6 is non empty ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
{6} is non empty trivial V29() V30() V31() V32() V33() V34() 1 -element set
[:{6},NAT:] is V43() set
4 is non empty ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
5 is non empty ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
{4,5} is non empty V29() V30() V31() V32() V33() V34() set
{4} is non empty trivial V29() V30() V31() V32() V33() V34() 1 -element set
{5} is non empty trivial V29() V30() V31() V32() V33() V34() 1 -element set
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
fixed_QC-variables A is non empty Element of bool (QC-variables A)
x is Element of bound_QC-variables A
QC-symbols A is non empty set
[:{4},(QC-symbols A):] is set
p is set
y is set
[p,y] is set
{p,y} is non empty set
{p} is non empty trivial 1 -element set
{{p,y},{p}} is non empty set
[:{5},(QC-symbols A):] is set
p is set
l is set
[p,l] is set
{p,l} is non empty set
{p} is non empty trivial 1 -element set
{{p,l},{p}} is non empty set
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
fixed_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
free_QC-variables A is non empty Element of bool (QC-variables A)
bound_QC-variables A is non empty Element of bool (QC-variables A)
x is set
QC-symbols A is non empty set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
p is set
y is set
[p,y] is set
{p,y} is non empty set
{p} is non empty trivial 1 -element set
{{p,y},{p}} is non empty set
[:{4},(QC-symbols A):] is set
[:{5},(QC-symbols A):] is set
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
free_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
[:(free_QC-variables A),(QC-variables A):] is set
bool [:(free_QC-variables A),(QC-variables A):] is set
x is Relation-like NAT -defined QC-variables A -valued Function-like FinSequence-like FinSequence of QC-variables A
len x is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
p is Relation-like free_QC-variables A -defined QC-variables A -valued Function-like Element of bool [:(free_QC-variables A),(QC-variables A):]
dom p is set
Seg (len x) is V29() V30() V31() V32() V33() V34() Element of bool NAT
y is ext-real ordinal natural V43() cardinal set
x . y is set
p . (x . y) is set
p is set
y is Relation-like Function-like FinSequence-like set
dom y is V29() V30() V31() V32() V33() V34() Element of bool NAT
rng y is set
p is set
l is set
y . l is set
F1 is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
x . F1 is set
y . F1 is set
p . (x . F1) is set
F1 is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
x . F1 is set
y . F1 is set
F1 is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
x . F1 is set
y . F1 is set
p . (x . F1) is set
F1 is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
x . F1 is set
y . F1 is set
p . (x . F1) is set
dom x is V29() V30() V31() V32() V33() V34() Element of bool NAT
p is Relation-like NAT -defined QC-variables A -valued Function-like FinSequence-like FinSequence of QC-variables A
len p is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
l is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
x . l is set
p . l is set
p . (x . l) is set
dom x is V29() V30() V31() V32() V33() V34() Element of bool NAT
y is Relation-like NAT -defined QC-variables A -valued Function-like FinSequence-like FinSequence of QC-variables A
len y is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
p is Relation-like NAT -defined QC-variables A -valued Function-like FinSequence-like FinSequence of QC-variables A
len p is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
l is ext-real ordinal natural V43() cardinal set
x . l is set
y . l is set
p . (x . l) is set
p . l is set
x is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
free_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
[:(free_QC-variables A),(QC-variables A):] is set
bool [:(free_QC-variables A),(QC-variables A):] is set
p is Relation-like NAT -defined QC-variables A -valued Function-like x -element FinSequence-like FinSequence of QC-variables A
y is Relation-like free_QC-variables A -defined QC-variables A -valued Function-like Element of bool [:(free_QC-variables A),(QC-variables A):]
(A,p,y) is Relation-like NAT -defined QC-variables A -valued Function-like FinSequence-like FinSequence of QC-variables A
len (A,p,y) is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
len p is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
free_QC-variables A is non empty Element of bool (QC-variables A)
[:(free_QC-variables A),(QC-variables A):] is set
bool [:(free_QC-variables A),(QC-variables A):] is set
x is Element of bound_QC-variables A
p is Element of free_QC-variables A
p .--> x is Relation-like free_QC-variables A -defined {p} -defined bound_QC-variables A -valued Function-like one-to-one trivial set
{p} is non empty trivial 1 -element set
{p} --> x is Relation-like {p} -defined bound_QC-variables A -valued {x} -valued Function-like constant non empty total V18({p},{x}) Element of bool [:{p},{x}:]
{x} is non empty trivial 1 -element set
[:{p},{x}:] is set
bool [:{p},{x}:] is set
rng (p .--> x) is set
dom (p .--> x) is set
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
free_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
bound_QC-variables A is non empty Element of bool (QC-variables A)
x is Element of free_QC-variables A
p is Element of bound_QC-variables A
x .--> p is Relation-like free_QC-variables A -defined {x} -defined bound_QC-variables A -valued Function-like one-to-one trivial set
{x} is non empty trivial 1 -element set
{x} --> p is Relation-like {x} -defined bound_QC-variables A -valued {p} -valued Function-like constant non empty total V18({x},{p}) Element of bool [:{x},{p}:]
{p} is non empty trivial 1 -element set
[:{x},{p}:] is set
bool [:{x},{p}:] is set
[:(free_QC-variables A),(QC-variables A):] is set
bool [:(free_QC-variables A),(QC-variables A):] is set
A is Relation-like non empty QC-alphabet
free_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
bool (QC-variables A) is set
[:(free_QC-variables A),(QC-variables A):] is set
bool [:(free_QC-variables A),(QC-variables A):] is set
bound_QC-variables A is non empty Element of bool (QC-variables A)
x is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
p is Relation-like free_QC-variables A -defined QC-variables A -valued Function-like Element of bool [:(free_QC-variables A),(QC-variables A):]
y is Element of bound_QC-variables A
p is Element of free_QC-variables A
(A,p,y) is Relation-like free_QC-variables A -defined {p} -defined free_QC-variables A -defined bound_QC-variables A -valued QC-variables A -valued Function-like one-to-one trivial Element of bool [:(free_QC-variables A),(QC-variables A):]
{p} is non empty trivial 1 -element set
{p} --> y is Relation-like {p} -defined bound_QC-variables A -valued {y} -valued Function-like constant non empty total V18({p},{y}) Element of bool [:{p},{y}:]
{y} is non empty trivial 1 -element set
[:{p},{y}:] is set
bool [:{p},{y}:] is set
F1 is Relation-like NAT -defined QC-variables A -valued Function-like FinSequence-like FinSequence of QC-variables A
l is Relation-like NAT -defined QC-variables A -valued Function-like FinSequence-like FinSequence of QC-variables A
(A,l,p) is Relation-like NAT -defined QC-variables A -valued Function-like FinSequence-like FinSequence of QC-variables A
len l is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
l . x is set
F1 . x is set
(A,p,y) . p is set
dom (A,p,y) is set
dom (A,p,y) is set
A is Relation-like non empty QC-alphabet
QC-WFF A is non empty set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
bool (QC-WFF A) is set
p is set
y is Element of QC-WFF A
Fixed y is Element of bool (fixed_QC-variables A)
fixed_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
bool (QC-variables A) is set
bool (fixed_QC-variables A) is set
Free y is Element of bool (free_QC-variables A)
free_QC-variables A is non empty Element of bool (QC-variables A)
bool (free_QC-variables A) is set
A is Relation-like non empty QC-alphabet
(A) is Element of bool (QC-WFF A)
QC-WFF A is non empty set
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
VERUM A is Element of QC-WFF A
Fixed (VERUM A) is Element of bool (fixed_QC-variables A)
fixed_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
bool (QC-variables A) is set
bool (fixed_QC-variables A) is set
Free (VERUM A) is Element of bool (free_QC-variables A)
free_QC-variables A is non empty Element of bool (QC-variables A)
bool (free_QC-variables A) is set
A is Relation-like non empty QC-alphabet
QC-WFF A is non empty set
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
x is Element of QC-WFF A
Fixed x is Element of bool (fixed_QC-variables A)
fixed_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
bool (QC-variables A) is set
bool (fixed_QC-variables A) is set
Free x is Element of bool (free_QC-variables A)
free_QC-variables A is non empty Element of bool (QC-variables A)
bool (free_QC-variables A) is set
p is Element of QC-WFF A
Fixed p is Element of bool (fixed_QC-variables A)
Free p is Element of bool (free_QC-variables A)
x is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
QC-symbols A is non empty set
y is Element of QC-symbols A
x. y is Element of bound_QC-variables A
x |-> (x. y) is Relation-like NAT -defined bound_QC-variables A -valued Function-like x -element FinSequence-like Element of x -tuples_on (bound_QC-variables A)
x -tuples_on (bound_QC-variables A) is functional non empty FinSequence-membered FinSequenceSet of bound_QC-variables A
(bound_QC-variables A) * is functional FinSequence-membered FinSequenceSet of bound_QC-variables A
{ b₁ where b₁ is Relation-like NAT -defined bound_QC-variables A -valued Function-like FinSequence-like Element of (bound_QC-variables A) * : len b₁ = x } is set
Seg x is V29() V30() V31() V32() V33() V34() Element of bool NAT
(Seg x) --> (x. y) is Relation-like Seg x -defined Seg x -defined bound_QC-variables A -valued {(x. y)} -valued Function-like constant total total V18( Seg x,{(x. y)}) FinSequence-like Element of bool [:(Seg x),{(x. y)}:]
{(x. y)} is non empty trivial 1 -element set
[:(Seg x),{(x. y)}:] is set
bool [:(Seg x),{(x. y)}:] is set
dom (x |-> (x. y)) is V29() V30() V31() V32() V33() V34() x -element Element of bool NAT
rng (x |-> (x. y)) is set
l is set
F1 is set
(x |-> (x. y)) . F1 is set
l is Relation-like NAT -defined QC-variables A -valued Function-like x -element FinSequence-like FinSequence of QC-variables A
F1 is set
rng l is set
dom l is V29() V30() V31() V32() V33() V34() x -element Element of bool NAT
ll is set
l . ll is set
F2 is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
l . F2 is set
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
free_QC-variables A is non empty Element of bool (QC-variables A)
fixed_QC-variables A is non empty Element of bool (QC-variables A)
x is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
p is Relation-like NAT -defined QC-variables A -valued Function-like x -element FinSequence-like FinSequence of QC-variables A
len p is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
{ (p . b₁) where b₁ is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len p & p . b₁ in free_QC-variables A ) } is set
{ (p . b₁) where b₁ is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len p & p . b₁ in fixed_QC-variables A ) } is set
the Element of { (p . b₁) where b₁ is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len p & p . b₁ in free_QC-variables A ) } is Element of { (p . b₁) where b₁ is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len p & p . b₁ in free_QC-variables A ) }
l is Relation-like NAT -defined QC-variables A -valued bound_QC-variables A -valued Function-like x -element FinSequence-like FinSequence of QC-variables A
len l is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
ll is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
l . ll is set
dom l is V29() V30() V31() V32() V33() V34() x -element Element of bool NAT
rng l is set
the Element of { (p . b₁) where b₁ is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len p & p . b₁ in fixed_QC-variables A ) } is Element of { (p . b₁) where b₁ is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len p & p . b₁ in fixed_QC-variables A ) }
ll is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
l . ll is set
l is set
rng p is set
dom p is V29() V30() V31() V32() V33() V34() x -element Element of bool NAT
F1 is set
p . F1 is set
ll is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
p . ll is set
A is Relation-like non empty QC-alphabet
VERUM A is Element of QC-WFF A
QC-WFF A is non empty set
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
Fixed (VERUM A) is Element of bool (fixed_QC-variables A)
fixed_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
bool (QC-variables A) is set
bool (fixed_QC-variables A) is set
Free (VERUM A) is Element of bool (free_QC-variables A)
free_QC-variables A is non empty Element of bool (QC-variables A)
bool (free_QC-variables A) is set
A is Relation-like non empty QC-alphabet
QC-pred_symbols A is non empty set
QC-variables A is non empty set
QC-WFF A is non empty set
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
free_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
fixed_QC-variables A is non empty Element of bool (QC-variables A)
x is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
x -ary_QC-pred_symbols A is non empty Element of bool (QC-pred_symbols A)
bool (QC-pred_symbols A) is set
p is Element of x -ary_QC-pred_symbols A
y is Relation-like NAT -defined QC-variables A -valued Function-like x -element FinSequence-like FinSequence of QC-variables A
p ! y is Element of QC-WFF A
len y is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
{ (y . b₁) where b₁ is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len y & y . b₁ in free_QC-variables A ) } is set
{ (y . b₁) where b₁ is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len y & y . b₁ in fixed_QC-variables A ) } is set
Free (p ! y) is Element of bool (free_QC-variables A)
bool (free_QC-variables A) is set
Fixed (p ! y) is Element of bool (fixed_QC-variables A)
bool (fixed_QC-variables A) is set
x is Relation-like non empty QC-alphabet
QC-pred_symbols x is non empty set
A is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
A -ary_QC-pred_symbols x is non empty Element of bool (QC-pred_symbols x)
bool (QC-pred_symbols x) is set
bound_QC-variables x is non empty Element of bool (QC-variables x)
QC-variables x is non empty set
bool (QC-variables x) is set
p is Element of A -ary_QC-pred_symbols x
y is Relation-like NAT -defined bound_QC-variables x -valued QC-variables x -valued Function-like A -element FinSequence-like FinSequence of QC-variables x
p ! y is Element of QC-WFF x
QC-WFF x is non empty set
(x) is non empty Element of bool (QC-WFF x)
bool (QC-WFF x) is set
{ b₁ where b₁ is Element of QC-WFF x : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
len y is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
fixed_QC-variables x is non empty Element of bool (QC-variables x)
{ (y . b₁) where b₁ is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len y & y . b₁ in fixed_QC-variables x ) } is set
free_QC-variables x is non empty Element of bool (QC-variables x)
{ (y . b₁) where b₁ is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len y & y . b₁ in free_QC-variables x ) } is set
A is Relation-like non empty QC-alphabet
QC-WFF A is non empty set
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
x is Element of QC-WFF A
'not' x is Element of QC-WFF A
Free ('not' x) is Element of bool (free_QC-variables A)
free_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
bool (QC-variables A) is set
bool (free_QC-variables A) is set
Free x is Element of bool (free_QC-variables A)
Fixed ('not' x) is Element of bool (fixed_QC-variables A)
fixed_QC-variables A is non empty Element of bool (QC-variables A)
bool (fixed_QC-variables A) is set
Fixed x is Element of bool (fixed_QC-variables A)
p is Element of (A)
Fixed p is Element of bool (fixed_QC-variables A)
fixed_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
bool (QC-variables A) is set
bool (fixed_QC-variables A) is set
'not' p is Element of QC-WFF A
Fixed ('not' p) is Element of bool (fixed_QC-variables A)
Free p is Element of bool (free_QC-variables A)
free_QC-variables A is non empty Element of bool (QC-variables A)
bool (free_QC-variables A) is set
Free ('not' p) is Element of bool (free_QC-variables A)
A is Relation-like non empty QC-alphabet
QC-WFF A is non empty set
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
x is Element of QC-WFF A
p is Element of QC-WFF A
x '&' p is Element of QC-WFF A
Fixed (x '&' p) is Element of bool (fixed_QC-variables A)
fixed_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
bool (QC-variables A) is set
bool (fixed_QC-variables A) is set
Fixed x is Element of bool (fixed_QC-variables A)
Fixed p is Element of bool (fixed_QC-variables A)
(Fixed x) \/ (Fixed p) is Element of bool (fixed_QC-variables A)
Free (x '&' p) is Element of bool (free_QC-variables A)
free_QC-variables A is non empty Element of bool (QC-variables A)
bool (free_QC-variables A) is set
Free x is Element of bool (free_QC-variables A)
Free p is Element of bool (free_QC-variables A)
(Free x) \/ (Free p) is Element of bool (free_QC-variables A)
y is Element of (A)
Fixed y is Element of bool (fixed_QC-variables A)
fixed_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
bool (QC-variables A) is set
bool (fixed_QC-variables A) is set
p is Element of (A)
Fixed p is Element of bool (fixed_QC-variables A)
(Fixed y) \/ (Fixed p) is Element of bool (fixed_QC-variables A)
y '&' p is Element of QC-WFF A
Fixed (y '&' p) is Element of bool (fixed_QC-variables A)
Free y is Element of bool (free_QC-variables A)
free_QC-variables A is non empty Element of bool (QC-variables A)
bool (free_QC-variables A) is set
Free p is Element of bool (free_QC-variables A)
(Free y) \/ (Free p) is Element of bool (free_QC-variables A)
Free (y '&' p) is Element of bool (free_QC-variables A)
A is Relation-like non empty QC-alphabet
VERUM A is Element of QC-WFF A
QC-WFF A is non empty set
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
x is Element of (A)
'not' x is Element of QC-WFF A
p is Element of (A)
x '&' p is Element of QC-WFF A
A is Relation-like non empty QC-alphabet
QC-WFF A is non empty set
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
x is Element of (A)
p is Element of (A)
x => p is Element of QC-WFF A
(A,p) is Element of (A)
(A,x,(A,p)) is Element of (A)
(A,(A,x,(A,p))) is Element of (A)
A is Relation-like non empty QC-alphabet
QC-WFF A is non empty set
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
x is Element of (A)
p is Element of (A)
x 'or' p is Element of QC-WFF A
(A,x) is Element of (A)
(A,p) is Element of (A)
(A,(A,x),(A,p)) is Element of (A)
(A,(A,(A,x),(A,p))) is Element of (A)
A is Relation-like non empty QC-alphabet
QC-WFF A is non empty set
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
x is Element of (A)
p is Element of (A)
x <=> p is Element of QC-WFF A
x => p is Element of QC-WFF A
p => x is Element of QC-WFF A
(x => p) '&' (p => x) is Element of QC-WFF A
(A,p) is Element of (A)
(A,x,(A,p)) is Element of (A)
(A,(A,x,(A,p))) is Element of (A)
(A,(A,x,(A,p))) '&' (p => x) is Element of QC-WFF A
(A,x) is Element of (A)
(A,p,(A,x)) is Element of (A)
(A,(A,p,(A,x))) is Element of (A)
(A,(A,(A,x,(A,p))),(A,(A,p,(A,x)))) is Element of (A)
A is Relation-like non empty QC-alphabet
QC-WFF A is non empty set
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
x is Element of (A)
p is Element of (A)
x => p is Element of QC-WFF A
x 'or' p is Element of QC-WFF A
x <=> p is Element of QC-WFF A
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
QC-WFF A is non empty set
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
x is Element of bound_QC-variables A
p is Element of QC-WFF A
All (x,p) is Element of QC-WFF A
Fixed (All (x,p)) is Element of bool (fixed_QC-variables A)
fixed_QC-variables A is non empty Element of bool (QC-variables A)
bool (fixed_QC-variables A) is set
Fixed p is Element of bool (fixed_QC-variables A)
Free (All (x,p)) is Element of bool (free_QC-variables A)
free_QC-variables A is non empty Element of bool (QC-variables A)
bool (free_QC-variables A) is set
Free p is Element of bool (free_QC-variables A)
Fixed p is Element of bool (fixed_QC-variables A)
fixed_QC-variables A is non empty Element of bool (QC-variables A)
bool (fixed_QC-variables A) is set
Fixed (All (x,p)) is Element of bool (fixed_QC-variables A)
Free p is Element of bool (free_QC-variables A)
free_QC-variables A is non empty Element of bool (QC-variables A)
bool (free_QC-variables A) is set
Free (All (x,p)) is Element of bool (free_QC-variables A)
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
QC-WFF A is non empty set
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
x is Element of bound_QC-variables A
p is Element of (A)
All (x,p) is Element of QC-WFF A
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
QC-WFF A is non empty set
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
x is Element of bound_QC-variables A
p is Element of (A)
Ex (x,p) is Element of QC-WFF A
(A,p) is Element of (A)
(A,x,(A,p)) is Element of (A)
(A,(A,x,(A,p))) is Element of (A)
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
QC-WFF A is non empty set
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
x is Element of bound_QC-variables A
p is Element of (A)
Ex (x,p) is Element of QC-WFF A
F₁() is Relation-like non empty QC-alphabet
QC-WFF F₁() is non empty set
(F₁()) is non empty Element of bool (QC-WFF F₁())
bool (QC-WFF F₁()) is set
{ b₁ where b₁ is Element of QC-WFF F₁() : ( Fixed b₁ = {} & Free b₁ = {} ) } is 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 set
QC-pred_symbols F₁() is non empty set
(F₁()) is Element of (F₁())
A is Element of QC-WFF F₁()
'not' A is Element of QC-WFF F₁()
A is Element of QC-WFF F₁()
x is Element of QC-WFF F₁()
A '&' x is Element of QC-WFF F₁()
A is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
A -ary_QC-pred_symbols F₁() is non empty Element of bool (QC-pred_symbols F₁())
bool (QC-pred_symbols F₁()) is set
x is Element of A -ary_QC-pred_symbols F₁()
p is Relation-like NAT -defined QC-variables F₁() -valued Function-like A -element FinSequence-like FinSequence of QC-variables F₁()
x ! p is Element of QC-WFF F₁()
len p is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
fixed_QC-variables F₁() is non empty Element of bool (QC-variables F₁())
{ (p . b₁) where b₁ is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len p & p . b₁ in fixed_QC-variables F₁() ) } is set
free_QC-variables F₁() is non empty Element of bool (QC-variables F₁())
{ (p . b₁) where b₁ is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len p & p . b₁ in free_QC-variables F₁() ) } is set
A is Element of bound_QC-variables F₁()
x is Element of QC-WFF F₁()
All (A,x) is Element of QC-WFF F₁()
A is Element of (F₁())
F₂() is non empty set
F₁() is Relation-like non empty QC-alphabet
(F₁()) is non empty Element of bool (QC-WFF F₁())
QC-WFF F₁() is non empty set
bool (QC-WFF F₁()) is set
{ b₁ where b₁ is Element of QC-WFF F₁() : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
[:(F₁()),F₂():] is set
bool [:(F₁()),F₂():] is set
(F₁()) is Element of (F₁())
F₃() is Element of F₂()
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 set
QC-pred_symbols F₁() is non empty set
[:(QC-WFF F₁()),F₂():] is set
bool [:(QC-WFF F₁()),F₂():] is set
A is Relation-like QC-WFF F₁() -defined F₂() -valued Function-like V18( QC-WFF F₁(),F₂()) Element of bool [:(QC-WFF F₁()),F₂():]
A . (F₁()) is Element of F₂()
A | (F₁()) is Relation-like QC-WFF F₁() -defined F₂() -valued Function-like Element of bool [:(QC-WFF F₁()),F₂():]
x is Relation-like (F₁()) -defined F₂() -valued Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
x . (F₁()) is Element of F₂()
p is Element of (F₁())
(F₁(),p) is Element of (F₁())
x . (F₁(),p) is Element of F₂()
x . p is Element of F₂()
F₅((x . p)) is Element of F₂()
y is Element of (F₁())
(F₁(),p,y) is Element of (F₁())
x . (F₁(),p,y) is Element of F₂()
x . y is Element of F₂()
F₆((x . p),(x . y)) is Element of F₂()
p is Element of bound_QC-variables F₁()
(F₁(),p,p) is Element of (F₁())
x . (F₁(),p,p) is Element of F₂()
F₇(p,(x . p)) is Element of F₂()
l is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
l -ary_QC-pred_symbols F₁() is non empty Element of bool (QC-pred_symbols F₁())
bool (QC-pred_symbols F₁()) is set
F1 is Relation-like NAT -defined QC-variables F₁() -valued bound_QC-variables F₁() -valued Function-like l -element FinSequence-like FinSequence of QC-variables F₁()
ll is Element of l -ary_QC-pred_symbols F₁()
(l,F₁(),ll,F1) is Element of (F₁())
x . (l,F₁(),ll,F1) is Element of F₂()
F₄(l,ll,F1) is Element of F₂()
the_arity_of ll is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
the_arguments_of (l,F₁(),ll,F1) is Relation-like NAT -defined QC-variables F₁() -valued Function-like FinSequence-like FinSequence of QC-variables F₁()
the_pred_symbol_of (l,F₁(),ll,F1) is Element of QC-pred_symbols F₁()
A . (l,F₁(),ll,F1) is Element of F₂()
A . p is Element of F₂()
the_left_argument_of (F₁(),p,y) is Element of QC-WFF F₁()
the_right_argument_of (F₁(),p,y) is Element of QC-WFF F₁()
the_argument_of (F₁(),p) is Element of QC-WFF F₁()
A . (F₁(),p) is Element of F₂()
A . y is Element of F₂()
A . (F₁(),p,y) is Element of F₂()
bound_in (F₁(),p,p) is Element of bound_QC-variables F₁()
the_scope_of (F₁(),p,p) is Element of QC-WFF F₁()
A . (F₁(),p,p) is Element of F₂()
F₁() is Relation-like non empty QC-alphabet
(F₁()) is non empty Element of bool (QC-WFF F₁())
QC-WFF F₁() is non empty set
bool (QC-WFF F₁()) is set
{ b₁ where b₁ is Element of QC-WFF F₁() : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
F₂() is non empty set
[:(F₁()),F₂():] is set
bool [:(F₁()),F₂():] is set
F₃() is Relation-like (F₁()) -defined F₂() -valued Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
(F₁()) is Element of (F₁())
F₃() . (F₁()) is Element of F₂()
F₅() is Element of F₂()
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 set
QC-pred_symbols F₁() is non empty set
F₄() is Relation-like (F₁()) -defined F₂() -valued Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
F₄() . (F₁()) is Element of F₂()
F₃() . (F₁()) is set
F₄() . (F₁()) is set
A is Element of (F₁())
F₃() . A is set
F₄() . A is set
(F₁(),A) is Element of (F₁())
F₃() . (F₁(),A) is set
F₄() . (F₁(),A) is set
x is Element of (F₁())
F₃() . x is set
F₄() . x is set
(F₁(),A,x) is Element of (F₁())
F₃() . (F₁(),A,x) is set
F₄() . (F₁(),A,x) is set
p is Element of bound_QC-variables F₁()
(F₁(),p,A) is Element of (F₁())
F₃() . (F₁(),p,A) is set
F₄() . (F₁(),p,A) is set
y is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
y -ary_QC-pred_symbols F₁() is non empty Element of bool (QC-pred_symbols F₁())
bool (QC-pred_symbols F₁()) is set
p is Relation-like NAT -defined QC-variables F₁() -valued bound_QC-variables F₁() -valued Function-like y -element FinSequence-like FinSequence of QC-variables F₁()
l is Element of y -ary_QC-pred_symbols F₁()
(y,F₁(),l,p) is Element of (F₁())
F₃() . (y,F₁(),l,p) is set
F₄() . (y,F₁(),l,p) is set
F₃() . (y,F₁(),l,p) is Element of F₂()
F₆(y,l,p) is Element of F₂()
F₄() . (y,F₁(),l,p) is Element of F₂()
F₃() . (F₁(),A) is Element of F₂()
F₃() . A is Element of F₂()
F₇((F₃() . A)) is Element of F₂()
F₄() . A is Element of F₂()
F₄() . (F₁(),A) is Element of F₂()
F₃() . (F₁(),A,x) is Element of F₂()
F₃() . x is Element of F₂()
F₈((F₃() . A),(F₃() . x)) is Element of F₂()
F₄() . x is Element of F₂()
F₄() . (F₁(),A,x) is Element of F₂()
F₃() . (F₁(),p,A) is Element of F₂()
F₉(p,(F₃() . A)) is Element of F₂()
F₁() is Relation-like non empty QC-alphabet
QC-WFF F₁() is non empty set
(F₁()) is non empty Element of bool (QC-WFF F₁())
bool (QC-WFF F₁()) is set
{ b₁ where b₁ is Element of QC-WFF F₁() : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
F₂() is non empty set
[:(F₁()),F₂():] is set
bool [:(F₁()),F₂():] is set
F₃() is Element of (F₁())
(F₁()) is Element of (F₁())
F₄() is Element of F₂()
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 set
QC-pred_symbols F₁() is non empty set
A is Relation-like (F₁()) -defined F₂() -valued Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
A . (F₁()) is Element of F₂()
A . F₃() is Element of F₂()
x is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
x -ary_QC-pred_symbols F₁() is non empty Element of bool (QC-pred_symbols F₁())
bool (QC-pred_symbols F₁()) is set
y is Element of x -ary_QC-pred_symbols F₁()
p is Relation-like NAT -defined QC-variables F₁() -valued bound_QC-variables F₁() -valued Function-like x -element FinSequence-like FinSequence of QC-variables F₁()
(x,F₁(),y,p) is Element of (F₁())
A . (x,F₁(),y,p) is Element of F₂()
F₅(x,y,p) is Element of F₂()
p is Element of (F₁())
(F₁(),p) is Element of (F₁())
A . (F₁(),p) is Element of F₂()
A . p is Element of F₂()
F₆((A . p)) is Element of F₂()
l is Element of (F₁())
F1 is Element of (F₁())
(F₁(),l,F1) is Element of (F₁())
A . (F₁(),l,F1) is Element of F₂()
A . l is Element of F₂()
A . F1 is Element of F₂()
F₇((A . l),(A . F1)) is Element of F₂()
F2 is Element of bound_QC-variables F₁()
ll is Element of (F₁())
(F₁(),F2,ll) is Element of (F₁())
A . (F₁(),F2,ll) is Element of F₂()
A . ll is Element of F₂()
F₈(F2,(A . ll)) is Element of F₂()
A is Element of F₂()
x is Element of F₂()
p is Relation-like (F₁()) -defined F₂() -valued Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
p . F₃() is Element of F₂()
p . (F₁()) is Element of F₂()
y is Relation-like (F₁()) -defined F₂() -valued Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
y . F₃() is Element of F₂()
y . (F₁()) is Element of F₂()
F₂() is non empty set
F₁() is Relation-like non empty QC-alphabet
QC-WFF F₁() is non empty set
(F₁()) is non empty Element of bool (QC-WFF F₁())
bool (QC-WFF F₁()) is set
{ b₁ where b₁ is Element of QC-WFF F₁() : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
[:(F₁()),F₂():] is set
bool [:(F₁()),F₂():] is set
(F₁()) is Element of (F₁())
F₄() is Element of F₂()
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 set
QC-pred_symbols F₁() is non empty set
F₃((F₁())) is Element of F₂()
A is Relation-like (F₁()) -defined F₂() -valued Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
A . (F₁()) is Element of F₂()
F₂() is non empty set
F₁() is Relation-like non empty QC-alphabet
QC-pred_symbols F₁() is non empty set
F₆() is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
F₆() -ary_QC-pred_symbols F₁() is non empty Element of bool (QC-pred_symbols F₁())
bool (QC-pred_symbols F₁()) is set
bound_QC-variables F₁() is non empty Element of bool (QC-variables F₁())
QC-variables F₁() is non empty set
bool (QC-variables F₁()) is set
QC-WFF F₁() is non empty set
(F₁()) is non empty Element of bool (QC-WFF F₁())
bool (QC-WFF F₁()) is set
{ b₁ where b₁ is Element of QC-WFF F₁() : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
[:(F₁()),F₂():] is set
bool [:(F₁()),F₂():] is set
(F₁()) is Element of (F₁())
F₃() is Element of F₂()
F₇() is Element of F₆() -ary_QC-pred_symbols F₁()
F₈() is Relation-like NAT -defined bound_QC-variables F₁() -valued QC-variables F₁() -valued Function-like F₆() -element FinSequence-like FinSequence of QC-variables F₁()
(F₆(),F₁(),F₇(),F₈()) is Element of (F₁())
F₄((F₆(),F₁(),F₇(),F₈())) is Element of F₂()
F₅(F₆(),F₇(),F₈()) is Element of F₂()
A is Relation-like (F₁()) -defined F₂() -valued Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
A . (F₁()) is Element of F₂()
A . (F₆(),F₁(),F₇(),F₈()) is Element of F₂()
F₂() is non empty set
F₁() is Relation-like non empty QC-alphabet
QC-WFF F₁() is non empty set
(F₁()) is non empty Element of bool (QC-WFF F₁())
bool (QC-WFF F₁()) is set
{ b₁ where b₁ is Element of QC-WFF F₁() : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
[:(F₁()),F₂():] is set
bool [:(F₁()),F₂():] is set
(F₁()) is Element of (F₁())
F₄() is Element of F₂()
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 set
QC-pred_symbols F₁() is non empty set
F₇() is Element of (F₁())
(F₁(),F₇()) is Element of (F₁())
F₃((F₁(),F₇())) is Element of F₂()
F₃(F₇()) is Element of F₂()
F₆(F₃(F₇())) is Element of F₂()
A is Relation-like (F₁()) -defined F₂() -valued Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
A . F₇() is Element of F₂()
A . (F₁()) is Element of F₂()
x is Relation-like (F₁()) -defined F₂() -valued Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
x . (F₁()) is Element of F₂()
x . (F₁(),F₇()) is Element of F₂()
x . F₇() is Element of F₂()
F₆((x . F₇())) is Element of F₂()
F₂() is non empty set
F₁() is Relation-like non empty QC-alphabet
QC-WFF F₁() is non empty set
(F₁()) is non empty Element of bool (QC-WFF F₁())
bool (QC-WFF F₁()) is set
{ b₁ where b₁ is Element of QC-WFF F₁() : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
[:(F₁()),F₂():] is set
bool [:(F₁()),F₂():] is set
(F₁()) is Element of (F₁())
F₄() is Element of F₂()
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 set
QC-pred_symbols F₁() is non empty set
F₈() is Element of (F₁())
F₉() is Element of (F₁())
(F₁(),F₈(),F₉()) is Element of (F₁())
F₃((F₁(),F₈(),F₉())) is Element of F₂()
F₃(F₈()) is Element of F₂()
F₃(F₉()) is Element of F₂()
F₇(F₃(F₈()),F₃(F₉())) is Element of F₂()
A is Relation-like (F₁()) -defined F₂() -valued Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
A . F₉() is Element of F₂()
A . (F₁()) is Element of F₂()
x is Relation-like (F₁()) -defined F₂() -valued Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
x . F₈() is Element of F₂()
x . (F₁()) is Element of F₂()
p is Relation-like (F₁()) -defined F₂() -valued Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
p . (F₁()) is Element of F₂()
p . (F₁(),F₈(),F₉()) is Element of F₂()
p . F₈() is Element of F₂()
p . F₉() is Element of F₂()
F₇((p . F₈()),(p . F₉())) is Element of F₂()
F₂() is non empty set
F₁() is Relation-like non empty QC-alphabet
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 set
QC-WFF F₁() is non empty set
(F₁()) is non empty Element of bool (QC-WFF F₁())
bool (QC-WFF F₁()) is set
{ b₁ where b₁ is Element of QC-WFF F₁() : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
[:(F₁()),F₂():] is set
bool [:(F₁()),F₂():] is set
(F₁()) is Element of (F₁())
F₄() is Element of F₂()
QC-pred_symbols F₁() is non empty set
F₉() is Element of bound_QC-variables F₁()
F₁₀() is Element of (F₁())
(F₁(),F₉(),F₁₀()) is Element of (F₁())
F₃((F₁(),F₉(),F₁₀())) is Element of F₂()
F₃(F₁₀()) is Element of F₂()
F₈(F₉(),F₃(F₁₀())) is Element of F₂()
A is Relation-like (F₁()) -defined F₂() -valued Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
A . F₁₀() is Element of F₂()
A . (F₁()) is Element of F₂()
x is Relation-like (F₁()) -defined F₂() -valued Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
x . (F₁()) is Element of F₂()
x . (F₁(),F₉(),F₁₀()) is Element of F₂()
x . F₁₀() is Element of F₂()
F₈(F₉(),(x . F₁₀())) is Element of F₂()
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
QC-WFF A is non empty set
[:(QC-WFF A),(QC-WFF A):] is set
bool [:(QC-WFF A),(QC-WFF A):] is set
(A) is Element of (A)
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
A a. 0 is Element of free_QC-variables A
free_QC-variables A is non empty Element of bool (QC-variables A)
x is Element of bound_QC-variables A
(A,(A a. 0),x) is Relation-like free_QC-variables A -defined {(A a. 0)} -defined free_QC-variables A -defined bound_QC-variables A -valued QC-variables A -valued Function-like one-to-one trivial Element of bool [:(free_QC-variables A),(QC-variables A):]
{(A a. 0)} is non empty trivial 1 -element set
[:(free_QC-variables A),(QC-variables A):] is set
bool [:(free_QC-variables A),(QC-variables A):] is set
{(A a. 0)} --> x is Relation-like {(A a. 0)} -defined bound_QC-variables A -valued {x} -valued Function-like constant non empty total V18({(A a. 0)},{x}) Element of bool [:{(A a. 0)},{x}:]
{x} is non empty trivial 1 -element set
[:{(A a. 0)},{x}:] is set
bool [:{(A a. 0)},{x}:] is set
p is Relation-like QC-WFF A -defined QC-WFF A -valued Function-like V18( QC-WFF A, QC-WFF A) Element of bool [:(QC-WFF A),(QC-WFF A):]
p . (A) is Element of QC-WFF A
y is Relation-like QC-WFF A -defined QC-WFF A -valued Function-like V18( QC-WFF A, QC-WFF A) Element of bool [:(QC-WFF A),(QC-WFF A):]
y . (A) is Element of QC-WFF A
p is Element of QC-WFF A
p . p is Element of QC-WFF A
l is Element of QC-WFF A
p . l is Element of QC-WFF A
the_pred_symbol_of l is Element of QC-pred_symbols A
QC-pred_symbols A is non empty set
the_arguments_of l is Relation-like NAT -defined QC-variables A -valued Function-like FinSequence-like FinSequence of QC-variables A
(A,(the_arguments_of l),(A,(A a. 0),x)) is Relation-like NAT -defined QC-variables A -valued Function-like FinSequence-like FinSequence of QC-variables A
(the_pred_symbol_of l) ! (A,(the_arguments_of l),(A,(A a. 0),x)) is Element of QC-WFF A
F1 is Element of QC-WFF A
ll is Element of QC-WFF A
the_argument_of F1 is Element of QC-WFF A
p . (the_argument_of F1) is Element of QC-WFF A
p . F1 is Element of QC-WFF A
'not' ll is Element of QC-WFF A
F2 is Element of QC-WFF A
y is Element of QC-WFF A
the_left_argument_of F2 is Element of QC-WFF A
p . (the_left_argument_of F2) is Element of QC-WFF A
i is Element of QC-WFF A
the_right_argument_of F2 is Element of QC-WFF A
p . (the_right_argument_of F2) is Element of QC-WFF A
p . F2 is Element of QC-WFF A
y '&' i is Element of QC-WFF A
c₁₂ is Element of QC-WFF A
c₁₃ is Element of QC-WFF A
the_scope_of c₁₂ is Element of QC-WFF A
p . (the_scope_of c₁₂) is Element of QC-WFF A
p . c₁₂ is Element of QC-WFF A
bound_in c₁₂ is Element of bound_QC-variables A
All ((bound_in c₁₂),c₁₃) is Element of QC-WFF A
IFEQ ((bound_in c₁₂),x,c₁₂,(All ((bound_in c₁₂),c₁₃))) is Element of QC-WFF A
p is Element of QC-WFF A
y . p is Element of QC-WFF A
l is Element of QC-WFF A
y . l is Element of QC-WFF A
the_pred_symbol_of l is Element of QC-pred_symbols A
QC-pred_symbols A is non empty set
the_arguments_of l is Relation-like NAT -defined QC-variables A -valued Function-like FinSequence-like FinSequence of QC-variables A
(A,(the_arguments_of l),(A,(A a. 0),x)) is Relation-like NAT -defined QC-variables A -valued Function-like FinSequence-like FinSequence of QC-variables A
(the_pred_symbol_of l) ! (A,(the_arguments_of l),(A,(A a. 0),x)) is Element of QC-WFF A
F1 is Element of QC-WFF A
ll is Element of QC-WFF A
the_argument_of F1 is Element of QC-WFF A
y . (the_argument_of F1) is Element of QC-WFF A
y . F1 is Element of QC-WFF A
'not' ll is Element of QC-WFF A
F2 is Element of QC-WFF A
y is Element of QC-WFF A
the_left_argument_of F2 is Element of QC-WFF A
y . (the_left_argument_of F2) is Element of QC-WFF A
i is Element of QC-WFF A
the_right_argument_of F2 is Element of QC-WFF A
y . (the_right_argument_of F2) is Element of QC-WFF A
y . F2 is Element of QC-WFF A
y '&' i is Element of QC-WFF A
c₁₂ is Element of QC-WFF A
c₁₃ is Element of QC-WFF A
the_scope_of c₁₂ is Element of QC-WFF A
y . (the_scope_of c₁₂) is Element of QC-WFF A
y . c₁₂ is Element of QC-WFF A
bound_in c₁₂ is Element of bound_QC-variables A
All ((bound_in c₁₂),c₁₃) is Element of QC-WFF A
IFEQ ((bound_in c₁₂),x,c₁₂,(All ((bound_in c₁₂),c₁₃))) is Element of QC-WFF A
A is Relation-like non empty QC-alphabet
QC-WFF A is non empty set
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
[:(QC-WFF A),(QC-WFF A):] is set
bool [:(QC-WFF A),(QC-WFF A):] is set
x is Element of QC-WFF A
(A) is Element of (A)
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
A a. 0 is Element of free_QC-variables A
free_QC-variables A is non empty Element of bool (QC-variables A)
p is Element of bound_QC-variables A
(A,(A a. 0),p) is Relation-like free_QC-variables A -defined {(A a. 0)} -defined free_QC-variables A -defined bound_QC-variables A -valued QC-variables A -valued Function-like one-to-one trivial Element of bool [:(free_QC-variables A),(QC-variables A):]
{(A a. 0)} is non empty trivial 1 -element set
[:(free_QC-variables A),(QC-variables A):] is set
bool [:(free_QC-variables A),(QC-variables A):] is set
{(A a. 0)} --> p is Relation-like {(A a. 0)} -defined bound_QC-variables A -valued {p} -valued Function-like constant non empty total V18({(A a. 0)},{p}) Element of bool [:{(A a. 0)},{p}:]
{p} is non empty trivial 1 -element set
[:{(A a. 0)},{p}:] is set
bool [:{(A a. 0)},{p}:] is set
y is Relation-like QC-WFF A -defined QC-WFF A -valued Function-like V18( QC-WFF A, QC-WFF A) Element of bool [:(QC-WFF A),(QC-WFF A):]
y . (A) is Element of QC-WFF A
y . x is Element of QC-WFF A
p is Element of QC-WFF A
y . p is Element of QC-WFF A
the_pred_symbol_of p is Element of QC-pred_symbols A
QC-pred_symbols A is non empty set
the_arguments_of p is Relation-like NAT -defined QC-variables A -valued Function-like FinSequence-like FinSequence of QC-variables A
(A,(the_arguments_of p),(A,(A a. 0),p)) is Relation-like NAT -defined QC-variables A -valued Function-like FinSequence-like FinSequence of QC-variables A
(the_pred_symbol_of p) ! (A,(the_arguments_of p),(A,(A a. 0),p)) is Element of QC-WFF A
l is Element of QC-WFF A
y . l is Element of QC-WFF A
the_argument_of l is Element of QC-WFF A
y . (the_argument_of l) is Element of QC-WFF A
'not' (y . (the_argument_of l)) is Element of QC-WFF A
F1 is Element of QC-WFF A
y . F1 is Element of QC-WFF A
the_left_argument_of F1 is Element of QC-WFF A
y . (the_left_argument_of F1) is Element of QC-WFF A
the_right_argument_of F1 is Element of QC-WFF A
y . (the_right_argument_of F1) is Element of QC-WFF A
(y . (the_left_argument_of F1)) '&' (y . (the_right_argument_of F1)) is Element of QC-WFF A
ll is Element of QC-WFF A
y . ll is Element of QC-WFF A
bound_in ll is Element of bound_QC-variables A
the_scope_of ll is Element of QC-WFF A
y . (the_scope_of ll) is Element of QC-WFF A
All ((bound_in ll),(y . (the_scope_of ll))) is Element of QC-WFF A
IFEQ ((bound_in ll),p,ll,(All ((bound_in ll),(y . (the_scope_of ll))))) is Element of QC-WFF A
y is Element of QC-WFF A
l is Relation-like QC-WFF A -defined QC-WFF A -valued Function-like V18( QC-WFF A, QC-WFF A) Element of bool [:(QC-WFF A),(QC-WFF A):]
l . x is Element of QC-WFF A
l . (A) is Element of QC-WFF A
p is Element of QC-WFF A
F1 is Relation-like QC-WFF A -defined QC-WFF A -valued Function-like V18( QC-WFF A, QC-WFF A) Element of bool [:(QC-WFF A),(QC-WFF A):]
F1 . x is Element of QC-WFF A
F1 . (A) is Element of QC-WFF A
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
(A) is Element of (A)
QC-WFF A is non empty set
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
x is Element of bound_QC-variables A
(A,(A),x) is Element of QC-WFF A
[:(QC-WFF A),(QC-WFF A):] is set
bool [:(QC-WFF A),(QC-WFF A):] is set
A a. 0 is Element of free_QC-variables A
free_QC-variables A is non empty Element of bool (QC-variables A)
(A,(A a. 0),x) is Relation-like free_QC-variables A -defined {(A a. 0)} -defined free_QC-variables A -defined bound_QC-variables A -valued QC-variables A -valued Function-like one-to-one trivial Element of bool [:(free_QC-variables A),(QC-variables A):]
{(A a. 0)} is non empty trivial 1 -element set
[:(free_QC-variables A),(QC-variables A):] is set
bool [:(free_QC-variables A),(QC-variables A):] is set
{(A a. 0)} --> x is Relation-like {(A a. 0)} -defined bound_QC-variables A -valued {x} -valued Function-like constant non empty total V18({(A a. 0)},{x}) Element of bool [:{(A a. 0)},{x}:]
{x} is non empty trivial 1 -element set
[:{(A a. 0)},{x}:] is set
bool [:{(A a. 0)},{x}:] is set
p is Relation-like QC-WFF A -defined QC-WFF A -valued Function-like V18( QC-WFF A, QC-WFF A) Element of bool [:(QC-WFF A),(QC-WFF A):]
p . (A) is Element of QC-WFF A
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
QC-WFF A is non empty set
A a. 0 is Element of free_QC-variables A
free_QC-variables A is non empty Element of bool (QC-variables A)
x is Element of bound_QC-variables A
(A,(A a. 0),x) is Relation-like free_QC-variables A -defined {(A a. 0)} -defined free_QC-variables A -defined bound_QC-variables A -valued QC-variables A -valued Function-like one-to-one trivial Element of bool [:(free_QC-variables A),(QC-variables A):]
{(A a. 0)} is non empty trivial 1 -element set
[:(free_QC-variables A),(QC-variables A):] is set
bool [:(free_QC-variables A),(QC-variables A):] is set
{(A a. 0)} --> x is Relation-like {(A a. 0)} -defined bound_QC-variables A -valued {x} -valued Function-like constant non empty total V18({(A a. 0)},{x}) Element of bool [:{(A a. 0)},{x}:]
{x} is non empty trivial 1 -element set
[:{(A a. 0)},{x}:] is set
bool [:{(A a. 0)},{x}:] is set
p is Element of QC-WFF A
(A,p,x) is Element of QC-WFF A
the_pred_symbol_of p is Element of QC-pred_symbols A
QC-pred_symbols A is non empty set
the_arguments_of p is Relation-like NAT -defined QC-variables A -valued Function-like FinSequence-like FinSequence of QC-variables A
(A,(the_arguments_of p),(A,(A a. 0),x)) is Relation-like NAT -defined QC-variables A -valued Function-like FinSequence-like FinSequence of QC-variables A
(the_pred_symbol_of p) ! (A,(the_arguments_of p),(A,(A a. 0),x)) is Element of QC-WFF A
[:(QC-WFF A),(QC-WFF A):] is set
bool [:(QC-WFF A),(QC-WFF A):] is set
(A) is Element of (A)
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
y is Relation-like QC-WFF A -defined QC-WFF A -valued Function-like V18( QC-WFF A, QC-WFF A) Element of bool [:(QC-WFF A),(QC-WFF A):]
y . p is Element of QC-WFF A
y . (A) is Element of QC-WFF A
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
QC-pred_symbols A is non empty set
A a. 0 is Element of free_QC-variables A
free_QC-variables A is non empty Element of bool (QC-variables A)
x is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
x -ary_QC-pred_symbols A is non empty Element of bool (QC-pred_symbols A)
bool (QC-pred_symbols A) is set
p is Element of bound_QC-variables A
(A,(A a. 0),p) is Relation-like free_QC-variables A -defined {(A a. 0)} -defined free_QC-variables A -defined bound_QC-variables A -valued QC-variables A -valued Function-like one-to-one trivial Element of bool [:(free_QC-variables A),(QC-variables A):]
{(A a. 0)} is non empty trivial 1 -element set
[:(free_QC-variables A),(QC-variables A):] is set
bool [:(free_QC-variables A),(QC-variables A):] is set
{(A a. 0)} --> p is Relation-like {(A a. 0)} -defined bound_QC-variables A -valued {p} -valued Function-like constant non empty total V18({(A a. 0)},{p}) Element of bool [:{(A a. 0)},{p}:]
{p} is non empty trivial 1 -element set
[:{(A a. 0)},{p}:] is set
bool [:{(A a. 0)},{p}:] is set
y is Element of x -ary_QC-pred_symbols A
p is Relation-like NAT -defined QC-variables A -valued Function-like x -element FinSequence-like FinSequence of QC-variables A
y ! p is Element of QC-WFF A
QC-WFF A is non empty set
(A,(y ! p),p) is Element of QC-WFF A
(A,p,(A,(A a. 0),p)) is Relation-like NAT -defined QC-variables A -valued Function-like x -element FinSequence-like FinSequence of QC-variables A
y ! (A,p,(A,(A a. 0),p)) is Element of QC-WFF A
the_arguments_of (y ! p) is Relation-like NAT -defined QC-variables A -valued Function-like FinSequence-like FinSequence of QC-variables A
the_pred_symbol_of (y ! p) is Element of QC-pred_symbols A
l is Element of QC-pred_symbols A
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
p is Element of QC-WFF A
(A,p,x) is Element of QC-WFF A
the_argument_of p is Element of QC-WFF A
(A,(the_argument_of p),x) is Element of QC-WFF A
'not' (A,(the_argument_of p),x) is Element of QC-WFF A
[:(QC-WFF A),(QC-WFF A):] is set
bool [:(QC-WFF A),(QC-WFF A):] is set
(A) is Element of (A)
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
A a. 0 is Element of free_QC-variables A
free_QC-variables A is non empty Element of bool (QC-variables A)
(A,(A a. 0),x) is Relation-like free_QC-variables A -defined {(A a. 0)} -defined free_QC-variables A -defined bound_QC-variables A -valued QC-variables A -valued Function-like one-to-one trivial Element of bool [:(free_QC-variables A),(QC-variables A):]
{(A a. 0)} is non empty trivial 1 -element set
[:(free_QC-variables A),(QC-variables A):] is set
bool [:(free_QC-variables A),(QC-variables A):] is set
{(A a. 0)} --> x is Relation-like {(A a. 0)} -defined bound_QC-variables A -valued {x} -valued Function-like constant non empty total V18({(A a. 0)},{x}) Element of bool [:{(A a. 0)},{x}:]
{x} is non empty trivial 1 -element set
[:{(A a. 0)},{x}:] is set
bool [:{(A a. 0)},{x}:] is set
y is Relation-like QC-WFF A -defined QC-WFF A -valued Function-like V18( QC-WFF A, QC-WFF A) Element of bool [:(QC-WFF A),(QC-WFF A):]
y . p is Element of QC-WFF A
y . (A) is Element of QC-WFF A
p is Relation-like QC-WFF A -defined QC-WFF A -valued Function-like V18( QC-WFF A, QC-WFF A) Element of bool [:(QC-WFF A),(QC-WFF A):]
p . (the_argument_of p) is Element of QC-WFF A
p . (A) is Element of QC-WFF A
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
p is Element of QC-WFF A
'not' p is Element of QC-WFF A
(A,('not' p),x) is Element of QC-WFF A
(A,p,x) is Element of QC-WFF A
'not' (A,p,x) is Element of QC-WFF A
the_argument_of ('not' p) is Element of QC-WFF A
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
p is Element of QC-WFF A
(A,p,x) is Element of QC-WFF A
the_left_argument_of p is Element of QC-WFF A
(A,(the_left_argument_of p),x) is Element of QC-WFF A
the_right_argument_of p is Element of QC-WFF A
(A,(the_right_argument_of p),x) is Element of QC-WFF A
(A,(the_left_argument_of p),x) '&' (A,(the_right_argument_of p),x) is Element of QC-WFF A
[:(QC-WFF A),(QC-WFF A):] is set
bool [:(QC-WFF A),(QC-WFF A):] is set
(A) is Element of (A)
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
A a. 0 is Element of free_QC-variables A
free_QC-variables A is non empty Element of bool (QC-variables A)
(A,(A a. 0),x) is Relation-like free_QC-variables A -defined {(A a. 0)} -defined free_QC-variables A -defined bound_QC-variables A -valued QC-variables A -valued Function-like one-to-one trivial Element of bool [:(free_QC-variables A),(QC-variables A):]
{(A a. 0)} is non empty trivial 1 -element set
[:(free_QC-variables A),(QC-variables A):] is set
bool [:(free_QC-variables A),(QC-variables A):] is set
{(A a. 0)} --> x is Relation-like {(A a. 0)} -defined bound_QC-variables A -valued {x} -valued Function-like constant non empty total V18({(A a. 0)},{x}) Element of bool [:{(A a. 0)},{x}:]
{x} is non empty trivial 1 -element set
[:{(A a. 0)},{x}:] is set
bool [:{(A a. 0)},{x}:] is set
y is Relation-like QC-WFF A -defined QC-WFF A -valued Function-like V18( QC-WFF A, QC-WFF A) Element of bool [:(QC-WFF A),(QC-WFF A):]
y . p is Element of QC-WFF A
y . (A) is Element of QC-WFF A
p is Relation-like QC-WFF A -defined QC-WFF A -valued Function-like V18( QC-WFF A, QC-WFF A) Element of bool [:(QC-WFF A),(QC-WFF A):]
p . (the_right_argument_of p) is Element of QC-WFF A
p . (A) is Element of QC-WFF A
l is Relation-like QC-WFF A -defined QC-WFF A -valued Function-like V18( QC-WFF A, QC-WFF A) Element of bool [:(QC-WFF A),(QC-WFF A):]
l . (the_left_argument_of p) is Element of QC-WFF A
l . (A) is Element of QC-WFF A
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
p is Element of QC-WFF A
(A,p,x) is Element of QC-WFF A
y is Element of QC-WFF A
p '&' y is Element of QC-WFF A
(A,(p '&' y),x) is Element of QC-WFF A
(A,y,x) is Element of QC-WFF A
(A,p,x) '&' (A,y,x) is Element of QC-WFF A
the_left_argument_of (p '&' y) is Element of QC-WFF A
the_right_argument_of (p '&' y) is Element of QC-WFF A
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
p is Element of QC-WFF A
(A,p,x) is Element of QC-WFF A
bound_in p is Element of bound_QC-variables A
the_scope_of p is Element of QC-WFF A
(A,(the_scope_of p),x) is Element of QC-WFF A
All ((bound_in p),(A,(the_scope_of p),x)) is Element of QC-WFF A
IFEQ ((bound_in p),x,p,(All ((bound_in p),(A,(the_scope_of p),x)))) is Element of QC-WFF A
[:(QC-WFF A),(QC-WFF A):] is set
bool [:(QC-WFF A),(QC-WFF A):] is set
(A) is Element of (A)
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
A a. 0 is Element of free_QC-variables A
free_QC-variables A is non empty Element of bool (QC-variables A)
(A,(A a. 0),x) is Relation-like free_QC-variables A -defined {(A a. 0)} -defined free_QC-variables A -defined bound_QC-variables A -valued QC-variables A -valued Function-like one-to-one trivial Element of bool [:(free_QC-variables A),(QC-variables A):]
{(A a. 0)} is non empty trivial 1 -element set
[:(free_QC-variables A),(QC-variables A):] is set
bool [:(free_QC-variables A),(QC-variables A):] is set
{(A a. 0)} --> x is Relation-like {(A a. 0)} -defined bound_QC-variables A -valued {x} -valued Function-like constant non empty total V18({(A a. 0)},{x}) Element of bool [:{(A a. 0)},{x}:]
{x} is non empty trivial 1 -element set
[:{(A a. 0)},{x}:] is set
bool [:{(A a. 0)},{x}:] is set
y is Relation-like QC-WFF A -defined QC-WFF A -valued Function-like V18( QC-WFF A, QC-WFF A) Element of bool [:(QC-WFF A),(QC-WFF A):]
y . p is Element of QC-WFF A
y . (A) is Element of QC-WFF A
p is Relation-like QC-WFF A -defined QC-WFF A -valued Function-like V18( QC-WFF A, QC-WFF A) Element of bool [:(QC-WFF A),(QC-WFF A):]
p . (the_scope_of p) is Element of QC-WFF A
p . (A) is Element of QC-WFF A
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
p is Element of QC-WFF A
bound_in p is Element of bound_QC-variables A
(A,p,x) is Element of QC-WFF A
the_scope_of p is Element of QC-WFF A
(A,(the_scope_of p),x) is Element of QC-WFF A
All ((bound_in p),(A,(the_scope_of p),x)) is Element of QC-WFF A
IFEQ ((bound_in p),x,p,(All ((bound_in p),(A,(the_scope_of p),x)))) is Element of QC-WFF A
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
p is Element of QC-WFF A
bound_in p is Element of bound_QC-variables A
(A,p,x) is Element of QC-WFF A
the_scope_of p is Element of QC-WFF A
(A,(the_scope_of p),x) is Element of QC-WFF A
All ((bound_in p),(A,(the_scope_of p),x)) is Element of QC-WFF A
IFEQ ((bound_in p),x,p,(All ((bound_in p),(A,(the_scope_of p),x)))) is Element of QC-WFF A
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
p is Element of QC-WFF A
All (x,p) is Element of QC-WFF A
(A,(All (x,p)),x) is Element of QC-WFF A
bound_in (All (x,p)) is Element of bound_QC-variables A
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
p is Element of bound_QC-variables A
y is Element of QC-WFF A
All (x,y) is Element of QC-WFF A
(A,(All (x,y)),p) is Element of QC-WFF A
(A,y,p) is Element of QC-WFF A
All (x,(A,y,p)) is Element of QC-WFF A
the_scope_of (All (x,y)) is Element of QC-WFF A
bound_in (All (x,y)) is Element of bound_QC-variables A
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
p is Element of QC-WFF A
Free p is Element of bool (free_QC-variables A)
free_QC-variables A is non empty Element of bool (QC-variables A)
bool (free_QC-variables A) is set
(A,p,x) is Element of QC-WFF A
y is Element of QC-WFF A
Free y is Element of bool (free_QC-variables A)
(A,y,x) is Element of QC-WFF A
'not' y is Element of QC-WFF A
Free ('not' y) is Element of bool (free_QC-variables A)
(A,('not' y),x) is Element of QC-WFF A
y is Element of QC-WFF A
Free y is Element of bool (free_QC-variables A)
(A,y,x) is Element of QC-WFF A
p is Element of QC-WFF A
Free p is Element of bool (free_QC-variables A)
(A,p,x) is Element of QC-WFF A
y '&' p is Element of QC-WFF A
Free (y '&' p) is Element of bool (free_QC-variables A)
(A,(y '&' p),x) is Element of QC-WFF A
(Free y) \/ (Free p) is Element of bool (free_QC-variables A)
QC-pred_symbols A is non empty set
y is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
y -ary_QC-pred_symbols A is non empty Element of bool (QC-pred_symbols A)
bool (QC-pred_symbols A) is set
p is Element of y -ary_QC-pred_symbols A
l is Relation-like NAT -defined QC-variables A -valued Function-like y -element FinSequence-like FinSequence of QC-variables A
p ! l is Element of QC-WFF A
Free (p ! l) is Element of bool (free_QC-variables A)
(A,(p ! l),x) is Element of QC-WFF A
F1 is ext-real ordinal natural V43() cardinal set
len l is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
l . F1 is set
A a. 0 is Element of free_QC-variables A
{ (l . b₁) where b₁ is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len l & l . b₁ in free_QC-variables A ) } is set
(A,(A a. 0),x) is Relation-like free_QC-variables A -defined {(A a. 0)} -defined free_QC-variables A -defined bound_QC-variables A -valued QC-variables A -valued Function-like one-to-one trivial Element of bool [:(free_QC-variables A),(QC-variables A):]
{(A a. 0)} is non empty trivial 1 -element set
[:(free_QC-variables A),(QC-variables A):] is set
bool [:(free_QC-variables A),(QC-variables A):] is set
{(A a. 0)} --> x is Relation-like {(A a. 0)} -defined bound_QC-variables A -valued {x} -valued Function-like constant non empty total V18({(A a. 0)},{x}) Element of bool [:{(A a. 0)},{x}:]
{x} is non empty trivial 1 -element set
[:{(A a. 0)},{x}:] is set
bool [:{(A a. 0)},{x}:] is set
(A,l,(A,(A a. 0),x)) is Relation-like NAT -defined QC-variables A -valued Function-like y -element FinSequence-like FinSequence of QC-variables A
(A,l,(A,(A a. 0),x)) . F1 is set
len (A,l,(A,(A a. 0),x)) is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
y is Element of bound_QC-variables A
p is Element of QC-WFF A
Free p is Element of bool (free_QC-variables A)
(A,p,x) is Element of QC-WFF A
All (y,p) is Element of QC-WFF A
Free (All (y,p)) is Element of bool (free_QC-variables A)
(A,(All (y,p)),x) is Element of QC-WFF A
(A) is Element of (A)
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
Free (A) is Element of bool (free_QC-variables A)
(A,(A),x) is Element of QC-WFF A
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
QC-WFF A is non empty set
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
x is Element of bound_QC-variables A
p is Element of (A)
(A,p,x) is Element of QC-WFF A
Free p is Element of bool (free_QC-variables A)
free_QC-variables A is non empty Element of bool (QC-variables A)
bool (free_QC-variables A) is set
A is Relation-like non empty QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
p is Element of QC-WFF A
(A,p,x) is Element of QC-WFF A
Fixed (A,p,x) is Element of bool (fixed_QC-variables A)
fixed_QC-variables A is non empty Element of bool (QC-variables A)
bool (fixed_QC-variables A) is set
Fixed p is Element of bool (fixed_QC-variables A)
y is Element of QC-WFF A
(A,y,x) is Element of QC-WFF A
Fixed (A,y,x) is Element of bool (fixed_QC-variables A)
Fixed y is Element of bool (fixed_QC-variables A)
'not' y is Element of QC-WFF A
(A,('not' y),x) is Element of QC-WFF A
Fixed (A,('not' y),x) is Element of bool (fixed_QC-variables A)
Fixed ('not' y) is Element of bool (fixed_QC-variables A)
'not' (A,y,x) is Element of QC-WFF A
Fixed ('not' (A,y,x)) is Element of bool (fixed_QC-variables A)
y is Element of QC-WFF A
(A,y,x) is Element of QC-WFF A
Fixed (A,y,x) is Element of bool (fixed_QC-variables A)
Fixed y is Element of bool (fixed_QC-variables A)
p is Element of QC-WFF A
(A,p,x) is Element of QC-WFF A
Fixed (A,p,x) is Element of bool (fixed_QC-variables A)
Fixed p is Element of bool (fixed_QC-variables A)
y '&' p is Element of QC-WFF A
(A,(y '&' p),x) is Element of QC-WFF A
Fixed (A,(y '&' p),x) is Element of bool (fixed_QC-variables A)
Fixed (y '&' p) is Element of bool (fixed_QC-variables A)
(A,y,x) '&' (A,p,x) is Element of QC-WFF A
Fixed ((A,y,x) '&' (A,p,x)) is Element of bool (fixed_QC-variables A)
(Fixed y) \/ (Fixed p) is Element of bool (fixed_QC-variables A)
QC-pred_symbols A is non empty set
y is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
y -ary_QC-pred_symbols A is non empty Element of bool (QC-pred_symbols A)
bool (QC-pred_symbols A) is set
p is Element of y -ary_QC-pred_symbols A
l is Relation-like NAT -defined QC-variables A -valued Function-like y -element FinSequence-like FinSequence of QC-variables A
p ! l is Element of QC-WFF A
(A,(p ! l),x) is Element of QC-WFF A
Fixed (A,(p ! l),x) is Element of bool (fixed_QC-variables A)
Fixed (p ! l) is Element of bool (fixed_QC-variables A)
len l is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
{ (l . b₁) where b₁ is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len l & l . b₁ in fixed_QC-variables A ) } is set
A a. 0 is Element of free_QC-variables A
free_QC-variables A is non empty Element of bool (QC-variables A)
(A,(A a. 0),x) is Relation-like free_QC-variables A -defined {(A a. 0)} -defined free_QC-variables A -defined bound_QC-variables A -valued QC-variables A -valued Function-like one-to-one trivial Element of bool [:(free_QC-variables A),(QC-variables A):]
{(A a. 0)} is non empty trivial 1 -element set
[:(free_QC-variables A),(QC-variables A):] is set
bool [:(free_QC-variables A),(QC-variables A):] is set
{(A a. 0)} --> x is Relation-like {(A a. 0)} -defined bound_QC-variables A -valued {x} -valued Function-like constant non empty total V18({(A a. 0)},{x}) Element of bool [:{(A a. 0)},{x}:]
{x} is non empty trivial 1 -element set
[:{(A a. 0)},{x}:] is set
bool [:{(A a. 0)},{x}:] is set
(A,l,(A,(A a. 0),x)) is Relation-like NAT -defined QC-variables A -valued Function-like y -element FinSequence-like FinSequence of QC-variables A
len (A,l,(A,(A a. 0),x)) is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
{ ((A,l,(A,(A a. 0),x)) . b₁) where b₁ is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (A,l,(A,(A a. 0),x)) & (A,l,(A,(A a. 0),x)) . b₁ in fixed_QC-variables A ) } is set
y is set
i is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
l . i is set
(A,l,(A,(A a. 0),x)) . i is set
i is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT
(A,l,(A,(A a. 0),x)) . i is set
l . i is set
p ! (A,l,(A,(A a. 0),x)) is Element of QC-WFF A
Fixed (p ! (A,l,(A,(A a. 0),x))) is Element of bool (fixed_QC-variables A)
y is Element of bound_QC-variables A
p is Element of QC-WFF A
(A,p,x) is Element of QC-WFF A
Fixed (A,p,x) is Element of bool (fixed_QC-variables A)
Fixed p is Element of bool (fixed_QC-variables A)
All (y,p) is Element of QC-WFF A
(A,(All (y,p)),x) is Element of QC-WFF A
Fixed (A,(All (y,p)),x) is Element of bool (fixed_QC-variables A)
Fixed (All (y,p)) is Element of bool (fixed_QC-variables A)
All (y,(A,p,x)) is Element of QC-WFF A
Fixed (All (y,(A,p,x))) is Element of bool (fixed_QC-variables A)
(A) is Element of (A)
(A) is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is set
{ b₁ where b₁ is Element of QC-WFF A : ( Fixed b₁ = {} & Free b₁ = {} ) } is set
(A,(A),x) is Element of QC-WFF A
Fixed (A,(A),x) is Element of bool (fixed_QC-variables A)
Fixed (A) is Element of bool (fixed_QC-variables A)
A is set
x is set
p is set
(A,x) :-> p is Relation-like [:{A},{x}:] -defined {p} -valued Function-like V18([:{A},{x}:],{p}) Element of bool [:[:{A},{x}:],{p}:]
{A} is non empty trivial 1 -element set
{x} is non empty trivial 1 -element set
[:{A},{x}:] is set
{p} is non empty trivial 1 -element set
[:[:{A},{x}:],{p}:] is set
bool [:[:{A},{x}:],{p}:] is set
[A,x] is set
{A,x} is non empty set
{{A,x},{A}} is non empty set
{[A,x]} is non empty trivial 1 -element set
{[A,x]} --> p is Relation-like {[A,x]} -defined {p} -valued Function-like constant non empty total V18({[A,x]},{p}) Element of bool [:{[A,x]},{p}:]
[:{[A,x]},{p}:] is set
bool [:{[A,x]},{p}:] is set
[A,x] .--> p is Relation-like {[A,x]} -defined Function-like one-to-one trivial set
A is set
x is set
p is set
(A,x) :-> p is Relation-like [:{A},{x}:] -defined {p} -valued Function-like V18([:{A},{x}:],{p}) Element of bool [:[:{A},{x}:],{p}:]
{A} is non empty trivial 1 -element set
{x} is non empty trivial 1 -element set
[:{A},{x}:] is set
{p} is non empty trivial 1 -element set
[:[:{A},{x}:],{p}:] is set
bool [:[:{A},{x}:],{p}:] is set
[A,x] is set
{A,x} is non empty set
{{A,x},{A}} is non empty set
{[A,x]} is non empty trivial 1 -element set
{[A,x]} --> p is Relation-like {[A,x]} -defined {p} -valued Function-like constant non empty total V18({[A,x]},{p}) Element of bool [:{[A,x]},{p}:]
[:{[A,x]},{p}:] is set
bool [:{[A,x]},{p}:] is set
((A,x) :-> p) . (A,x) is set
A is set
x is set
p is set
(A,A) --> (x,p) is Relation-like Function-like set
A .--> p is Relation-like {A} -defined Function-like one-to-one trivial set
{A} is non empty trivial 1 -element set
{A} --> p is Relation-like {A} -defined {p} -valued Function-like constant non empty total V18({A},{p}) Element of bool [:{A},{p}:]
{p} is non empty trivial 1 -element set
[:{A},{p}:] is set
bool [:{A},{p}:] is set
x is set
y is set
A is Relation-like Function-like set
p is set
x .--> p is Relation-like {x} -defined Function-like one-to-one trivial set
{x} is non empty trivial 1 -element set
{x} --> p is Relation-like {x} -defined {p} -valued Function-like constant non empty total V18({x},{p}) Element of bool [:{x},{p}:]
{p} is non empty trivial 1 -element set
[:{x},{p}:] is set
bool [:{x},{p}:] is set
A +* (x .--> p) is Relation-like Function-like set
(A +* (x .--> p)) . y is set
A . y is set
x is set
p is set
A is Relation-like Function-like set
y is set
p is set
(x,p) --> (y,p) is Relation-like Function-like set
A +* ((x,p) --> (y,p)) is Relation-like Function-like set
(A +* ((x,p) --> (y,p))) . x is set
(A +* ((x,p) --> (y,p))) . p is set