:: QC_LANG3 semantic presentation

REAL is V24() V25() V26() V30() set

NAT is non empty V24() V25() V26() V27() V28() V29() V30() V31() V32() V33() Element of bool REAL

bool REAL is non empty set

NAT is non empty V24() V25() V26() V27() V28() V29() V30() V31() V32() V33() set

bool NAT is non empty set

bool NAT is non empty set

{} is set

1 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

F

QC-WFF F

F

[:(QC-WFF F

bool [:(QC-WFF F

VERUM F

K98() is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

[K98(),K98()] is set

{K98(),K98()} is V24() V25() V26() V27() V28() V29() set

{K98()} is V24() V25() V26() V27() V28() V29() set

{{K98(),K98()},{K98()}} is set

<*[K98(),K98()]*> is V1() Function-like set

F

F

F

QC-pred_symbols F

QC-symbols F

K49(F

7 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

{ [b

QC-variables F

6 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

{6} is V24() V25() V26() V27() V28() V29() set

[:{6},NAT:] is set

4 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

5 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

{4,5} is V24() V25() V26() V27() V28() V29() set

[:{4,5},(QC-symbols F

[:{6},NAT:] \/ [:{4,5},(QC-symbols F

A is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

A -ary_QC-pred_symbols F

bool (QC-pred_symbols F

{ b

x is Element of A -ary_QC-pred_symbols F

p is V1() V4( NAT ) V5( QC-variables F

x ! p is Element of QC-WFF F

F

F

F

bound_QC-variables F

bool (QC-variables F

{4} is V24() V25() V26() V27() V28() V29() set

[:{4},(QC-symbols F

A is Element of bound_QC-variables F

x is Element of QC-WFF F

F

F

All (A,x) is Element of QC-WFF F

3 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

[3,K98()] is set

{3,K98()} is V24() V25() V26() V27() V28() V29() set

{3} is V24() V25() V26() V27() V28() V29() set

{{3,K98()},{3}} is set

<*[3,K98()]*> is V1() Function-like set

<*A*> is V1() V4( NAT ) V5( bound_QC-variables F

K113(<*[3,K98()]*>,<*A*>) is V1() Function-like FinSequence-like set

@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols F

[:NAT,(QC-symbols F

K113(K113(<*[3,K98()]*>,<*A*>),(@ x)) is V1() Function-like FinSequence-like set

F

F

the_scope_of (All (A,x)) is Element of QC-WFF F

F

F

A is Element of QC-WFF F

F

F

x is Element of QC-WFF F

F

F

A '&' x is Element of QC-WFF F

2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

[2,K98()] is set

{2,K98()} is V24() V25() V26() V27() V28() V29() set

{2} is V24() V25() V26() V27() V28() V29() set

{{2,K98()},{2}} is set

<*[2,K98()]*> is V1() Function-like set

@ A is V1() V4( NAT ) V5([:NAT,(QC-symbols F

[:NAT,(QC-symbols F

K113(<*[2,K98()]*>,(@ A)) is V1() Function-like FinSequence-like set

@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols F

K113(K113(<*[2,K98()]*>,(@ A)),(@ x)) is V1() Function-like FinSequence-like set

F

F

the_left_argument_of (A '&' x) is Element of QC-WFF F

the_right_argument_of (A '&' x) is Element of QC-WFF F

F

A is Element of QC-WFF F

F

F

'not' A is Element of QC-WFF F

[1,K98()] is set

{1,K98()} is V24() V25() V26() V27() V28() V29() set

{1} is V24() V25() V26() V27() V28() V29() set

{{1,K98()},{1}} is set

<*[1,K98()]*> is V1() Function-like set

@ A is V1() V4( NAT ) V5([:NAT,(QC-symbols F

[:NAT,(QC-symbols F

K113(<*[1,K98()]*>,(@ A)) is V1() Function-like FinSequence-like set

F

F

the_argument_of ('not' A) is Element of QC-WFF F

F

F

F

F

F

QC-WFF F

[:(QC-WFF F

bool [:(QC-WFF F

F

VERUM F

K98() is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

[K98(),K98()] is set

{K98(),K98()} is V24() V25() V26() V27() V28() V29() set

{K98()} is V24() V25() V26() V27() V28() V29() set

{{K98(),K98()},{K98()}} is set

<*[K98(),K98()]*> is V1() Function-like set

F

A is V1() V4( QC-WFF F

A . (VERUM F

A . F

x is Element of QC-WFF F

A . x is Element of F

p is Element of QC-WFF F

A . p is Element of F

F

V is Element of QC-WFF F

x is Element of F

the_argument_of V is Element of QC-WFF F

A . (the_argument_of V) is Element of F

A . V is Element of F

F

a1 is Element of QC-WFF F

a2 is Element of F

the_left_argument_of a1 is Element of QC-WFF F

A . (the_left_argument_of a1) is Element of F

c

the_right_argument_of a1 is Element of QC-WFF F

A . (the_right_argument_of a1) is Element of F

A . a1 is Element of F

F

c

c

the_scope_of c

A . (the_scope_of c

A . c

F

A is Element of F

x is Element of F

p is V1() V4( QC-WFF F

p . F

V is V1() V4( QC-WFF F

V . F

F

QC-WFF F

F

[:(QC-WFF F

bool [:(QC-WFF F

VERUM F

K98() is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

[K98(),K98()] is set

{K98(),K98()} is V24() V25() V26() V27() V28() V29() set

{K98()} is V24() V25() V26() V27() V28() V29() set

{{K98(),K98()},{K98()}} is set

<*[K98(),K98()]*> is V1() Function-like set

F

F

A is V1() V4( QC-WFF F

A . (VERUM F

F

F

QC-WFF F

[:(QC-WFF F

bool [:(QC-WFF F

VERUM F

K98() is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

[K98(),K98()] is set

{K98(),K98()} is V24() V25() V26() V27() V28() V29() set

{K98()} is V24() V25() V26() V27() V28() V29() set

{{K98(),K98()},{K98()}} is set

<*[K98(),K98()]*> is V1() Function-like set

F

F

F

F

A is V1() V4( QC-WFF F

A . F

F

F

QC-WFF F

[:(QC-WFF F

bool [:(QC-WFF F

VERUM F

K98() is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

[K98(),K98()] is set

{K98(),K98()} is V24() V25() V26() V27() V28() V29() set

{K98()} is V24() V25() V26() V27() V28() V29() set

{{K98(),K98()},{K98()}} is set

<*[K98(),K98()]*> is V1() Function-like set

F

F

F

the_argument_of F

F

F

A is V1() V4( QC-WFF F

A . F

A . (the_argument_of F

F

F

QC-WFF F

[:(QC-WFF F

bool [:(QC-WFF F

VERUM F

K98() is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

[K98(),K98()] is set

{K98(),K98()} is V24() V25() V26() V27() V28() V29() set

{K98()} is V24() V25() V26() V27() V28() V29() set

{{K98(),K98()},{K98()}} is set

<*[K98(),K98()]*> is V1() Function-like set

F

F

the_left_argument_of F

F

the_right_argument_of F

F

F

A is V1() V4( QC-WFF F

A . F

x is Element of F

p is Element of F

F

A . (the_left_argument_of F

A . (the_right_argument_of F

F

F

QC-WFF F

[:(QC-WFF F

bool [:(QC-WFF F

VERUM F

K98() is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

[K98(),K98()] is set

{K98(),K98()} is V24() V25() V26() V27() V28() V29() set

{K98()} is V24() V25() V26() V27() V28() V29() set

{{K98(),K98()},{K98()}} is set

<*[K98(),K98()]*> is V1() Function-like set

F

F

F

the_scope_of F

F

F

A is V1() V4( QC-WFF F

A . F

A . (the_scope_of F

A is V1() non empty QC-alphabet

QC-pred_symbols A is non empty set

QC-symbols A is non empty set

K49(A) is set

7 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

{ [b

x is Element of QC-pred_symbols A

the_arity_of x is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

(the_arity_of x) -ary_QC-pred_symbols A is non empty Element of bool (QC-pred_symbols A)

bool (QC-pred_symbols A) is non empty set

{ b

A is V1() non empty QC-alphabet

QC-variables A is non empty set

6 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

{6} is V24() V25() V26() V27() V28() V29() set

[:{6},NAT:] is set

4 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

5 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

{4,5} is V24() V25() V26() V27() V28() V29() set

QC-symbols A is non empty set

K49(A) is set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

bool (QC-variables A) is non empty set

x is V1() V4( NAT ) V5( QC-variables A) Function-like FinSequence-like FinSequence of QC-variables A

len x is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

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

{ (x . b

bool p is non empty set

x is set

a1 is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

x . a1 is set

A is V1() non empty QC-alphabet

QC-variables A is non empty set

QC-symbols A is non empty set

K49(A) is set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

x is V1() V4( NAT ) V5( QC-variables A) Function-like FinSequence-like FinSequence of QC-variables A

still_not-bound_in x is Element of bool (bound_QC-variables A)

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

bool (QC-variables A) is non empty set

{4} is V24() V25() V26() V27() V28() V29() set

[:{4},(QC-symbols A):] is set

bool (bound_QC-variables A) is non empty set

len x is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

{ (x . b

(A,x,(bound_QC-variables A)) is Element of bool (bound_QC-variables A)

A is V1() non empty QC-alphabet

QC-WFF A is non empty set

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

QC-variables A is non empty set

QC-symbols A is non empty set

K49(A) is set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

bool (QC-variables A) is non empty set

{4} is V24() V25() V26() V27() V28() V29() set

[:{4},(QC-symbols A):] is set

bool (bound_QC-variables A) is non empty set

[:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set

bool [:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set

VERUM A is Element of QC-WFF A

K98() is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

[K98(),K98()] is set

{K98(),K98()} is V24() V25() V26() V27() V28() V29() set

{K98()} is V24() V25() V26() V27() V28() V29() set

{{K98(),K98()},{K98()}} is set

<*[K98(),K98()]*> is V1() Function-like set

{} (bound_QC-variables A) is empty proper V24() V25() V26() V27() V28() V29() V30() V31() V32() V33() V35() V36() V37() Element of bool (bound_QC-variables A)

x is Element of QC-WFF A

still_not-bound_in x is Element of bool (bound_QC-variables A)

p is Element of bool (bound_QC-variables A)

V is V1() V4( QC-WFF A) V5( bool (bound_QC-variables A)) Function-like V18( QC-WFF A, bool (bound_QC-variables A)) Element of bool [:(QC-WFF A),(bool (bound_QC-variables A)):]

V . x is Element of bool (bound_QC-variables A)

V . (VERUM A) is Element of bool (bound_QC-variables A)

x is Element of QC-WFF A

V . x is Element of bool (bound_QC-variables A)

the_arguments_of x is V1() V4( NAT ) V5( QC-variables A) Function-like FinSequence-like FinSequence of QC-variables A

still_not-bound_in (the_arguments_of x) is Element of bool (bound_QC-variables A)

len (the_arguments_of x) is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

{ ((the_arguments_of x) . b

the_argument_of x is Element of QC-WFF A

V . (the_argument_of x) is Element of bool (bound_QC-variables A)

the_left_argument_of x is Element of QC-WFF A

V . (the_left_argument_of x) is Element of bool (bound_QC-variables A)

the_right_argument_of x is Element of QC-WFF A

V . (the_right_argument_of x) is Element of bool (bound_QC-variables A)

the_scope_of x is Element of QC-WFF A

V . (the_scope_of x) is Element of bool (bound_QC-variables A)

bound_in x is Element of bound_QC-variables A

{(bound_in x)} is set

a1 is Element of bool (bound_QC-variables A)

a2 is Element of bool (bound_QC-variables A)

a1 \/ a2 is Element of bool (bound_QC-variables A)

a1 \ {(bound_in x)} is Element of bool (bound_QC-variables A)

V is V1() V4( QC-WFF A) V5( bool (bound_QC-variables A)) Function-like V18( QC-WFF A, bool (bound_QC-variables A)) Element of bool [:(QC-WFF A),(bool (bound_QC-variables A)):]

V . x is Element of bool (bound_QC-variables A)

V . (VERUM A) is Element of bool (bound_QC-variables A)

x is Element of QC-WFF A

V . x is Element of bool (bound_QC-variables A)

the_arguments_of x is V1() V4( NAT ) V5( QC-variables A) Function-like FinSequence-like FinSequence of QC-variables A

len (the_arguments_of x) is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

{ ((the_arguments_of x) . b

still_not-bound_in (the_arguments_of x) is Element of bool (bound_QC-variables A)

the_argument_of x is Element of QC-WFF A

V . (the_argument_of x) is Element of bool (bound_QC-variables A)

the_left_argument_of x is Element of QC-WFF A

V . (the_left_argument_of x) is Element of bool (bound_QC-variables A)

the_right_argument_of x is Element of QC-WFF A

V . (the_right_argument_of x) is Element of bool (bound_QC-variables A)

(V . (the_left_argument_of x)) \/ (V . (the_right_argument_of x)) is Element of bool (bound_QC-variables A)

the_scope_of x is Element of QC-WFF A

V . (the_scope_of x) is Element of bool (bound_QC-variables A)

bound_in x is Element of bound_QC-variables A

{(bound_in x)} is set

(V . (the_scope_of x)) \ {(bound_in x)} is Element of bool (bound_QC-variables A)

A is V1() non empty QC-alphabet

VERUM A is Element of QC-WFF A

QC-WFF A is non empty set

still_not-bound_in (VERUM A) is Element of bool (bound_QC-variables A)

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

QC-variables A is non empty set

QC-symbols A is non empty set

K49(A) is set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is set

bool (bound_QC-variables A) is non empty set

[:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set

bool [:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set

{} (bound_QC-variables A) is empty proper V24() V25() V26() V27() V28() V29() V30() V31() V32() V33() V35() V36() V37() Element of bool (bound_QC-variables A)

p is Element of bool (bound_QC-variables A)

x is Element of QC-WFF A

still_not-bound_in x is Element of bool (bound_QC-variables A)

x is Element of bool (bound_QC-variables A)

a1 is V1() V4( QC-WFF A) V5( bool (bound_QC-variables A)) Function-like V18( QC-WFF A, bool (bound_QC-variables A)) Element of bool [:(QC-WFF A),(bool (bound_QC-variables A)):]

V is Element of QC-WFF A

a1 . V is Element of bool (bound_QC-variables A)

still_not-bound_in V is Element of bool (bound_QC-variables A)

A is V1() non empty QC-alphabet

QC-WFF A is non empty set

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

QC-variables A is non empty set

QC-symbols A is non empty set

K49(A) is set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is set

bool (bound_QC-variables A) is non empty set

[:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set

bool [:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set

VERUM A is Element of QC-WFF A

{} (bound_QC-variables A) is empty proper V24() V25() V26() V27() V28() V29() V30() V31() V32() V33() V35() V36() V37() Element of bool (bound_QC-variables A)

p is Element of bool (bound_QC-variables A)

x is Element of QC-WFF A

still_not-bound_in x is Element of bool (bound_QC-variables A)

x is Element of bool (bound_QC-variables A)

a1 is V1() V4( QC-WFF A) V5( bool (bound_QC-variables A)) Function-like V18( QC-WFF A, bool (bound_QC-variables A)) Element of bool [:(QC-WFF A),(bool (bound_QC-variables A)):]

V is Element of QC-WFF A

a1 . V is Element of bool (bound_QC-variables A)

still_not-bound_in V is Element of bool (bound_QC-variables A)

x is Element of QC-WFF A

still_not-bound_in x is Element of bool (bound_QC-variables A)

the_arguments_of x is V1() V4( NAT ) V5( QC-variables A) Function-like FinSequence-like FinSequence of QC-variables A

still_not-bound_in (the_arguments_of x) is Element of bool (bound_QC-variables A)

len (the_arguments_of x) is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

{ ((the_arguments_of x) . b

A is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

x is V1() non empty QC-alphabet

QC-pred_symbols x is non empty set

QC-symbols x is non empty set

K49(x) is set

7 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

{ [b

A -ary_QC-pred_symbols x is non empty Element of bool (QC-pred_symbols x)

bool (QC-pred_symbols x) is non empty set

{ b

QC-variables x is non empty set

[:{4,5},(QC-symbols x):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols x):] is set

p is Element of A -ary_QC-pred_symbols x

V is V1() V4( NAT ) V5( QC-variables x) Function-like V45(A) FinSequence-like FinSequence of QC-variables x

p ! V is Element of QC-WFF x

QC-WFF x is non empty set

still_not-bound_in (p ! V) is Element of bool (bound_QC-variables x)

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

bool (QC-variables x) is non empty set

[:{4},(QC-symbols x):] is set

bool (bound_QC-variables x) is non empty set

still_not-bound_in V is Element of bool (bound_QC-variables x)

len V is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

{ (V . b

the_arguments_of (p ! V) is V1() V4( NAT ) V5( QC-variables x) Function-like FinSequence-like FinSequence of QC-variables x

A is V1() non empty QC-alphabet

QC-WFF A is non empty set

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

QC-variables A is non empty set

QC-symbols A is non empty set

K49(A) is set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is set

bool (bound_QC-variables A) is non empty set

[:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set

bool [:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set

VERUM A is Element of QC-WFF A

{} (bound_QC-variables A) is empty proper V24() V25() V26() V27() V28() V29() V30() V31() V32() V33() V35() V36() V37() Element of bool (bound_QC-variables A)

p is Element of bool (bound_QC-variables A)

x is Element of QC-WFF A

still_not-bound_in x is Element of bool (bound_QC-variables A)

x is Element of bool (bound_QC-variables A)

a1 is V1() V4( QC-WFF A) V5( bool (bound_QC-variables A)) Function-like V18( QC-WFF A, bool (bound_QC-variables A)) Element of bool [:(QC-WFF A),(bool (bound_QC-variables A)):]

V is Element of QC-WFF A

a1 . V is Element of bool (bound_QC-variables A)

still_not-bound_in V is Element of bool (bound_QC-variables A)

x is Element of QC-WFF A

still_not-bound_in x is Element of bool (bound_QC-variables A)

the_argument_of x is Element of QC-WFF A

still_not-bound_in (the_argument_of x) is Element of bool (bound_QC-variables A)

A is V1() non empty QC-alphabet

QC-WFF A is non empty set

x is Element of QC-WFF A

'not' x is Element of QC-WFF A

[1,K98()] is set

{1,K98()} is V24() V25() V26() V27() V28() V29() set

{1} is V24() V25() V26() V27() V28() V29() set

{{1,K98()},{1}} is set

<*[1,K98()]*> is V1() Function-like set

@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

QC-symbols A is non empty set

K49(A) is set

[:NAT,(QC-symbols A):] is non empty set

K113(<*[1,K98()]*>,(@ x)) is V1() Function-like FinSequence-like set

still_not-bound_in ('not' x) is Element of bool (bound_QC-variables A)

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

QC-variables A is non empty set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is set

bool (bound_QC-variables A) is non empty set

still_not-bound_in x is Element of bool (bound_QC-variables A)

the_argument_of ('not' x) is Element of QC-WFF A

A is V1() non empty QC-alphabet

FALSUM A is Element of QC-WFF A

QC-WFF A is non empty set

still_not-bound_in (FALSUM A) is Element of bool (bound_QC-variables A)

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

QC-variables A is non empty set

QC-symbols A is non empty set

K49(A) is set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is set

bool (bound_QC-variables A) is non empty set

VERUM A is Element of QC-WFF A

'not' (VERUM A) is Element of QC-WFF A

[1,K98()] is set

{1,K98()} is V24() V25() V26() V27() V28() V29() set

{1} is V24() V25() V26() V27() V28() V29() set

{{1,K98()},{1}} is set

<*[1,K98()]*> is V1() Function-like set

@ (VERUM A) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

[:NAT,(QC-symbols A):] is non empty set

K113(<*[1,K98()]*>,(@ (VERUM A))) is V1() Function-like FinSequence-like set

still_not-bound_in ('not' (VERUM A)) is Element of bool (bound_QC-variables A)

still_not-bound_in (VERUM A) is Element of bool (bound_QC-variables A)

A is V1() non empty QC-alphabet

QC-WFF A is non empty set

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

QC-variables A is non empty set

QC-symbols A is non empty set

K49(A) is set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is set

bool (bound_QC-variables A) is non empty set

[:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set

bool [:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set

VERUM A is Element of QC-WFF A

{} (bound_QC-variables A) is empty proper V24() V25() V26() V27() V28() V29() V30() V31() V32() V33() V35() V36() V37() Element of bool (bound_QC-variables A)

p is Element of bool (bound_QC-variables A)

x is Element of QC-WFF A

still_not-bound_in x is Element of bool (bound_QC-variables A)

x is Element of bool (bound_QC-variables A)

a1 is V1() V4( QC-WFF A) V5( bool (bound_QC-variables A)) Function-like V18( QC-WFF A, bool (bound_QC-variables A)) Element of bool [:(QC-WFF A),(bool (bound_QC-variables A)):]

V is Element of QC-WFF A

a1 . V is Element of bool (bound_QC-variables A)

still_not-bound_in V is Element of bool (bound_QC-variables A)

x is Element of QC-WFF A

still_not-bound_in x is Element of bool (bound_QC-variables A)

the_left_argument_of x is Element of QC-WFF A

still_not-bound_in (the_left_argument_of x) is Element of bool (bound_QC-variables A)

the_right_argument_of x is Element of QC-WFF A

still_not-bound_in (the_right_argument_of x) is Element of bool (bound_QC-variables A)

(still_not-bound_in (the_left_argument_of x)) \/ (still_not-bound_in (the_right_argument_of x)) is Element of bool (bound_QC-variables A)

A is V1() non empty QC-alphabet

QC-WFF A is non empty set

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

QC-variables A is non empty set

QC-symbols A is non empty set

K49(A) is set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is set

x is Element of QC-WFF A

p is Element of QC-WFF A

x '&' p is Element of QC-WFF A

2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

[2,K98()] is set

{2,K98()} is V24() V25() V26() V27() V28() V29() set

{2} is V24() V25() V26() V27() V28() V29() set

{{2,K98()},{2}} is set

<*[2,K98()]*> is V1() Function-like set

@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

[:NAT,(QC-symbols A):] is non empty set

K113(<*[2,K98()]*>,(@ x)) is V1() Function-like FinSequence-like set

@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

K113(K113(<*[2,K98()]*>,(@ x)),(@ p)) is V1() Function-like FinSequence-like set

still_not-bound_in (x '&' p) is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is non empty set

still_not-bound_in x is Element of bool (bound_QC-variables A)

still_not-bound_in p is Element of bool (bound_QC-variables A)

(still_not-bound_in x) \/ (still_not-bound_in p) is Element of bool (bound_QC-variables A)

the_left_argument_of (x '&' p) is Element of QC-WFF A

the_right_argument_of (x '&' p) is Element of QC-WFF A

A is V1() non empty QC-alphabet

QC-WFF A is non empty set

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

QC-variables A is non empty set

QC-symbols A is non empty set

K49(A) is set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is set

bool (bound_QC-variables A) is non empty set

[:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set

bool [:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set

VERUM A is Element of QC-WFF A

{} (bound_QC-variables A) is empty proper V24() V25() V26() V27() V28() V29() V30() V31() V32() V33() V35() V36() V37() Element of bool (bound_QC-variables A)

p is Element of bool (bound_QC-variables A)

x is Element of QC-WFF A

still_not-bound_in x is Element of bool (bound_QC-variables A)

x is Element of bool (bound_QC-variables A)

a1 is V1() V4( QC-WFF A) V5( bool (bound_QC-variables A)) Function-like V18( QC-WFF A, bool (bound_QC-variables A)) Element of bool [:(QC-WFF A),(bool (bound_QC-variables A)):]

V is Element of QC-WFF A

a1 . V is Element of bool (bound_QC-variables A)

still_not-bound_in V is Element of bool (bound_QC-variables A)

x is Element of QC-WFF A

still_not-bound_in x is Element of bool (bound_QC-variables A)

the_scope_of x is Element of QC-WFF A

still_not-bound_in (the_scope_of x) is Element of bool (bound_QC-variables A)

bound_in x is Element of bound_QC-variables A

{(bound_in x)} is set

(still_not-bound_in (the_scope_of x)) \ {(bound_in x)} is Element of bool (bound_QC-variables A)

H

A is V1() non empty QC-alphabet

QC-variables A is non empty set

QC-symbols A is non empty set

K49(A) is set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

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

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is set

QC-WFF A is non empty set

x is Element of bound_QC-variables A

{x} is set

p is Element of QC-WFF A

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

3 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

[3,K98()] is set

{3,K98()} is V24() V25() V26() V27() V28() V29() set

{3} is V24() V25() V26() V27() V28() V29() set

{{3,K98()},{3}} is set

<*[3,K98()]*> is V1() Function-like set

<*x*> is V1() V4( NAT ) V5( bound_QC-variables A) Function-like FinSequence-like FinSequence of bound_QC-variables A

K113(<*[3,K98()]*>,<*x*>) is V1() Function-like FinSequence-like set

@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

[:NAT,(QC-symbols A):] is non empty set

K113(K113(<*[3,K98()]*>,<*x*>),(@ p)) is V1() Function-like FinSequence-like set

still_not-bound_in (All (x,p)) is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is non empty set

still_not-bound_in p is Element of bool (bound_QC-variables A)

(still_not-bound_in p) \ {x} is Element of bool (bound_QC-variables A)

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

bound_in (All (x,p)) is Element of bound_QC-variables A

A is V1() non empty QC-alphabet

QC-WFF A is non empty set

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

QC-variables A is non empty set

QC-symbols A is non empty set

K49(A) is set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is set

x is Element of QC-WFF A

still_not-bound_in x is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is non empty set

the_left_disjunct_of x is Element of QC-WFF A

still_not-bound_in (the_left_disjunct_of x) is Element of bool (bound_QC-variables A)

the_right_disjunct_of x is Element of QC-WFF A

still_not-bound_in (the_right_disjunct_of x) is Element of bool (bound_QC-variables A)

(still_not-bound_in (the_left_disjunct_of x)) \/ (still_not-bound_in (the_right_disjunct_of x)) is Element of bool (bound_QC-variables A)

(the_left_disjunct_of x) 'or' (the_right_disjunct_of x) is Element of QC-WFF A

'not' (the_left_disjunct_of x) is Element of QC-WFF A

[1,K98()] is set

{1,K98()} is V24() V25() V26() V27() V28() V29() set

{1} is V24() V25() V26() V27() V28() V29() set

{{1,K98()},{1}} is set

<*[1,K98()]*> is V1() Function-like set

@ (the_left_disjunct_of x) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

[:NAT,(QC-symbols A):] is non empty set

K113(<*[1,K98()]*>,(@ (the_left_disjunct_of x))) is V1() Function-like FinSequence-like set

'not' (the_right_disjunct_of x) is Element of QC-WFF A

@ (the_right_disjunct_of x) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

K113(<*[1,K98()]*>,(@ (the_right_disjunct_of x))) is V1() Function-like FinSequence-like set

('not' (the_left_disjunct_of x)) '&' ('not' (the_right_disjunct_of x)) is Element of QC-WFF A

2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

[2,K98()] is set

{2,K98()} is V24() V25() V26() V27() V28() V29() set

{2} is V24() V25() V26() V27() V28() V29() set

{{2,K98()},{2}} is set

<*[2,K98()]*> is V1() Function-like set

@ ('not' (the_left_disjunct_of x)) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

K113(<*[2,K98()]*>,(@ ('not' (the_left_disjunct_of x)))) is V1() Function-like FinSequence-like set

@ ('not' (the_right_disjunct_of x)) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

K113(K113(<*[2,K98()]*>,(@ ('not' (the_left_disjunct_of x)))),(@ ('not' (the_right_disjunct_of x)))) is V1() Function-like FinSequence-like set

'not' (('not' (the_left_disjunct_of x)) '&' ('not' (the_right_disjunct_of x))) is Element of QC-WFF A

@ (('not' (the_left_disjunct_of x)) '&' ('not' (the_right_disjunct_of x))) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

K113(<*[1,K98()]*>,(@ (('not' (the_left_disjunct_of x)) '&' ('not' (the_right_disjunct_of x))))) is V1() Function-like FinSequence-like set

still_not-bound_in (('not' (the_left_disjunct_of x)) '&' ('not' (the_right_disjunct_of x))) is Element of bool (bound_QC-variables A)

still_not-bound_in ('not' (the_left_disjunct_of x)) is Element of bool (bound_QC-variables A)

still_not-bound_in ('not' (the_right_disjunct_of x)) is Element of bool (bound_QC-variables A)

(still_not-bound_in ('not' (the_left_disjunct_of x))) \/ (still_not-bound_in ('not' (the_right_disjunct_of x))) is Element of bool (bound_QC-variables A)

(still_not-bound_in (the_left_disjunct_of x)) \/ (still_not-bound_in ('not' (the_right_disjunct_of x))) is Element of bool (bound_QC-variables A)

A is V1() non empty QC-alphabet

QC-WFF A is non empty set

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

QC-variables A is non empty set

QC-symbols A is non empty set

K49(A) is set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is set

x is Element of QC-WFF A

p is Element of QC-WFF A

x 'or' p is Element of QC-WFF A

still_not-bound_in (x 'or' p) is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is non empty set

still_not-bound_in x is Element of bool (bound_QC-variables A)

still_not-bound_in p is Element of bool (bound_QC-variables A)

(still_not-bound_in x) \/ (still_not-bound_in p) is Element of bool (bound_QC-variables A)

the_right_disjunct_of (x 'or' p) is Element of QC-WFF A

the_left_disjunct_of (x 'or' p) is Element of QC-WFF A

A is V1() non empty QC-alphabet

QC-WFF A is non empty set

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

QC-variables A is non empty set

QC-symbols A is non empty set

K49(A) is set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is set

x is Element of QC-WFF A

still_not-bound_in x is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is non empty set

the_antecedent_of x is Element of QC-WFF A

still_not-bound_in (the_antecedent_of x) is Element of bool (bound_QC-variables A)

the_right_disjunct_of x is Element of QC-WFF A

still_not-bound_in (the_right_disjunct_of x) is Element of bool (bound_QC-variables A)

(still_not-bound_in (the_antecedent_of x)) \/ (still_not-bound_in (the_right_disjunct_of x)) is Element of bool (bound_QC-variables A)

(the_antecedent_of x) => (the_right_disjunct_of x) is Element of QC-WFF A

'not' (the_right_disjunct_of x) is Element of QC-WFF A

[1,K98()] is set

{1,K98()} is V24() V25() V26() V27() V28() V29() set

{1} is V24() V25() V26() V27() V28() V29() set

{{1,K98()},{1}} is set

<*[1,K98()]*> is V1() Function-like set

@ (the_right_disjunct_of x) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

[:NAT,(QC-symbols A):] is non empty set

K113(<*[1,K98()]*>,(@ (the_right_disjunct_of x))) is V1() Function-like FinSequence-like set

(the_antecedent_of x) '&' ('not' (the_right_disjunct_of x)) is Element of QC-WFF A

2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

[2,K98()] is set

{2,K98()} is V24() V25() V26() V27() V28() V29() set

{2} is V24() V25() V26() V27() V28() V29() set

{{2,K98()},{2}} is set

<*[2,K98()]*> is V1() Function-like set

@ (the_antecedent_of x) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

K113(<*[2,K98()]*>,(@ (the_antecedent_of x))) is V1() Function-like FinSequence-like set

@ ('not' (the_right_disjunct_of x)) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

K113(K113(<*[2,K98()]*>,(@ (the_antecedent_of x))),(@ ('not' (the_right_disjunct_of x)))) is V1() Function-like FinSequence-like set

'not' ((the_antecedent_of x) '&' ('not' (the_right_disjunct_of x))) is Element of QC-WFF A

@ ((the_antecedent_of x) '&' ('not' (the_right_disjunct_of x))) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

K113(<*[1,K98()]*>,(@ ((the_antecedent_of x) '&' ('not' (the_right_disjunct_of x))))) is V1() Function-like FinSequence-like set

still_not-bound_in ((the_antecedent_of x) '&' ('not' (the_right_disjunct_of x))) is Element of bool (bound_QC-variables A)

still_not-bound_in ('not' (the_right_disjunct_of x)) is Element of bool (bound_QC-variables A)

(still_not-bound_in (the_antecedent_of x)) \/ (still_not-bound_in ('not' (the_right_disjunct_of x))) is Element of bool (bound_QC-variables A)

A is V1() non empty QC-alphabet

QC-WFF A is non empty set

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

QC-variables A is non empty set

QC-symbols A is non empty set

K49(A) is set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is set

x is Element of QC-WFF A

p is Element of QC-WFF A

x => p is Element of QC-WFF A

still_not-bound_in (x => p) is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is non empty set

still_not-bound_in x is Element of bool (bound_QC-variables A)

still_not-bound_in p is Element of bool (bound_QC-variables A)

(still_not-bound_in x) \/ (still_not-bound_in p) is Element of bool (bound_QC-variables A)

the_right_disjunct_of (x => p) is Element of QC-WFF A

the_antecedent_of (x => p) is Element of QC-WFF A

A is V1() non empty QC-alphabet

QC-WFF A is non empty set

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

QC-variables A is non empty set

QC-symbols A is non empty set

K49(A) is set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is set

x is Element of QC-WFF A

still_not-bound_in x is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is non empty set

the_left_side_of x is Element of QC-WFF A

still_not-bound_in (the_left_side_of x) is Element of bool (bound_QC-variables A)

the_right_side_of x is Element of QC-WFF A

still_not-bound_in (the_right_side_of x) is Element of bool (bound_QC-variables A)

(still_not-bound_in (the_left_side_of x)) \/ (still_not-bound_in (the_right_side_of x)) is Element of bool (bound_QC-variables A)

(the_left_side_of x) <=> (the_right_side_of x) is Element of QC-WFF A

(the_left_side_of x) => (the_right_side_of x) is Element of QC-WFF A

(the_right_side_of x) => (the_left_side_of x) is Element of QC-WFF A

((the_left_side_of x) => (the_right_side_of x)) '&' ((the_right_side_of x) => (the_left_side_of x)) is Element of QC-WFF A

2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

[2,K98()] is set

{2,K98()} is V24() V25() V26() V27() V28() V29() set

{2} is V24() V25() V26() V27() V28() V29() set

{{2,K98()},{2}} is set

<*[2,K98()]*> is V1() Function-like set

@ ((the_left_side_of x) => (the_right_side_of x)) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

[:NAT,(QC-symbols A):] is non empty set

K113(<*[2,K98()]*>,(@ ((the_left_side_of x) => (the_right_side_of x)))) is V1() Function-like FinSequence-like set

@ ((the_right_side_of x) => (the_left_side_of x)) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

K113(K113(<*[2,K98()]*>,(@ ((the_left_side_of x) => (the_right_side_of x)))),(@ ((the_right_side_of x) => (the_left_side_of x)))) is V1() Function-like FinSequence-like set

still_not-bound_in ((the_left_side_of x) => (the_right_side_of x)) is Element of bool (bound_QC-variables A)

still_not-bound_in ((the_right_side_of x) => (the_left_side_of x)) is Element of bool (bound_QC-variables A)

(still_not-bound_in ((the_left_side_of x) => (the_right_side_of x))) \/ (still_not-bound_in ((the_right_side_of x) => (the_left_side_of x))) is Element of bool (bound_QC-variables A)

((still_not-bound_in (the_left_side_of x)) \/ (still_not-bound_in (the_right_side_of x))) \/ (still_not-bound_in ((the_right_side_of x) => (the_left_side_of x))) is Element of bool (bound_QC-variables A)

((still_not-bound_in (the_left_side_of x)) \/ (still_not-bound_in (the_right_side_of x))) \/ ((still_not-bound_in (the_left_side_of x)) \/ (still_not-bound_in (the_right_side_of x))) is Element of bool (bound_QC-variables A)

A is V1() non empty QC-alphabet

QC-WFF A is non empty set

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

QC-variables A is non empty set

QC-symbols A is non empty set

K49(A) is set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is set

x is Element of QC-WFF A

p is Element of QC-WFF A

x <=> p is Element of QC-WFF A

still_not-bound_in (x <=> p) is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is non empty set

still_not-bound_in x is Element of bool (bound_QC-variables A)

still_not-bound_in p is Element of bool (bound_QC-variables A)

(still_not-bound_in x) \/ (still_not-bound_in p) is Element of bool (bound_QC-variables A)

the_right_side_of (x <=> p) is Element of QC-WFF A

the_left_side_of (x <=> p) is Element of QC-WFF A

A is V1() non empty QC-alphabet

QC-variables A is non empty set

QC-symbols A is non empty set

K49(A) is set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

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

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is set

QC-WFF A is non empty set

x is Element of bound_QC-variables A

{x} is set

p is Element of QC-WFF A

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

still_not-bound_in (Ex (x,p)) is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is non empty set

still_not-bound_in p is Element of bool (bound_QC-variables A)

(still_not-bound_in p) \ {x} is Element of bool (bound_QC-variables A)

'not' p is Element of QC-WFF A

[1,K98()] is set

{1,K98()} is V24() V25() V26() V27() V28() V29() set

{1} is V24() V25() V26() V27() V28() V29() set

{{1,K98()},{1}} is set

<*[1,K98()]*> is V1() Function-like set

@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

[:NAT,(QC-symbols A):] is non empty set

K113(<*[1,K98()]*>,(@ p)) is V1() Function-like FinSequence-like set

All (x,('not' p)) is Element of QC-WFF A

3 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

[3,K98()] is set

{3,K98()} is V24() V25() V26() V27() V28() V29() set

{3} is V24() V25() V26() V27() V28() V29() set

{{3,K98()},{3}} is set

<*[3,K98()]*> is V1() Function-like set

<*x*> is V1() V4( NAT ) V5( bound_QC-variables A) Function-like FinSequence-like FinSequence of bound_QC-variables A

K113(<*[3,K98()]*>,<*x*>) is V1() Function-like FinSequence-like set

@ ('not' p) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

K113(K113(<*[3,K98()]*>,<*x*>),(@ ('not' p))) is V1() Function-like FinSequence-like set

'not' (All (x,('not' p))) is Element of QC-WFF A

@ (All (x,('not' p))) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

K113(<*[1,K98()]*>,(@ (All (x,('not' p))))) is V1() Function-like FinSequence-like set

still_not-bound_in (All (x,('not' p))) is Element of bool (bound_QC-variables A)

still_not-bound_in ('not' p) is Element of bool (bound_QC-variables A)

(still_not-bound_in ('not' p)) \ {x} is Element of bool (bound_QC-variables A)

A is V1() non empty QC-alphabet

VERUM A is Element of QC-WFF A

QC-WFF A is non empty set

FALSUM A is Element of QC-WFF A

still_not-bound_in (VERUM A) is Element of bool (bound_QC-variables A)

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

QC-variables A is non empty set

QC-symbols A is non empty set

K49(A) is set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is set

bool (bound_QC-variables A) is non empty set

still_not-bound_in (FALSUM A) is Element of bool (bound_QC-variables A)

A is V1() non empty QC-alphabet

QC-WFF A is non empty set

x is Element of QC-WFF A

'not' x is Element of QC-WFF A

[1,K98()] is set

{1,K98()} is V24() V25() V26() V27() V28() V29() set

{1} is V24() V25() V26() V27() V28() V29() set

{{1,K98()},{1}} is set

<*[1,K98()]*> is V1() Function-like set

@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

QC-symbols A is non empty set

K49(A) is set

[:NAT,(QC-symbols A):] is non empty set

K113(<*[1,K98()]*>,(@ x)) is V1() Function-like FinSequence-like set

still_not-bound_in x is Element of bool (bound_QC-variables A)

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

QC-variables A is non empty set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is set

bool (bound_QC-variables A) is non empty set

still_not-bound_in ('not' x) is Element of bool (bound_QC-variables A)

still_not-bound_in ('not' x) is Element of bool (bound_QC-variables A)

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

QC-variables A is non empty set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is set

bool (bound_QC-variables A) is non empty set

still_not-bound_in x is Element of bool (bound_QC-variables A)

A is V1() non empty QC-alphabet

QC-WFF A is non empty set

x is Element of QC-WFF A

p is Element of QC-WFF A

x '&' p is Element of QC-WFF A

2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

[2,K98()] is set

{2,K98()} is V24() V25() V26() V27() V28() V29() set

{2} is V24() V25() V26() V27() V28() V29() set

{{2,K98()},{2}} is set

<*[2,K98()]*> is V1() Function-like set

@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

QC-symbols A is non empty set

K49(A) is set

[:NAT,(QC-symbols A):] is non empty set

K113(<*[2,K98()]*>,(@ x)) is V1() Function-like FinSequence-like set

@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

K113(K113(<*[2,K98()]*>,(@ x)),(@ p)) is V1() Function-like FinSequence-like set

still_not-bound_in x is Element of bool (bound_QC-variables A)

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

QC-variables A is non empty set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is set

bool (bound_QC-variables A) is non empty set

still_not-bound_in p is Element of bool (bound_QC-variables A)

(still_not-bound_in x) \/ (still_not-bound_in p) is Element of bool (bound_QC-variables A)

still_not-bound_in (x '&' p) is Element of bool (bound_QC-variables A)

still_not-bound_in (x '&' p) is Element of bool (bound_QC-variables A)

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

QC-variables A is non empty set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is set

bool (bound_QC-variables A) is non empty set

still_not-bound_in x is Element of bool (bound_QC-variables A)

still_not-bound_in p is Element of bool (bound_QC-variables A)

(still_not-bound_in x) \/ (still_not-bound_in p) is Element of bool (bound_QC-variables A)

A is V1() non empty QC-alphabet

QC-variables A is non empty set

QC-symbols A is non empty set

K49(A) is set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

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

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is set

QC-WFF A is non empty set

x is Element of bound_QC-variables A

{x} is set

p is Element of QC-WFF A

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

3 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

[3,K98()] is set

{3,K98()} is V24() V25() V26() V27() V28() V29() set

{3} is V24() V25() V26() V27() V28() V29() set

{{3,K98()},{3}} is set

<*[3,K98()]*> is V1() Function-like set

<*x*> is V1() V4( NAT ) V5( bound_QC-variables A) Function-like FinSequence-like FinSequence of bound_QC-variables A

K113(<*[3,K98()]*>,<*x*>) is V1() Function-like FinSequence-like set

@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

[:NAT,(QC-symbols A):] is non empty set

K113(K113(<*[3,K98()]*>,<*x*>),(@ p)) is V1() Function-like FinSequence-like set

still_not-bound_in p is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is non empty set

still_not-bound_in (All (x,p)) is Element of bool (bound_QC-variables A)

(still_not-bound_in p) \ {x} is Element of bool (bound_QC-variables A)

(still_not-bound_in p) \ {x} is Element of bool (bound_QC-variables A)

still_not-bound_in (All (x,p)) is Element of bool (bound_QC-variables A)

A is V1() non empty QC-alphabet

QC-variables A is non empty set

QC-symbols A is non empty set

K49(A) is set

[:{4,5},(QC-symbols A):] is set

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set

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

bool (QC-variables A) is non empty set

[:{4},(QC-symbols 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

3 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

[3,K98()] is set

{3,K98()} is V24() V25() V26() V27() V28() V29() set

{3} is V24() V25() V26() V27() V28() V29() set

{{3,K98()},{3}} is set

<*[3,K98()]*> is V1() Function-like set

<*x*> is V1() V4( NAT ) V5( bound_QC-variables A) Function-like FinSequence-like FinSequence of bound_QC-variables A

K113(<*[3,K98()]*>,<*x*>) is V1() Function-like FinSequence-like set

@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

[:NAT,(QC-symbols A):] is non empty set

K113(K113(<*[3,K98()]*>,<*x*>),(@ p)) is V1() Function-like FinSequence-like set

still_not-bound_in p is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is non empty set

{x} is set

A is V1() non empty QC-alphabet

QC-WFF A is non empty set

x is Element of QC-WFF A

p is Element of QC-WFF A

x 'or' p is Element of QC-WFF A

'not' x is Element of QC-WFF A

[1,K98()] is set

{1,K98()} is V24() V25() V26() V27() V28() V29() set

{1} is V24() V25() V26() V27() V28() V29() set

{{1,K98()},{1}} is set

<*[1,K98()]*> is V1() Function-like set

@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

QC-symbols A is non empty set

K49(A) is set

[:NAT,(QC-symbols A):] is non empty set

K113(<*[1,K98()]*>,(@ x)) is V1() Function-like FinSequence-like set

'not' p is Element of QC-WFF A

@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

K113(<*[1,K98()]*>,(@ p)) is V1() Function-like FinSequence-like set

('not' x) '&' ('not' p) is Element of QC-WFF A

2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT

[2,K98()] is set

{2,K98()} is V24() V25() V26() V27() V28() V29() set

{2} is V24() V25() V26() V27() V28() V29() set

{{2,K98()},{2}} is set

<*[2,K98()]*> is V1() Function-like set

@ ('not' x) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

K113(<*[2,K98()]*>,(@ ('not' x))) is V1() Function-like FinSequence-like set

@ ('not' p) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

K113(K113(<*[2,K98()]*>,(@ ('not' x))),(@ ('not' p))) is V1() Function-like FinSequence-like set

'not' (('not' x) '&' ('not' p)) is Element of QC-WFF A

@ (('not' x) '&' ('not' p)) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

K113(<*[1,K98()]*>,(@ (('not' x) '&' ('not' p)))) is V1() Function-like FinSequence-like set

A is V1() non empty QC-alphabet

QC-WFF A is non empty set

x is Element of QC-WFF A

p is Element of QC-WFF A

x => p is Element of QC-WFF A

'not' p is Element of QC-WFF A

[1,K98()] is set

{1,K98()} is V24() V25() V26() V27() V28() V29() set

{1} is V24() V25() V26() V27() V28() V29() set

{{1,K98()},{1}} is set

<*[1,K98()]*> is V1() Function-like set

@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]

QC-symbols A is non empty set

K49(A) is set

[:NAT,(QC-symbols A):] is non empty set

K113(