:: SUBSTUT1 semantic presentation

REAL is V45() V46() V47() V51() set

NAT is non empty non trivial V21() V22() V23() V45() V46() V47() V48() V49() V50() V51() non finite cardinal limit_cardinal V94() V95() Element of bool REAL

bool REAL is non empty set

COMPLEX is V45() V51() set

RAT is V45() V46() V47() V48() V51() set

INT is V45() V46() V47() V48() V49() V51() set

NAT is non empty non trivial V21() V22() V23() V45() V46() V47() V48() V49() V50() V51() non finite cardinal limit_cardinal V94() V95() set

bool NAT is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

[:COMPLEX,COMPLEX:] is set

bool [:COMPLEX,COMPLEX:] is non empty set

[:COMPLEX,REAL:] is set

bool [:COMPLEX,REAL:] is non empty set

{} is Function-like functional empty ext-real non positive non negative V21() V22() V23() V25() V26() V27() V45() V46() V47() V48() V49() V50() V51() finite V56() cardinal {} -element FinSequence-membered V94() set

1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

2 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

3 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

Seg 1 is non empty trivial V45() V46() V47() V48() V49() V50() finite 1 -element V94() Element of bool NAT

0 is Function-like functional empty ext-real non positive non negative V21() V22() V23() V25() V26() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() V51() finite V56() cardinal {} -element FinSequence-membered V94() Element of NAT

[0,0] is V15() set

{0,0} is non empty V45() V46() V47() V48() V49() V50() finite V56() V94() set

{0} is non empty trivial V45() V46() V47() V48() V49() V50() finite V56() 1 -element V94() set

{{0,0},{0}} is non empty finite V56() V94() set

<*[0,0]*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V94() set

[1,0] is V15() set

{1,0} is non empty V45() V46() V47() V48() V49() V50() finite V56() V94() set

{1} is non empty trivial V45() V46() V47() V48() V49() V50() finite V56() 1 -element V94() set

{{1,0},{1}} is non empty finite V56() V94() set

<*[1,0]*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V94() set

[2,0] is V15() set

{2,0} is non empty V45() V46() V47() V48() V49() V50() finite V56() V94() set

{2} is non empty trivial V45() V46() V47() V48() V49() V50() finite V56() 1 -element V94() set

{{2,0},{2}} is non empty finite V56() V94() set

<*[2,0]*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V94() set

[3,0] is V15() set

{3,0} is non empty V45() V46() V47() V48() V49() V50() finite V56() V94() set

{3} is non empty trivial V45() V46() V47() V48() V49() V50() finite V56() 1 -element V94() set

{{3,0},{3}} is non empty finite V56() V94() set

<*[3,0]*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V94() set

card NAT is non empty non trivial V21() V22() V23() non finite cardinal set

A is Relation-like non empty QC-alphabet

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

QC-variables A is non empty set

6 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

{6} is non empty trivial V45() V46() V47() V48() V49() V50() finite V56() 1 -element V94() set

[:{6},NAT:] is non empty non trivial non finite set

4 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

5 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

{4,5} is non empty V45() V46() V47() V48() V49() V50() finite V56() V94() set

QC-symbols A is non empty set

proj2 A is set

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

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

bool (QC-variables A) is non empty set

{4} is non empty trivial V45() V46() V47() V48() V49() V50() finite V56() 1 -element V94() set

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

PFuncs ((bound_QC-variables A),(bound_QC-variables A)) is functional non empty set

A is Relation-like non empty QC-alphabet

(A) is 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

proj2 A is set

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

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

bool (QC-variables A) is non empty set

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

PFuncs ((bound_QC-variables A),(bound_QC-variables A)) is functional non empty set

A is Relation-like non empty QC-alphabet

(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

proj2 A is set

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

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

bool (QC-variables A) is non empty set

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

PFuncs ((bound_QC-variables A),(bound_QC-variables A)) is functional non empty set

A is Relation-like non empty QC-alphabet

(A) is functional 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

proj2 A is set

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

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

bool (QC-variables A) is non empty set

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

PFuncs ((bound_QC-variables A),(bound_QC-variables A)) is functional non empty set

S is Relation-like Function-like Element of (A)

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

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

A is Relation-like non empty QC-alphabet

(A) is functional 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

proj2 A is set

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

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

bool (QC-variables A) is non empty set

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

PFuncs ((bound_QC-variables A),(bound_QC-variables A)) is functional non empty set

S is set

SQ is Relation-like Function-like Element of (A)

proj1 SQ is set

SQ . S is set

(A,SQ) is Relation-like bound_QC-variables A -defined bound_QC-variables A -valued Function-like Element of bool [:(bound_QC-variables A),(bound_QC-variables A):]

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

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

dom (A,SQ) is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is non empty set

A is Relation-like non empty QC-alphabet

QC-variables A is non empty set

QC-symbols A is non empty set

proj2 A is set

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

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

(A) is functional non empty 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 non empty set

PFuncs ((bound_QC-variables A),(bound_QC-variables A)) is functional non empty set

S is Relation-like NAT -defined QC-variables A -valued Function-like finite FinSequence-like FinSubsequence-like V94() FinSequence of QC-variables A

len S is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

SQ is Relation-like Function-like Element of (A)

proj1 SQ is set

Seg (len S) is V45() V46() V47() V48() V49() V50() finite len S -element V94() Element of bool NAT

S9 is ext-real V21() V22() V23() V27() finite cardinal V94() set

S . S9 is set

SQ . (S . S9) is set

S9 is set

S9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V94() set

dom S9 is V45() V46() V47() V48() V49() V50() finite V94() Element of bool NAT

proj2 S9 is finite V94() set

S9 is set

l is set

S9 . l is set

l is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

S . l is set

S9 . l is set

SQ . (S . l) is set

l is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

S . l is set

dom S is V45() V46() V47() V48() V49() V50() finite V94() Element of bool NAT

rng S is finite V94() Element of bool (QC-variables A)

S9 . l is set

l is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

S . l is set

S9 . l is set

l is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

S . l is set

S9 . l is set

S9 is Relation-like NAT -defined QC-variables A -valued Function-like finite FinSequence-like FinSubsequence-like V94() FinSequence of QC-variables A

len S9 is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

l is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

S . l is set

S9 . l is set

SQ . (S . l) is set

dom S is V45() V46() V47() V48() V49() V50() finite V94() Element of bool NAT

S9 is Relation-like NAT -defined QC-variables A -valued Function-like finite FinSequence-like FinSubsequence-like V94() FinSequence of QC-variables A

len S9 is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

S9 is Relation-like NAT -defined QC-variables A -valued Function-like finite FinSequence-like FinSubsequence-like V94() FinSequence of QC-variables A

len S9 is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

l is ext-real V21() V22() V23() V27() finite cardinal V94() set

S . l is set

S9 . l is set

SQ . (S . l) is set

S9 . l is set

A is Relation-like non empty QC-alphabet

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

proj2 A is set

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

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

bool (QC-variables A) is non empty set

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

S is Relation-like NAT -defined bound_QC-variables A -valued Function-like finite FinSequence-like FinSubsequence-like V94() FinSequence of bound_QC-variables A

rng S is finite V94() Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is non empty set

A is Relation-like non empty QC-alphabet

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

proj2 A is set

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

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

bool (QC-variables A) is non empty set

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

(A) is functional non empty set

PFuncs ((bound_QC-variables A),(bound_QC-variables A)) is functional non empty set

S is Relation-like NAT -defined bound_QC-variables A -valued Function-like finite FinSequence-like FinSubsequence-like V94() FinSequence of bound_QC-variables A

(A,S) is Relation-like NAT -defined QC-variables A -valued Function-like finite FinSequence-like FinSubsequence-like V94() FinSequence of QC-variables A

SQ is Relation-like Function-like Element of (A)

(A,(A,S),SQ) is Relation-like NAT -defined QC-variables A -valued Function-like finite FinSequence-like FinSubsequence-like V94() FinSequence of QC-variables A

len (A,(A,S),SQ) is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

len (A,S) is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

dom (A,(A,S),SQ) is V45() V46() V47() V48() V49() V50() finite V94() Element of bool NAT

Seg (len (A,S)) is V45() V46() V47() V48() V49() V50() finite len (A,S) -element V94() Element of bool NAT

proj1 SQ is set

S9 is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

(A,S) . S9 is set

(A,(A,S),SQ) . S9 is set

SQ . ((A,S) . S9) is set

rng (A,(A,S),SQ) is finite V94() Element of bool (QC-variables A)

S9 is set

S9 is set

(A,(A,S),SQ) . S9 is set

l is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

(A,S) . l is set

(A,(A,S),SQ) . l is set

SQ . ((A,S) . l) is set

l is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

(A,S) . l is set

rng S is finite V94() Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is non empty set

dom (A,S) is V45() V46() V47() V48() V49() V50() finite V94() Element of bool NAT

rng (A,S) is finite V94() Element of bool (QC-variables A)

(A,(A,S),SQ) . l is set

l is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

(A,S) . l is set

(A,(A,S),SQ) . l is set

l is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

(A,S) . l is set

(A,(A,S),SQ) . l is set

A is Relation-like non empty QC-alphabet

(A) is functional 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

proj2 A is set

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

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

bool (QC-variables A) is non empty set

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

PFuncs ((bound_QC-variables A),(bound_QC-variables A)) is functional non empty set

S is Relation-like Function-like Element of (A)

SQ is set

S | SQ is Relation-like Function-like set

(A,S) is Relation-like bound_QC-variables A -defined bound_QC-variables A -valued Function-like Element of bool [:(bound_QC-variables A),(bound_QC-variables A):]

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

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

(A,S) | SQ is Relation-like bound_QC-variables A -defined bound_QC-variables A -valued Function-like Element of bool [:(bound_QC-variables A),(bound_QC-variables A):]

A is Relation-like non empty QC-alphabet

(A) is functional 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

proj2 A is set

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

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

bool (QC-variables A) is non empty set

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

PFuncs ((bound_QC-variables A),(bound_QC-variables A)) is functional non empty set

S is Function-like functional empty ext-real non positive non negative V21() V22() V23() V25() V26() V27() V45() V46() V47() V48() V49() V50() V51() finite V56() cardinal {} -element FinSequence-membered V94() set

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

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

A is Relation-like non empty QC-alphabet

QC-variables A is non empty set

QC-symbols A is non empty set

proj2 A is set

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

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is non empty 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 non empty set

QC-WFF A is non empty set

(A) is functional non empty set

PFuncs ((bound_QC-variables A),(bound_QC-variables A)) is functional non empty set

S9 is Relation-like Function-like Element of (A)

SQ is Element of QC-WFF A

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

bool (bound_QC-variables A) is non empty set

proj1 S9 is set

S is Element of bound_QC-variables A

{ b

(A,S9, { b

{ b

l is finite V94() set

l /\ { b

s is set

P9 is Element of bound_QC-variables A

S9 . P9 is set

P9 is Element of bound_QC-variables A

S9 . P9 is set

s is finite V94() set

(A,S9,s) is Relation-like Function-like finite V94() Element of (A)

A is Relation-like non empty QC-alphabet

QC-variables A is non empty set

QC-symbols A is non empty set

proj2 A is set

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

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

S is Relation-like NAT -defined QC-variables A -valued Function-like finite FinSequence-like FinSubsequence-like V94() FinSequence of QC-variables A

len S is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

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 non empty set

{ (S . b

bool (bound_QC-variables A) is non empty set

S9 is set

S9 is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

S . S9 is set

A is Relation-like 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

proj2 A is set

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

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

bool (QC-variables A) is non empty set

[:{4},(QC-symbols A):] is non empty 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

S is Element of QC-WFF A

VERUM A is Element of CQC-WFF A

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is non empty set

{} (bound_QC-variables A) is Function-like functional empty proper ext-real non positive non negative V21() V22() V23() V25() V26() V27() V45() V46() V47() V48() V49() V50() V51() finite V56() cardinal {} -element FinSequence-membered V94() Element of bool (bound_QC-variables A)

A is Relation-like non empty QC-alphabet

QC-WFF A is non empty set

VERUM A is Element of CQC-WFF A

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is non empty set

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

proj2 A is set

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

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

bool (QC-variables A) is non empty set

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

bool (bound_QC-variables A) is non empty set

{} (bound_QC-variables A) is Function-like functional empty proper ext-real non positive non negative V21() V22() V23() V25() V26() V27() V45() V46() V47() V48() V49() V50() V51() finite V56() cardinal {} -element FinSequence-membered V94() Element of bool (bound_QC-variables A)

S is Element of QC-WFF A

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

the_arguments_of S is Relation-like NAT -defined QC-variables A -valued Function-like finite FinSequence-like FinSubsequence-like V94() FinSequence of QC-variables A

(A,(the_arguments_of S)) is Element of bool (bound_QC-variables A)

len (the_arguments_of S) is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

{ ((the_arguments_of S) . b

the_argument_of S is Element of QC-WFF A

(A,(the_argument_of S)) is Element of bool (bound_QC-variables A)

the_left_argument_of S is Element of QC-WFF A

(A,(the_left_argument_of S)) is Element of bool (bound_QC-variables A)

the_right_argument_of S is Element of QC-WFF A

(A,(the_right_argument_of S)) is Element of bool (bound_QC-variables A)

(A,(the_left_argument_of S)) \/ (A,(the_right_argument_of S)) is Element of bool (bound_QC-variables A)

the_scope_of S is Element of QC-WFF A

(A,(the_scope_of S)) is Element of bool (bound_QC-variables A)

bound_in S is Element of bound_QC-variables A

{(bound_in S)} is non empty trivial finite 1 -element V94() Element of bool (bound_QC-variables A)

(A,(the_scope_of S)) \/ {(bound_in S)} is non empty Element of bool (bound_QC-variables A)

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

S9 is Element of bool (bound_QC-variables A)

S9 is Element of QC-WFF A

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

l is Element of bool (bound_QC-variables A)

s is Relation-like QC-WFF A -defined bool (bound_QC-variables A) -valued Function-like V29( QC-WFF A, bool (bound_QC-variables A)) Element of bool [:(QC-WFF A),(bool (bound_QC-variables A)):]

l is Element of QC-WFF A

s . l is Element of bool (bound_QC-variables A)

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

H

A is Relation-like non empty QC-alphabet

VERUM A is Element of CQC-WFF A

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is non empty set

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

proj2 A is set

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

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

bool (QC-variables A) is non empty set

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

bool (bound_QC-variables A) is non empty set

{} (bound_QC-variables A) is Function-like functional empty proper ext-real non positive non negative V21() V22() V23() V25() V26() V27() V45() V46() V47() V48() V49() V50() V51() finite V56() cardinal {} -element FinSequence-membered V94() Element of bool (bound_QC-variables A)

A is Relation-like non empty QC-alphabet

QC-WFF A is non empty set

S is Element of QC-WFF A

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

proj2 A is set

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

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

bool (QC-variables A) is non empty set

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

bool (bound_QC-variables A) is non empty set

the_arguments_of S is Relation-like NAT -defined QC-variables A -valued Function-like finite FinSequence-like FinSubsequence-like V94() FinSequence of QC-variables A

(A,(the_arguments_of S)) is Element of bool (bound_QC-variables A)

len (the_arguments_of S) is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

{ ((the_arguments_of S) . b

A is Relation-like non empty QC-alphabet

QC-WFF A is non empty set

S is Element of QC-WFF A

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

proj2 A is set

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

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

bool (QC-variables A) is non empty set

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

bool (bound_QC-variables A) is non empty set

the_argument_of S is Element of QC-WFF A

(A,(the_argument_of S)) is Element of bool (bound_QC-variables A)

A is Relation-like non empty QC-alphabet

QC-WFF A is non empty set

S is Element of QC-WFF A

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

proj2 A is set

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

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

bool (QC-variables A) is non empty set

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

bool (bound_QC-variables A) is non empty set

the_left_argument_of S is Element of QC-WFF A

(A,(the_left_argument_of S)) is Element of bool (bound_QC-variables A)

the_right_argument_of S is Element of QC-WFF A

(A,(the_right_argument_of S)) is Element of bool (bound_QC-variables A)

(A,(the_left_argument_of S)) \/ (A,(the_right_argument_of S)) is Element of bool (bound_QC-variables A)

A is Relation-like non empty QC-alphabet

QC-WFF A is non empty set

S is Element of QC-WFF A

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

proj2 A is set

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

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

bool (QC-variables A) is non empty set

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

bool (bound_QC-variables A) is non empty set

the_scope_of S is Element of QC-WFF A

(A,(the_scope_of S)) is Element of bool (bound_QC-variables A)

bound_in S is Element of bound_QC-variables A

{(bound_in S)} is non empty trivial finite 1 -element V94() Element of bool (bound_QC-variables A)

(A,(the_scope_of S)) \/ {(bound_in S)} is non empty Element of bool (bound_QC-variables A)

A is Relation-like non empty QC-alphabet

QC-WFF A is non empty set

S is Element of QC-WFF A

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

proj2 A is set

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

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

bool (QC-variables A) is non empty set

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

bool (bound_QC-variables A) is non empty set

VERUM A is Element of CQC-WFF A

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is non empty set

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

SQ is Element of QC-WFF A

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

the_argument_of SQ is Element of QC-WFF A

(A,(the_argument_of SQ)) is Element of bool (bound_QC-variables A)

the_left_argument_of SQ is Element of QC-WFF A

(A,(the_left_argument_of SQ)) is Element of bool (bound_QC-variables A)

the_right_argument_of SQ is Element of QC-WFF A

(A,(the_right_argument_of SQ)) is Element of bool (bound_QC-variables A)

the_scope_of SQ is Element of QC-WFF A

(A,(the_scope_of SQ)) is Element of bool (bound_QC-variables A)

the_arguments_of SQ is Relation-like NAT -defined QC-variables A -valued Function-like finite FinSequence-like FinSubsequence-like V94() FinSequence of QC-variables A

len (the_arguments_of SQ) is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

S9 is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

(the_arguments_of SQ) . S9 is set

{ H

{ H

(A,(the_arguments_of SQ)) is Element of bool (bound_QC-variables A)

{ ((the_arguments_of SQ) . b

rng (the_arguments_of SQ) is finite V94() Element of bool (QC-variables A)

(A,(the_left_argument_of SQ)) \/ (A,(the_right_argument_of SQ)) is Element of bool (bound_QC-variables A)

bound_in SQ is Element of bound_QC-variables A

{(bound_in SQ)} is non empty trivial finite 1 -element V94() Element of bool (bound_QC-variables A)

(A,(the_scope_of SQ)) \/ {(bound_in SQ)} is non empty Element of bool (bound_QC-variables A)

A is Relation-like non empty QC-alphabet

QC-WFF A is non empty set

QC-symbols A is non empty set

proj2 A is set

S is Element of QC-WFF A

(A,S) is finite V94() 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 non empty set

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

bool (QC-variables A) is non empty set

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

bool (bound_QC-variables A) is non empty set

{ b

bool (QC-symbols A) is non empty set

S9 is set

S9 is Element of QC-symbols A

x. S9 is Element of bound_QC-variables A

[4,S9] is V15() set

{4,S9} is non empty finite V94() set

{{4,S9},{4}} is non empty finite V56() V94() set

S9 is set

S9 is Element of QC-symbols A

x. S9 is Element of bound_QC-variables A

[4,S9] is V15() set

{4,S9} is non empty finite V94() set

{{4,S9},{4}} is non empty finite V56() V94() set

S9 is Relation-like Function-like set

proj1 S9 is set

S9 | { b

proj2 (S9 | { b

S9 is set

proj1 (S9 | { b

l is set

(S9 | { b

S9 . l is set

l is Element of QC-symbols A

x. l is Element of bound_QC-variables A

[4,l] is V15() set

{4,l} is non empty finite V94() set

{{4,l},{4}} is non empty finite V56() V94() set

s is Element of QC-symbols A

x. s is Element of bound_QC-variables A

[4,s] is V15() set

{4,s} is non empty finite V94() set

{{4,s},{4}} is non empty finite V56() V94() set

S9 is set

l is set

S9 . S9 is set

S9 . l is set

l is Element of QC-symbols A

x. l is Element of bound_QC-variables A

[4,l] is V15() set

{4,l} is non empty finite V94() set

{{4,l},{4}} is non empty finite V56() V94() set

s is Element of QC-symbols A

x. s is Element of bound_QC-variables A

[4,s] is V15() set

{4,s} is non empty finite V94() set

{{4,s},{4}} is non empty finite V56() V94() set

proj1 (S9 | { b

S9 is Element of bool (QC-symbols A)

S9 | S9 is Relation-like Function-like set

proj1 (S9 | S9) is set

l is set

l is set

S9 /\ (QC-symbols A) is Element of bool (QC-symbols A)

A is Relation-like non empty QC-alphabet

(A) is functional 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

proj2 A is set

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

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

bool (QC-variables A) is non empty set

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

PFuncs ((bound_QC-variables A),(bound_QC-variables A)) is functional non empty set

S is Relation-like Function-like finite V94() Element of (A)

proj2 S is finite V94() set

{ b

bool (QC-symbols A) is non empty set

S9 is set

S9 is Element of QC-symbols A

x. S9 is Element of bound_QC-variables A

[4,S9] is V15() set

{4,S9} is non empty finite V94() set

{{4,S9},{4}} is non empty finite V56() V94() set

S9 is set

S9 is Element of QC-symbols A

x. S9 is Element of bound_QC-variables A

[4,S9] is V15() set

{4,S9} is non empty finite V94() set

{{4,S9},{4}} is non empty finite V56() V94() set

S9 is Relation-like Function-like set

proj1 S9 is set

S9 | { b

proj2 (S9 | { b

S9 is set

proj1 (S9 | { b

l is set

(S9 | { b

S9 . l is set

l is Element of QC-symbols A

x. l is Element of bound_QC-variables A

[4,l] is V15() set

{4,l} is non empty finite V94() set

{{4,l},{4}} is non empty finite V56() V94() set

s is Element of QC-symbols A

x. s is Element of bound_QC-variables A

[4,s] is V15() set

{4,s} is non empty finite V94() set

{{4,s},{4}} is non empty finite V56() V94() set

S9 is set

l is set

S9 . S9 is set

S9 . l is set

l is Element of QC-symbols A

x. l is Element of bound_QC-variables A

[4,l] is V15() set

{4,l} is non empty finite V94() set

{{4,l},{4}} is non empty finite V56() V94() set

s is Element of QC-symbols A

x. s is Element of bound_QC-variables A

[4,s] is V15() set

{4,s} is non empty finite V94() set

{{4,s},{4}} is non empty finite V56() V94() set

proj1 (S9 | { b

S9 is Element of bool (QC-symbols A)

S9 | S9 is Relation-like Function-like set

proj1 (S9 | S9) is set

l is set

l is set

S9 /\ (QC-symbols A) is Element of bool (QC-symbols A)

A is set

card A is V21() V22() V23() cardinal set

S is set

card S is V21() V22() V23() cardinal set

S \ A is Element of bool S

bool S is non empty set

A is Relation-like non empty QC-alphabet

QC-WFF A is non empty set

(A) is functional 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

proj2 A is set

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

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

bool (QC-variables A) is non empty set

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

PFuncs ((bound_QC-variables A),(bound_QC-variables A)) is functional non empty set

S is Element of QC-WFF A

(A,S) is finite V94() Element of bool (QC-symbols A)

bool (QC-symbols A) is non empty set

(A,S) is finite V94() Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is non empty set

{ b

SQ is Relation-like Function-like finite V94() Element of (A)

(A,SQ) is finite V94() Element of bool (QC-symbols A)

proj2 SQ is finite V94() set

{ b

(A,S) \/ (A,SQ) is finite V94() Element of bool (QC-symbols A)

NAT \ ((A,S) \/ (A,SQ)) is V45() V46() V47() V48() V49() V50() Element of bool REAL

card ((A,S) \/ (A,SQ)) is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

card NAT is non empty non trivial V21() V22() V23() non finite cardinal set

A is Relation-like non empty QC-alphabet

(A) is functional 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

proj2 A is set

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

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

bool (QC-variables A) is non empty set

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

PFuncs ((bound_QC-variables A),(bound_QC-variables A)) is functional non empty set

QC-WFF A is non empty set

SQ is Element of QC-WFF A

S is Relation-like Function-like finite V94() Element of (A)

(A,SQ,S) is non empty Element of bool (QC-symbols A)

bool (QC-symbols A) is non empty set

(A,SQ) is finite V94() Element of bool (QC-symbols A)

(A,SQ) is finite V94() Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is non empty set

{ b

(A,S) is finite V94() Element of bool (QC-symbols A)

proj2 S is finite V94() set

{ b

(A,SQ) \/ (A,S) is finite V94() Element of bool (QC-symbols A)

NAT \ ((A,SQ) \/ (A,S)) is V45() V46() V47() V48() V49() V50() Element of bool REAL

the Element of (A,SQ,S) is Element of (A,SQ,S)

A is Relation-like non empty QC-alphabet

QC-variables A is non empty set

QC-symbols A is non empty set

proj2 A is set

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

[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is non empty 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 non empty set

QC-WFF A is non empty set

(A) is functional non empty set

PFuncs ((bound_QC-variables A),(bound_QC-variables A)) is functional non empty set

S9 is Relation-like Function-like finite V94() Element of (A)

S is Element of bound_QC-variables A

SQ is Element of QC-WFF A

All (S,SQ) is Element of QC-WFF A

<*S*> is Relation-like NAT -defined bound_QC-variables A -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V94() FinSequence of bound_QC-variables A

<*[3,0]*> ^ <*S*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like V94() set

1 + 1 is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

@ SQ is Relation-like NAT -defined [:NAT,(QC-symbols A):] -valued Function-like finite FinSequence-like FinSubsequence-like V94() FinSequence of [:NAT,(QC-symbols A):]

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

(<*[3,0]*> ^ <*S*>) ^ (@ SQ) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like V94() set

proj2 S9 is finite V94() set

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

(A,S9,SQ) is Element of QC-symbols A

(A,SQ,S9) is non empty Element of bool (QC-symbols A)

bool (QC-symbols A) is non empty set

(A,SQ) is finite V94() Element of bool (QC-symbols A)

(A,SQ) is finite V94() Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is non empty set

{ b

(A,S9) is finite V94() Element of bool (QC-symbols A)

{ b

(A,SQ) \/ (A,S9) is finite V94() Element of bool (QC-symbols A)

NAT \ ((A,SQ) \/ (A,S9)) is V45() V46() V47() V48() V49() V50() Element of bool REAL

the Element of (A,SQ,S9) is Element of (A,SQ,S9)

x. (A,S9,SQ) is Element of bound_QC-variables A

[4,(A,S9,SQ)] is V15() set

{4,(A,S9,SQ)} is non empty finite V94() set

{{4,(A,S9,SQ)},{4}} is non empty finite V56() V94() set

[S,(x. (A,S9,SQ))] is V15() Element of [:(bound_QC-variables A),(bound_QC-variables A):]

{S,(x. (A,S9,SQ))} is non empty finite V94() set

{S} is non empty trivial finite 1 -element V94() set

{{S,(x. (A,S9,SQ))},{S}} is non empty finite V56() V94() set

{[S,(x. (A,S9,SQ))]} is Relation-like bound_QC-variables A -defined bound_QC-variables A -valued Function-like constant non empty trivial finite 1 -element V94() Element of bool [:(bound_QC-variables A),(bound_QC-variables A):]

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

S9 \/ {[S,(x. (A,S9,SQ))]} is non empty finite V94() set

[S,S] is V15() Element of [:(bound_QC-variables A),(bound_QC-variables A):]

{S,S} is non empty finite V94() set

{{S,S},{S}} is non empty finite V56() V94() set

{[S,S]} is Relation-like bound_QC-variables A -defined bound_QC-variables A -valued Function-like constant non empty trivial finite 1 -element V94() Element of bool [:(bound_QC-variables A),(bound_QC-variables A):]

S9 \/ {[S,S]} is non empty finite V94() set

l is Relation-like Function-like Element of (A)

(A,S,(All (S,SQ)),l) is Relation-like Function-like finite V94() Element of (A)

still_not-bound_in (All (S,SQ)) is Element of bool (bound_QC-variables A)

proj1 l is set

{ b

(A,l, { b

l is Relation-like Function-like Element of (A)

(A,S,(All (S,SQ)),l) is Relation-like Function-like finite V94() Element of (A)

still_not-bound_in (All (S,SQ)) is Element of bool (bound_QC-variables A)

proj1 l is set

{ b

(A,l, { b

proj1 S9 is finite V94() set

S9 is Relation-like set

proj1 S9 is set

(proj1 S9) /\ (proj1 S9) is finite V94() set

s is set

{S} is non empty trivial finite 1 -element V94() Element of bool (bound_QC-variables A)

P9 is Element of bound_QC-variables A

l . P9 is set

(A,S9) is Relation-like bound_QC-variables A -defined bound_QC-variables A -valued Function-like Element of bool [:(bound_QC-variables A),(bound_QC-variables A):]

dom (A,S9) is Element of bool (bound_QC-variables A)

l is Relation-like Function-like set

proj1 l is set

(dom (A,S9)) /\ (proj1 l) is Element of bool (bound_QC-variables A)

l is set

(A,S9) . l is set

l . l is set

(A,S9) \/ l is set

l is Relation-like Function-like set

s is Relation-like bound_QC-variables A -defined bound_QC-variables A -valued Element of bool [:(bound_QC-variables A),(bound_QC-variables A):]

(A,S9) \/ s is Relation-like bound_QC-variables A -defined bound_QC-variables A -valued Element of bool [:(bound_QC-variables A),(bound_QC-variables A):]

l is Relation-like Function-like Element of (A)

(A,S,(All (S,SQ)),l) is Relation-like Function-like finite V94() Element of (A)

proj1 l is set

{ b

(A,l, { b

l is Relation-like Function-like Element of (A)

(A,S,(All (S,SQ)),l) is Relation-like Function-like finite V94() Element of (A)

proj1 l is set

{ b

(A,l, { b

S9 is Relation-like set

proj1 S9 is set

(proj1 S9) /\ (proj1 S9) is finite V94() set

s is set

P9 is Element of bound_QC-variables A

l . P9 is set

l is Relation-like Function-like set

proj1 l is set

(dom (A,S9)) /\ (proj1 l) is Element of bool (bound_QC-variables A)

l is set

(A,S9) . l is set

l . l is set

(A,S9) \/ l is set

l is Relation-like Function-like set

s is Relation-like bound_QC-variables A -defined bound_QC-variables A -valued Element of bool [:(bound_QC-variables A),(bound_QC-variables A):]

(A,S9) \/ s is Relation-like bound_QC-variables A -defined bound_QC-variables A -valued Element of bool [:(bound_QC-variables A),(bound_QC-variables A):]

A is Relation-like non empty QC-alphabet

QC-WFF A is non empty set

(A) is functional 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

proj2 A is set

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

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

bool (QC-variables A) is non empty set

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

PFuncs ((bound_QC-variables A),(bound_QC-variables A)) is functional non empty set

A is Relation-like non empty QC-alphabet

QC-WFF A is non empty set

(A) is functional 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

proj2 A is set

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

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

bool (QC-variables A) is non empty set

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

PFuncs ((bound_QC-variables A),(bound_QC-variables A)) is functional non empty set

S is set

SQ is set

S9 is set

S9 is Element of QC-WFF A

l is Relation-like Function-like Element of (A)

[S9,l] is V15() Element of [:(QC-WFF A),(A):]

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

{S9,l} is non empty finite V94() set

{S9} is non empty trivial finite 1 -element V94() set

{{S9,l},{S9}} is non empty finite V56() V94() set

S9 is Element of QC-WFF A

l is Relation-like Function-like Element of (A)

[S9,l] is V15() Element of [:(QC-WFF A),(A):]

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

{S9,l} is non empty finite V94() set

{S9} is non empty trivial finite 1 -element V94() set

{{S9,l},{S9}} is non empty finite V56() V94() set

l is Element of QC-WFF A

s is Relation-like Function-like Element of (A)

[l,s] is V15() Element of [:(QC-WFF A),(A):]

{l,s} is non empty finite V94() set

{l} is non empty trivial finite 1 -element V94() set

{{l,s},{l}} is non empty finite V56() V94() set

l is Element of QC-WFF A

s is Relation-like Function-like Element of (A)

[l,s] is V15() Element of [:(QC-WFF A),(A):]

{l,s} is non empty finite V94() set

{l} is non empty trivial finite 1 -element V94() set

{{l,s},{l}} is non empty finite V56() V94() set

bound_in S9 is Element of bound_QC-variables A

the_scope_of S9 is Element of QC-WFF A

(A,(bound_in S9),S9,l) is Relation-like Function-like finite V94() Element of (A)

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

bool (bound_QC-variables A) is non empty set

proj1 l is set

{ b

(A,l, { b

(A,(bound_in S9),(the_scope_of S9),(A,(bound_in S9),S9,l)) is Relation-like Function-like Element of (A)

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

S is Relation-like Function-like set

SQ is set

S9 is set

S9 is set

[S9,S9] is V15() set

{S9,S9} is non empty finite V94() set

{S9} is non empty trivial finite 1 -element V94() set

{{S9,S9},{S9}} is non empty finite V56() V94() set

l is Element of QC-WFF A

l is Relation-like Function-like Element of (A)

[l,l] is V15() Element of [:(QC-WFF A),(A):]

{l,l} is non empty finite V94() set

{l} is non empty trivial finite 1 -element V94() set

{{l,l},{l}} is non empty finite V56() V94() set

S9 is Element of QC-WFF A

S9 is Relation-like Function-like Element of (A)

[S9,S9] is V15() Element of [:(QC-WFF A),(A):]

{S9,S9} is non empty finite V94() set

{S9} is non empty trivial finite 1 -element V94() set

{{S9,S9},{S9}} is non empty finite V56() V94() set

l is set

[[S9,S9],l] is V15() set

{[S9,S9],l} is non empty finite V94() set

{[S9,S9]} is Function-like non empty trivial finite 1 -element V94() set

{{[S9,S9],l},{[S9,S9]}} is non empty finite V56() V94() set

SQ is set

S9 is set

S9 is Element of QC-WFF A

l is Relation-like Function-like Element of (A)

[S9,l] is V15() Element of [:(QC-WFF A),(A):]

{S9,l} is non empty finite V94() set

{S9} is non empty trivial finite 1 -element V94() set

{{S9,l},{S9}} is non empty finite V56() V94() set

l is set

[[S9,l],l] is V15() set

{[S9,l],l} is non empty finite V94() set

{[S9,l]} is Function-like non empty trivial finite 1 -element V94() set

{{[S9,l],l},{[S9,l]}} is non empty finite V56() V94() set

S is Relation-like Function-like set

SQ is Relation-like Function-like set

S9 is set

S9 is Element of QC-WFF A

l is Relation-like Function-like Element of (A)

[S9,l] is V15() Element of [:(QC-WFF A),(A):]

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

{S9,l} is non empty finite V94() set

{S9} is non empty trivial finite 1 -element V94() set

{{S9,l},{S9}} is non empty finite V56() V94() set

l is set

[[S9,l],l] is V15() set

{[S9,l],l} is non empty finite V94() set

{[S9,l]} is Function-like non empty trivial finite 1 -element V94() set

{{[S9,l],l},{[S9,l]}} is non empty finite V56() V94() set

S9 is Element of QC-WFF A

l is Relation-like Function-like Element of (A)

[S9,l] is V15() Element of [:(QC-WFF A),(A):]

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

{S9,l} is non empty finite V94() set

{S9} is non empty trivial finite 1 -element V94() set

{{S9,l},{S9}} is non empty finite V56() V94() set

l is set

[[S9,l],l] is V15() set

{[S9,l],l} is non empty finite V94() set

{[S9,l]} is Function-like non empty trivial finite 1 -element V94() set

{{[S9,l],l},{[S9,l]}} is non empty finite V56() V94() set

[:NAT,NAT:] is non empty non trivial non finite set

[:NAT,[:NAT,NAT:]:] is non empty non trivial non finite set

bool [:NAT,[:NAT,NAT:]:] is non empty non trivial non finite set

[0,0] is V15() Element of [:NAT,NAT:]

<*[0,0]*> is Relation-like NAT -defined [:NAT,NAT:] -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V94() FinSequence of [:NAT,NAT:]

[1,0] is V15() Element of [:NAT,NAT:]

<*[1,0]*> is Relation-like NAT -defined [:NAT,NAT:] -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V94() FinSequence of [:NAT,NAT:]

[2,0] is V15() Element of [:NAT,NAT:]

<*[2,0]*> is Relation-like NAT -defined [:NAT,NAT:] -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V94() FinSequence of [:NAT,NAT:]

[3,0] is V15() Element of [:NAT,NAT:]

<*[3,0]*> is Relation-like NAT -defined [:NAT,NAT:] -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V94() FinSequence of [:NAT,NAT:]

A is Relation-like non empty QC-alphabet

QC-WFF A is non empty set

(A) is functional 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

proj2 A is set

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

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

bool (QC-variables A) is non empty set

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

PFuncs ((bound_QC-variables A),(bound_QC-variables A)) is functional non empty set

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

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

[:NAT,(QC-symbols A):] * is functional non empty FinSequence-membered set

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

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

QC-pred_symbols A is non empty set

7 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

{ [b

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

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

(A) is Relation-like Function-like set

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

S is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

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

SQ is Element of S -ary_QC-pred_symbols A

<*SQ*> is Relation-like NAT -defined S -ary_QC-pred_symbols A -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V94() FinSequence of S -ary_QC-pred_symbols A

S9 is Relation-like NAT -defined QC-variables A -valued Function-like finite S -element FinSequence-like FinSubsequence-like V94() FinSequence of QC-variables A

<*SQ*> ^ S9 is Relation-like NAT -defined Function-like non empty finite 1 + S -element FinSequence-like FinSubsequence-like V94() set

1 + S is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

S9 is Relation-like Function-like Element of (A)

[(<*SQ*> ^ S9),S9] is V15() set

{(<*SQ*> ^ S9),S9} is functional non empty finite V94() set

{(<*SQ*> ^ S9)} is functional non empty trivial finite V56() 1 -element V92() V94() set

{{(<*SQ*> ^ S9),S9},{(<*SQ*> ^ S9)}} is non empty finite V56() V94() set

SQ ! S9 is Element of QC-WFF A

VERUM A is Element of CQC-WFF A

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is non empty set

S is Relation-like Function-like Element of (A)

[<*[0,0]*>,S] is V15() Element of [:(bool [:NAT,[:NAT,NAT:]:]),(A):]

[:(bool [:NAT,[:NAT,NAT:]:]),(A):] is non empty non trivial non finite set

{<*[0,0]*>,S} is functional non empty finite V94() set

{<*[0,0]*>} is functional non empty trivial finite V56() 1 -element V92() V94() set

{{<*[0,0]*>,S},{<*[0,0]*>}} is non empty finite V56() V94() set

S is Relation-like NAT -defined [:NAT,(QC-symbols A):] -valued Function-like finite FinSequence-like FinSubsequence-like V94() FinSequence of [:NAT,(QC-symbols A):]

<*[1,0]*> ^ S is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like V94() set

SQ is Relation-like Function-like Element of (A)

[S,SQ] is V15() Element of [:(bool [:NAT,[:NAT,(QC-symbols A):]:]),(A):]

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

{S,SQ} is functional non empty finite V94() set

{S} is functional non empty trivial finite V56() 1 -element V92() V94() set

{{S,SQ},{S}} is non empty finite V56() V94() set

[(<*[1,0]*> ^ S),SQ] is V15() set

{(<*[1,0]*> ^ S),SQ} is functional non empty finite V94() set

{(<*[1,0]*> ^ S)} is functional non empty trivial finite V56() 1 -element V92() V94() set

{{(<*[1,0]*> ^ S),SQ},{(<*[1,0]*> ^ S)}} is non empty finite V56() V94() set

S9 is set

l is set

[S9,l] is V15() set

{S9,l} is non empty finite V94() set

{S9} is non empty trivial finite 1 -element V94() set

{{S9,l},{S9}} is non empty finite V56() V94() set

S9 is Element of QC-WFF A

'not' S9 is Element of QC-WFF A

@ S9 is Relation-like NAT -defined [:NAT,(QC-symbols A):] -valued Function-like finite FinSequence-like FinSubsequence-like V94() FinSequence of [:NAT,(QC-symbols A):]

<*[1,0]*> ^ (@ S9) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like V94() set

<*[1,0]*> ^ (@ S9) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like V94() set

S is Relation-like NAT -defined [:NAT,(QC-symbols A):] -valued Function-like finite FinSequence-like FinSubsequence-like V94() FinSequence of [:NAT,(QC-symbols A):]

SQ is Relation-like NAT -defined [:NAT,(QC-symbols A):] -valued Function-like finite FinSequence-like FinSubsequence-like V94() FinSequence of [:NAT,(QC-symbols A):]

<*[2,0]*> ^ S is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like V94() set

(<*[2,0]*> ^ S) ^ SQ is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like V94() set

S9 is Relation-like Function-like Element of (A)

[S,S9] is V15() Element of [:(bool [:NAT,[:NAT,(QC-symbols A):]:]),(A):]

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

{S,S9} is functional non empty finite V94() set

{S} is functional non empty trivial finite V56() 1 -element V92() V94() set

{{S,S9},{S}} is non empty finite V56() V94() set

[SQ,S9] is V15() Element of [:(bool [:NAT,[:NAT,(QC-symbols A):]:]),(A):]

{SQ,S9} is functional non empty finite V94() set

{SQ} is functional non empty trivial finite V56() 1 -element V92() V94() set

{{SQ,S9},{SQ}} is non empty finite V56() V94() set

[((<*[2,0]*> ^ S) ^ SQ),S9] is V15() set

{((<*[2,0]*> ^ S) ^ SQ),S9} is functional non empty finite V94() set

{((<*[2,0]*> ^ S) ^ SQ)} is functional non empty trivial finite V56() 1 -element V92() V94() set

{{((<*[2,0]*> ^ S) ^ SQ),S9},{((<*[2,0]*> ^ S) ^ SQ)}} is non empty finite V56() V94() set

l is set

l is set

[l,l] is V15() set

{l,l} is non empty finite V94() set

{l} is non empty trivial finite 1 -element V94() set

{{l,l},{l}} is non empty finite V56() V94() set

l is set

s is set

[l,s] is V15() set

{l,s} is non empty finite V94() set

{l} is non empty trivial finite 1 -element V94() set

{{l,s},{l}