:: 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₁ where b₁ is Element of bound_QC-variables A : ( b₁ in still_not-bound_in SQ & b₁ is Element of proj1 S9 & not b₁ = S & not b₁ = S9 . b₁ ) } is set
(A,S9, { b₁ where b₁ is Element of bound_QC-variables A : ( b₁ in still_not-bound_in SQ & b₁ is Element of proj1 S9 & not b₁ = S & not b₁ = S9 . b₁ ) } ) is Relation-like Function-like Element of (A)
{ b₁ where b₁ is Element of bound_QC-variables A : ( b₁ is Element of proj1 S9 & not b₁ = S & not b₁ = S9 . b₁ ) } is set
l is finite V94() set
l /\ { b₁ where b₁ is Element of bound_QC-variables A : ( b₁ is Element of proj1 S9 & not b₁ = S & not b₁ = S9 . b₁ ) } is finite V94() set
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₁) where b₁ is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT : ( 1 <= b₁ & b₁ <= len S & S . b₁ in bound_QC-variables A ) } is set
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₁) where b₁ is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT : ( 1 <= b₁ & b₁ <= len (the_arguments_of S) & (the_arguments_of S) . b₁ in bound_QC-variables A ) } is set
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₂( 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
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₁) where b₁ is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT : ( 1 <= b₁ & b₁ <= len (the_arguments_of S) & (the_arguments_of S) . b₁ in bound_QC-variables A ) } is set
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₁(b₁) where b₁ is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT : S₃[b₁] } is set
{ H₁(b₁) where b₁ is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT : S₂[b₁] } is set
(A,(the_arguments_of SQ)) is Element of bool (bound_QC-variables A)
{ ((the_arguments_of SQ) . b₁) where b₁ is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT : ( 1 <= b₁ & b₁ <= len (the_arguments_of SQ) & (the_arguments_of SQ) . b₁ in bound_QC-variables A ) } is set
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₁ where b₁ is Element of QC-symbols A : x. b₁ in (A,S) } is set
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₁ where b₁ is Element of QC-symbols A : x. b₁ in (A,S) } is Relation-like Function-like set
proj2 (S9 | { b₁ where b₁ is Element of QC-symbols A : x. b₁ in (A,S) } ) is set
S9 is set
proj1 (S9 | { b₁ where b₁ is Element of QC-symbols A : x. b₁ in (A,S) } ) is set
l is set
(S9 | { b₁ where b₁ is Element of QC-symbols A : x. b₁ in (A,S) } ) . l 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
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₁ where b₁ is Element of QC-symbols A : x. b₁ in (A,S) } ) is set
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₁ where b₁ is Element of QC-symbols A : x. b₁ in proj2 S } is set
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₁ where b₁ is Element of QC-symbols A : x. b₁ in proj2 S } is Relation-like Function-like set
proj2 (S9 | { b₁ where b₁ is Element of QC-symbols A : x. b₁ in proj2 S } ) is set
S9 is set
proj1 (S9 | { b₁ where b₁ is Element of QC-symbols A : x. b₁ in proj2 S } ) is set
l is set
(S9 | { b₁ where b₁ is Element of QC-symbols A : x. b₁ in proj2 S } ) . l 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
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₁ where b₁ is Element of QC-symbols A : x. b₁ in proj2 S } ) is set
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₁ where b₁ is Element of QC-symbols A : x. b₁ in (A,S) } is set
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₁ where b₁ is Element of QC-symbols A : x. b₁ in proj2 SQ } is set
(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₁ where b₁ is Element of QC-symbols A : x. b₁ in (A,SQ) } is set
(A,S) is finite V94() Element of bool (QC-symbols A)
proj2 S is finite V94() set
{ b₁ where b₁ is Element of QC-symbols A : x. b₁ in proj2 S } is set
(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₁ where b₁ is Element of QC-symbols A : x. b₁ in (A,SQ) } is set
(A,S9) is finite V94() Element of bool (QC-symbols A)
{ b₁ where b₁ is Element of QC-symbols A : x. b₁ in proj2 S9 } is set
(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₁ where b₁ is Element of bound_QC-variables A : ( b₁ in still_not-bound_in (All (S,SQ)) & b₁ is Element of proj1 l & not b₁ = S & not b₁ = l . b₁ ) } is set
(A,l, { b₁ where b₁ is Element of bound_QC-variables A : ( b₁ in still_not-bound_in (All (S,SQ)) & b₁ is Element of proj1 l & not b₁ = S & not b₁ = l . b₁ ) } ) is Relation-like Function-like Element of (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)
still_not-bound_in (All (S,SQ)) is Element of bool (bound_QC-variables A)
proj1 l is set
{ b₁ where b₁ is Element of bound_QC-variables A : ( b₁ in still_not-bound_in (All (S,SQ)) & b₁ is Element of proj1 l & not b₁ = S & not b₁ = l . b₁ ) } is set
(A,l, { b₁ where b₁ is Element of bound_QC-variables A : ( b₁ in still_not-bound_in (All (S,SQ)) & b₁ is Element of proj1 l & not b₁ = S & not b₁ = l . b₁ ) } ) is Relation-like Function-like Element of (A)
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₁ where b₁ is Element of bound_QC-variables A : ( b₁ in still_not-bound_in (All (S,SQ)) & b₁ is Element of proj1 l & not b₁ = S & not b₁ = l . b₁ ) } is set
(A,l, { b₁ where b₁ is Element of bound_QC-variables A : ( b₁ in still_not-bound_in (All (S,SQ)) & b₁ is Element of proj1 l & not b₁ = S & not b₁ = l . b₁ ) } ) is Relation-like Function-like Element of (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₁ where b₁ is Element of bound_QC-variables A : ( b₁ in still_not-bound_in (All (S,SQ)) & b₁ is Element of proj1 l & not b₁ = S & not b₁ = l . b₁ ) } is set
(A,l, { b₁ where b₁ is Element of bound_QC-variables A : ( b₁ in still_not-bound_in (All (S,SQ)) & b₁ is Element of proj1 l & not b₁ = S & not b₁ = l . b₁ ) } ) is Relation-like Function-like Element of (A)
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₁ where b₁ is Element of bound_QC-variables A : ( b₁ in still_not-bound_in S9 & b₁ is Element of proj1 l & not b₁ = bound_in S9 & not b₁ = l . b₁ ) } is set
(A,l, { b₁ where b₁ is Element of bound_QC-variables A : ( b₁ in still_not-bound_in S9 & b₁ is Element of proj1 l & not b₁ = bound_in S9 & not b₁ = l . b₁ ) } ) is Relation-like Function-like Element of (A)
(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₁,b₂] where b₁ is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT , b₂ is Element of QC-symbols A : 7 <= b₁ } is set
[: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₁ where b₁ is Element of QC-pred_symbols A : the_arity_of b₁ = S } is set
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}