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

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

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

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

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

{ (p . b

the Element of { (p . b

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

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

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

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

{ (y . b

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

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

free_QC-variables x is non empty Element of bool (QC-variables x)

{ (y . b

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

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

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

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

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

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

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

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

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

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

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

x is Element of bound_QC-variables A

p is Element of (A)

Ex (x,p) is Element of QC-WFF A

F

QC-WFF F

(F

bool (QC-WFF F

{ b

QC-variables F

bound_QC-variables F

bool (QC-variables F

QC-pred_symbols F

(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

bool (QC-pred_symbols F

x is Element of A -ary_QC-pred_symbols F

p is Relation-like NAT -defined 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

{ (p . b

free_QC-variables F

{ (p . b

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

F

(F

QC-WFF F

bool (QC-WFF F

{ b

[:(F

bool [:(F

(F

F

QC-variables F

bound_QC-variables F

bool (QC-variables F

QC-pred_symbols F

[:(QC-WFF F

bool [:(QC-WFF F

A is Relation-like QC-WFF F

A . (F

A | (F

x is Relation-like (F

x . (F

p is Element of (F

(F

x . (F

x . p is Element of F

F

y is Element of (F

(F

x . (F

x . y is Element of F

F

p is Element of bound_QC-variables F

(F

x . (F

F

l is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT

l -ary_QC-pred_symbols F

bool (QC-pred_symbols F

F1 is Relation-like NAT -defined QC-variables F

ll is Element of l -ary_QC-pred_symbols F

(l,F

x . (l,F

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

the_pred_symbol_of (l,F

A . (l,F

A . p is Element of F

the_left_argument_of (F

the_right_argument_of (F

the_argument_of (F

A . (F

A . y is Element of F

A . (F

bound_in (F

the_scope_of (F

A . (F

F

(F

QC-WFF F

bool (QC-WFF F

{ b

F

[:(F

bool [:(F

F

(F

F

F

QC-variables F

bound_QC-variables F

bool (QC-variables F

QC-pred_symbols F

F

F

F

F

A is Element of (F

F

F

(F

F

F

x is Element of (F

F

F

(F

F

F

p is Element of bound_QC-variables F

(F

F

F

y is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT

y -ary_QC-pred_symbols F

bool (QC-pred_symbols F

p is Relation-like NAT -defined QC-variables F

l is Element of y -ary_QC-pred_symbols F

(y,F

F

F

F

F

F

F

F

F

F

F

F

F

F

F

F

F

F

F

QC-WFF F

(F

bool (QC-WFF F

{ b

F

[:(F

bool [:(F

F

(F

F

QC-variables F

bound_QC-variables F

bool (QC-variables F

QC-pred_symbols F

A is Relation-like (F

A . (F

A . F

x is ext-real V29() V30() V31() V32() V33() V34() ordinal natural V43() cardinal Element of NAT

x -ary_QC-pred_symbols F

bool (QC-pred_symbols F

y is Element of x -ary_QC-pred_symbols F

p is Relation-like NAT -defined QC-variables F

(x,F

A . (x,F

F

p is Element of (F

(F

A . (F

A . p is Element of F

F

l is Element of (F

F1 is Element of (F

(F

A . (F

A . l is Element of F

A . F1 is Element of F

F

F2 is Element of bound_QC-variables F

ll is Element of (F

(F

A . (F

A . ll is Element of F

F

A is Element of F

x is Element of F

p is Relation-like (F

p . F

p . (F

y is Relation-like (F

y . F

y . (F

F

F

QC-WFF F

(F

bool (QC-WFF F

{ b

[:(F

bool [:(F

(F

F

QC-variables F

bound_QC-variables F

bool (QC-variables F

QC-pred_symbols F

F

A is Relation-like (F

A . (F

F

F

QC-pred_symbols F

F

F

bool (QC-pred_symbols F

bound_QC-variables F

QC-variables F

bool (QC-variables F

QC-WFF F

(F

bool (QC-WFF F

{ b

[:(F

bool [:(F

(F

F

F

F

(F

F

F

A is Relation-like (F

A . (F

A . (F

F

F

QC-WFF F

(F

bool (QC-WFF F

{ b

[:(F

bool [:(F

(F

F

QC-variables F

bound_QC-variables F

bool (QC-variables F

QC-pred_symbols F

F

(F

F

F

F

A is Relation-like (F

A . F

A . (F

x is Relation-like (F

x . (F

x . (F

x . F

F

F

F

QC-WFF F

(F

bool (QC-WFF F

{ b

[:(F

bool [:(F

(F

F

QC-variables F

bound_QC-variables F

bool (QC-variables F

QC-pred_symbols F

F

F

(F

F

F

F

F

A is Relation-like (F

A . F

A . (F

x is Relation-like (F

x . F

x . (F

p is Relation-like (F

p . (F

p . (F

p . F

p . F

F

F

F

QC-variables F

bound_QC-variables F

bool (QC-variables F

QC-WFF F

(F

bool (QC-WFF F

{ b

[:(F

bool [:(F

(F

F

QC-pred_symbols F

F

F

(F

F

F

F

A is Relation-like (F

A . F

A . (F

x is Relation-like (F

x . (F

x . (F

x . F

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

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

c

the_scope_of c

p . (the_scope_of c

p . c

bound_in c

All ((bound_in c

IFEQ ((bound_in c

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

c

the_scope_of c

y . (the_scope_of c

y . c

bound_in c

All ((bound_in c

IFEQ ((bound_in c

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

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

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

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

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

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

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