REAL is set
NAT is non empty non trivial V8() V9() V10() non finite V40() V41() Element of bool REAL
bool REAL is non empty set
NAT is non empty non trivial V8() V9() V10() non finite V40() V41() set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
{} is set
the ext-real non positive non negative V4() empty V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered set is ext-real non positive non negative V4() empty V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered set
1 is ext-real positive non negative V4() non empty V8() V9() V10() V14() V15() finite V40() Element of NAT
2 is ext-real positive non negative V4() non empty V8() V9() V10() V14() V15() finite V40() Element of NAT
3 is ext-real positive non negative V4() non empty V8() V9() V10() V14() V15() finite V40() Element of NAT
0 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
9 is ext-real positive non negative V4() non empty V8() V9() V10() V14() V15() finite V40() Element of NAT
4 is ext-real positive non negative V4() non empty V8() V9() V10() V14() V15() finite V40() Element of NAT
5 is ext-real positive non negative V4() non empty V8() V9() V10() V14() V15() finite V40() Element of NAT
6 is ext-real positive non negative V4() non empty V8() V9() V10() V14() V15() finite V40() Element of NAT
7 is ext-real positive non negative V4() non empty V8() V9() V10() V14() V15() finite V40() Element of NAT
8 is ext-real positive non negative V4() non empty V8() V9() V10() V14() V15() finite V40() Element of NAT
Al is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
Al + 1 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
{ b1 where b1 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT : b1 <= Al + 1 } is set
{ b1 where b1 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT : b1 <= Al } is set
{(Al + 1)} is non empty trivial finite V39() V42(1) set
{ b1 where b1 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT : b1 <= Al } \/ {(Al + 1)} is set
s is set
y is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
s is set
y is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
y is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
{ b1 where b1 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT : b1 <= a1 } is set
{ b1 where b1 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT : b1 <= 0 } is set
{0} is non empty trivial finite V39() V42(1) set
Al is set
s is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
Al is set
Al is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
{ b1 where b1 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT : b1 <= Al } is set
Al + 1 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
{ b1 where b1 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT : b1 <= Al + 1 } is set
{(Al + 1)} is non empty trivial finite V39() V42(1) set
{ b1 where b1 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT : b1 <= Al } \/ {(Al + 1)} is set
Al is set
s is set
y is set
[:s,y:] is set
Al is set
s is set
y is set
[:y,s:] is set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
s is Element of bool (CQC-WFF Al)
y is Element of bool (CQC-WFF Al)
s /\ y is Element of bool (CQC-WFF Al)
VERUM Al is Element of CQC-WFF Al
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
x is Element of CQC-WFF Al
'not' x is Element of CQC-WFF Al
('not' x) => x is Element of CQC-WFF Al
(('not' x) => x) => x is Element of CQC-WFF Al
still_not-bound_in x is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
x is Element of CQC-WFF Al
('not' x) => x is Element of CQC-WFF Al
x => (('not' x) => x) is Element of CQC-WFF Al
x => x is Element of CQC-WFF Al
x '&' x is Element of CQC-WFF Al
x '&' x is Element of CQC-WFF Al
(x '&' x) => (x '&' x) is Element of CQC-WFF Al
Z is Element of CQC-WFF Al
x '&' Z is Element of CQC-WFF Al
'not' (x '&' Z) is Element of CQC-WFF Al
x '&' Z is Element of CQC-WFF Al
'not' (x '&' Z) is Element of CQC-WFF Al
('not' (x '&' Z)) => ('not' (x '&' Z)) is Element of CQC-WFF Al
(x => x) => (('not' (x '&' Z)) => ('not' (x '&' Z))) is Element of CQC-WFF Al
Y is Element of QC-WFF Al
still_not-bound_in Y is Element of bool (bound_QC-variables Al)
n is Element of bound_QC-variables Al
All (n,x) is Element of CQC-WFF Al
(All (n,x)) => x is Element of CQC-WFF Al
All (n,x) is Element of CQC-WFF Al
x => (All (n,x)) is Element of CQC-WFF Al
Y . n is Element of QC-WFF Al
y is Element of bound_QC-variables Al
Y . y is Element of QC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
s is Element of bool (CQC-WFF Al)
y is set
x is set
x is Element of bool (CQC-WFF Al)
x is Element of CQC-WFF Al
Z is Element of bool (CQC-WFF Al)
Y is Element of CQC-WFF Al
y is Element of bool (CQC-WFF Al)
x is Element of bool (CQC-WFF Al)
x is set
Z is Element of CQC-WFF Al
Y is Element of bool (CQC-WFF Al)
Z is Element of CQC-WFF Al
Y is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
VERUM Al is Element of CQC-WFF Al
s is Element of bool (CQC-WFF Al)
(Al,s) is Element of bool (CQC-WFF Al)
y is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
s is Element of bool (CQC-WFF Al)
(Al,s) is Element of bool (CQC-WFF Al)
y is Element of CQC-WFF Al
'not' y is Element of CQC-WFF Al
('not' y) => y is Element of CQC-WFF Al
(('not' y) => y) => y is Element of CQC-WFF Al
x is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
s is Element of bool (CQC-WFF Al)
(Al,s) is Element of bool (CQC-WFF Al)
y is Element of CQC-WFF Al
'not' y is Element of CQC-WFF Al
x is Element of CQC-WFF Al
('not' y) => x is Element of CQC-WFF Al
y => (('not' y) => x) is Element of CQC-WFF Al
x is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
s is Element of bool (CQC-WFF Al)
(Al,s) is Element of bool (CQC-WFF Al)
y is Element of CQC-WFF Al
x is Element of CQC-WFF Al
y => x is Element of CQC-WFF Al
x is Element of CQC-WFF Al
x '&' x is Element of CQC-WFF Al
'not' (x '&' x) is Element of CQC-WFF Al
y '&' x is Element of CQC-WFF Al
'not' (y '&' x) is Element of CQC-WFF Al
('not' (x '&' x)) => ('not' (y '&' x)) is Element of CQC-WFF Al
(y => x) => (('not' (x '&' x)) => ('not' (y '&' x))) is Element of CQC-WFF Al
Z is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
s is Element of bool (CQC-WFF Al)
(Al,s) is Element of bool (CQC-WFF Al)
y is Element of CQC-WFF Al
x is Element of CQC-WFF Al
y '&' x is Element of CQC-WFF Al
x '&' y is Element of CQC-WFF Al
(y '&' x) => (x '&' y) is Element of CQC-WFF Al
x is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
s is Element of bool (CQC-WFF Al)
(Al,s) is Element of bool (CQC-WFF Al)
y is Element of CQC-WFF Al
x is Element of CQC-WFF Al
y => x is Element of CQC-WFF Al
x is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
s is Element of bool (CQC-WFF Al)
(Al,s) is Element of bool (CQC-WFF Al)
y is Element of CQC-WFF Al
x is Element of bound_QC-variables Al
All (x,y) is Element of CQC-WFF Al
(All (x,y)) => y is Element of CQC-WFF Al
x is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
s is Element of bool (CQC-WFF Al)
(Al,s) is Element of bool (CQC-WFF Al)
y is Element of CQC-WFF Al
still_not-bound_in y is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
x is Element of CQC-WFF Al
y => x is Element of CQC-WFF Al
x is Element of bound_QC-variables Al
All (x,x) is Element of CQC-WFF Al
y => (All (x,x)) is Element of CQC-WFF Al
Z is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
s is Element of bool (CQC-WFF Al)
(Al,s) is Element of bool (CQC-WFF Al)
y is Element of QC-WFF Al
still_not-bound_in y is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
x is Element of bound_QC-variables Al
y . x is Element of QC-WFF Al
x is Element of bound_QC-variables Al
y . x is Element of QC-WFF Al
Y is Element of CQC-WFF Al
n is Element of bool (CQC-WFF Al)
Z is Element of CQC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
s is Element of bool (CQC-WFF Al)
(Al,s) is Element of bool (CQC-WFF Al)
VERUM Al is Element of CQC-WFF Al
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
y is Element of CQC-WFF Al
'not' y is Element of CQC-WFF Al
('not' y) => y is Element of CQC-WFF Al
(('not' y) => y) => y is Element of CQC-WFF Al
still_not-bound_in y is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
x is Element of CQC-WFF Al
('not' y) => x is Element of CQC-WFF Al
y => (('not' y) => x) is Element of CQC-WFF Al
y => x is Element of CQC-WFF Al
y '&' x is Element of CQC-WFF Al
x '&' y is Element of CQC-WFF Al
(y '&' x) => (x '&' y) is Element of CQC-WFF Al
x is Element of CQC-WFF Al
x '&' x is Element of CQC-WFF Al
'not' (x '&' x) is Element of CQC-WFF Al
y '&' x is Element of CQC-WFF Al
'not' (y '&' x) is Element of CQC-WFF Al
('not' (x '&' x)) => ('not' (y '&' x)) is Element of CQC-WFF Al
(y => x) => (('not' (x '&' x)) => ('not' (y '&' x))) is Element of CQC-WFF Al
Z is Element of QC-WFF Al
still_not-bound_in Z is Element of bool (bound_QC-variables Al)
Y is Element of bound_QC-variables Al
All (Y,y) is Element of CQC-WFF Al
(All (Y,y)) => y is Element of CQC-WFF Al
All (Y,x) is Element of CQC-WFF Al
y => (All (Y,x)) is Element of CQC-WFF Al
Z . Y is Element of QC-WFF Al
n is Element of bound_QC-variables Al
Z . n is Element of QC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
s is Element of bool (CQC-WFF Al)
y is Element of bool (CQC-WFF Al)
(Al,y) is Element of bool (CQC-WFF Al)
x is set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
s is Element of bool (CQC-WFF Al)
(Al,s) is Element of bool (CQC-WFF Al)
y is set
x is Element of CQC-WFF Al
x is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
s is Element of bool (CQC-WFF Al)
(Al,s) is Element of bool (CQC-WFF Al)
y is Element of bool (CQC-WFF Al)
(Al,y) is Element of bool (CQC-WFF Al)
x is set
x is Element of CQC-WFF Al
Z is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
s is Element of bool (CQC-WFF Al)
(Al,s) is Element of bool (CQC-WFF Al)
(Al,(Al,s)) is Element of bool (CQC-WFF Al)
y is set
x is Element of CQC-WFF Al
x is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
s is Element of bool (CQC-WFF Al)
(Al,s) is Element of bool (CQC-WFF Al)
(Al,(Al,s)) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
s is Element of bool (CQC-WFF Al)
(Al,s) is Element of bool (CQC-WFF Al)
y is set
{ b1 where b1 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT : b1 <= 9 } is set
() is set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
len s is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
y is ext-real V4() V8() V9() V10() V14() V15() finite V40() set
s . y is set
(s . y) `2 is set
dom s is finite Element of bool NAT
Seg (len s) is finite V42( len s) Element of bool NAT
proj2 s is V16() finite set
x is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
bool (CQC-WFF Al) is non empty set
s is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
y is ext-real V4() V8() V9() V10() V14() V15() finite V40() set
s . y is set
(s . y) `2 is set
(s . y) `1 is set
x is Element of bool (CQC-WFF Al)
VERUM Al is Element of CQC-WFF Al
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
x is Element of CQC-WFF Al
'not' x is Element of CQC-WFF Al
('not' x) => x is Element of CQC-WFF Al
(('not' x) => x) => x is Element of CQC-WFF Al
Z is Element of CQC-WFF Al
'not' Z is Element of CQC-WFF Al
Y is Element of CQC-WFF Al
('not' Z) => Y is Element of CQC-WFF Al
Z => (('not' Z) => Y) is Element of CQC-WFF Al
n is Element of CQC-WFF Al
y is Element of CQC-WFF Al
n => y is Element of CQC-WFF Al
c10 is Element of CQC-WFF Al
y '&' c10 is Element of CQC-WFF Al
'not' (y '&' c10) is Element of CQC-WFF Al
n '&' c10 is Element of CQC-WFF Al
'not' (n '&' c10) is Element of CQC-WFF Al
('not' (y '&' c10)) => ('not' (n '&' c10)) is Element of CQC-WFF Al
(n => y) => (('not' (y '&' c10)) => ('not' (n '&' c10))) is Element of CQC-WFF Al
c11 is Element of CQC-WFF Al
c12 is Element of CQC-WFF Al
c11 '&' c12 is Element of CQC-WFF Al
c12 '&' c11 is Element of CQC-WFF Al
(c11 '&' c12) => (c12 '&' c11) is Element of CQC-WFF Al
c14 is Element of bound_QC-variables Al
c13 is Element of CQC-WFF Al
All (c14,c13) is Element of CQC-WFF Al
(All (c14,c13)) => c13 is Element of CQC-WFF Al
c15 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c16 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c17 is Element of CQC-WFF Al
s . c16 is set
(s . c16) `1 is set
c18 is Element of CQC-WFF Al
s . c15 is set
(s . c15) `1 is set
c17 => c18 is Element of CQC-WFF Al
c19 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
s . c19 is set
(s . c19) `1 is set
c20 is Element of CQC-WFF Al
c21 is Element of CQC-WFF Al
c20 => c21 is Element of CQC-WFF Al
c22 is Element of bound_QC-variables Al
still_not-bound_in c20 is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
All (c22,c21) is Element of CQC-WFF Al
c20 => (All (c22,c21)) is Element of CQC-WFF Al
c23 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c26 is Element of QC-WFF Al
c24 is Element of bound_QC-variables Al
c26 . c24 is Element of QC-WFF Al
c25 is Element of bound_QC-variables Al
c26 . c25 is Element of QC-WFF Al
still_not-bound_in c26 is Element of bool (bound_QC-variables Al)
s . c23 is set
(s . c23) `1 is set
c27 is Element of CQC-WFF Al
'not' c27 is Element of CQC-WFF Al
('not' c27) => c27 is Element of CQC-WFF Al
(('not' c27) => c27) => c27 is Element of CQC-WFF Al
c28 is Element of CQC-WFF Al
'not' c28 is Element of CQC-WFF Al
c29 is Element of CQC-WFF Al
('not' c28) => c29 is Element of CQC-WFF Al
c28 => (('not' c28) => c29) is Element of CQC-WFF Al
c30 is Element of CQC-WFF Al
c31 is Element of CQC-WFF Al
c30 => c31 is Element of CQC-WFF Al
c32 is Element of CQC-WFF Al
c31 '&' c32 is Element of CQC-WFF Al
'not' (c31 '&' c32) is Element of CQC-WFF Al
c30 '&' c32 is Element of CQC-WFF Al
'not' (c30 '&' c32) is Element of CQC-WFF Al
('not' (c31 '&' c32)) => ('not' (c30 '&' c32)) is Element of CQC-WFF Al
(c30 => c31) => (('not' (c31 '&' c32)) => ('not' (c30 '&' c32))) is Element of CQC-WFF Al
c33 is Element of CQC-WFF Al
c34 is Element of CQC-WFF Al
c33 '&' c34 is Element of CQC-WFF Al
c34 '&' c33 is Element of CQC-WFF Al
(c33 '&' c34) => (c34 '&' c33) is Element of CQC-WFF Al
c36 is Element of bound_QC-variables Al
c35 is Element of CQC-WFF Al
All (c36,c35) is Element of CQC-WFF Al
(All (c36,c35)) => c35 is Element of CQC-WFF Al
c37 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c38 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c39 is Element of CQC-WFF Al
s . c38 is set
(s . c38) `1 is set
c40 is Element of CQC-WFF Al
s . c37 is set
(s . c37) `1 is set
c39 => c40 is Element of CQC-WFF Al
c41 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
s . c41 is set
(s . c41) `1 is set
c42 is Element of CQC-WFF Al
c43 is Element of CQC-WFF Al
c42 => c43 is Element of CQC-WFF Al
c44 is Element of bound_QC-variables Al
still_not-bound_in c42 is Element of bool (bound_QC-variables Al)
All (c44,c43) is Element of CQC-WFF Al
c42 => (All (c44,c43)) is Element of CQC-WFF Al
c45 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c48 is Element of QC-WFF Al
c46 is Element of bound_QC-variables Al
c48 . c46 is Element of QC-WFF Al
c47 is Element of bound_QC-variables Al
c48 . c47 is Element of QC-WFF Al
still_not-bound_in c48 is Element of bool (bound_QC-variables Al)
s . c45 is set
(s . c45) `1 is set
c49 is Element of CQC-WFF Al
'not' c49 is Element of CQC-WFF Al
('not' c49) => c49 is Element of CQC-WFF Al
(('not' c49) => c49) => c49 is Element of CQC-WFF Al
c50 is Element of CQC-WFF Al
'not' c50 is Element of CQC-WFF Al
c51 is Element of CQC-WFF Al
('not' c50) => c51 is Element of CQC-WFF Al
c50 => (('not' c50) => c51) is Element of CQC-WFF Al
c52 is Element of CQC-WFF Al
'not' c52 is Element of CQC-WFF Al
('not' c52) => c52 is Element of CQC-WFF Al
(('not' c52) => c52) => c52 is Element of CQC-WFF Al
c53 is Element of CQC-WFF Al
c54 is Element of CQC-WFF Al
c53 => c54 is Element of CQC-WFF Al
c55 is Element of CQC-WFF Al
c54 '&' c55 is Element of CQC-WFF Al
'not' (c54 '&' c55) is Element of CQC-WFF Al
c53 '&' c55 is Element of CQC-WFF Al
'not' (c53 '&' c55) is Element of CQC-WFF Al
('not' (c54 '&' c55)) => ('not' (c53 '&' c55)) is Element of CQC-WFF Al
(c53 => c54) => (('not' (c54 '&' c55)) => ('not' (c53 '&' c55))) is Element of CQC-WFF Al
c56 is Element of CQC-WFF Al
'not' c56 is Element of CQC-WFF Al
('not' c56) => c56 is Element of CQC-WFF Al
(('not' c56) => c56) => c56 is Element of CQC-WFF Al
c57 is Element of CQC-WFF Al
c58 is Element of CQC-WFF Al
c57 '&' c58 is Element of CQC-WFF Al
c58 '&' c57 is Element of CQC-WFF Al
(c57 '&' c58) => (c58 '&' c57) is Element of CQC-WFF Al
c59 is Element of CQC-WFF Al
'not' c59 is Element of CQC-WFF Al
('not' c59) => c59 is Element of CQC-WFF Al
(('not' c59) => c59) => c59 is Element of CQC-WFF Al
c61 is Element of bound_QC-variables Al
c60 is Element of CQC-WFF Al
All (c61,c60) is Element of CQC-WFF Al
(All (c61,c60)) => c60 is Element of CQC-WFF Al
c62 is Element of CQC-WFF Al
'not' c62 is Element of CQC-WFF Al
('not' c62) => c62 is Element of CQC-WFF Al
(('not' c62) => c62) => c62 is Element of CQC-WFF Al
c63 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c64 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c65 is Element of CQC-WFF Al
s . c64 is set
(s . c64) `1 is set
c66 is Element of CQC-WFF Al
s . c63 is set
(s . c63) `1 is set
c65 => c66 is Element of CQC-WFF Al
c67 is Element of CQC-WFF Al
'not' c67 is Element of CQC-WFF Al
('not' c67) => c67 is Element of CQC-WFF Al
(('not' c67) => c67) => c67 is Element of CQC-WFF Al
c68 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
s . c68 is set
(s . c68) `1 is set
c69 is Element of CQC-WFF Al
c70 is Element of CQC-WFF Al
c69 => c70 is Element of CQC-WFF Al
c71 is Element of bound_QC-variables Al
still_not-bound_in c69 is Element of bool (bound_QC-variables Al)
All (c71,c70) is Element of CQC-WFF Al
c69 => (All (c71,c70)) is Element of CQC-WFF Al
c72 is Element of CQC-WFF Al
'not' c72 is Element of CQC-WFF Al
('not' c72) => c72 is Element of CQC-WFF Al
(('not' c72) => c72) => c72 is Element of CQC-WFF Al
c73 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c76 is Element of QC-WFF Al
c74 is Element of bound_QC-variables Al
c76 . c74 is Element of QC-WFF Al
c75 is Element of bound_QC-variables Al
c76 . c75 is Element of QC-WFF Al
still_not-bound_in c76 is Element of bool (bound_QC-variables Al)
s . c73 is set
(s . c73) `1 is set
c77 is Element of CQC-WFF Al
'not' c77 is Element of CQC-WFF Al
c78 is Element of CQC-WFF Al
('not' c77) => c78 is Element of CQC-WFF Al
c77 => (('not' c77) => c78) is Element of CQC-WFF Al
c79 is Element of CQC-WFF Al
c80 is Element of CQC-WFF Al
c79 => c80 is Element of CQC-WFF Al
c81 is Element of CQC-WFF Al
c80 '&' c81 is Element of CQC-WFF Al
'not' (c80 '&' c81) is Element of CQC-WFF Al
c79 '&' c81 is Element of CQC-WFF Al
'not' (c79 '&' c81) is Element of CQC-WFF Al
('not' (c80 '&' c81)) => ('not' (c79 '&' c81)) is Element of CQC-WFF Al
(c79 => c80) => (('not' (c80 '&' c81)) => ('not' (c79 '&' c81))) is Element of CQC-WFF Al
c82 is Element of CQC-WFF Al
'not' c82 is Element of CQC-WFF Al
c83 is Element of CQC-WFF Al
('not' c82) => c83 is Element of CQC-WFF Al
c82 => (('not' c82) => c83) is Element of CQC-WFF Al
c84 is Element of CQC-WFF Al
c85 is Element of CQC-WFF Al
c84 '&' c85 is Element of CQC-WFF Al
c85 '&' c84 is Element of CQC-WFF Al
(c84 '&' c85) => (c85 '&' c84) is Element of CQC-WFF Al
c86 is Element of CQC-WFF Al
'not' c86 is Element of CQC-WFF Al
c87 is Element of CQC-WFF Al
('not' c86) => c87 is Element of CQC-WFF Al
c86 => (('not' c86) => c87) is Element of CQC-WFF Al
c89 is Element of bound_QC-variables Al
c88 is Element of CQC-WFF Al
All (c89,c88) is Element of CQC-WFF Al
(All (c89,c88)) => c88 is Element of CQC-WFF Al
c90 is Element of CQC-WFF Al
'not' c90 is Element of CQC-WFF Al
c91 is Element of CQC-WFF Al
('not' c90) => c91 is Element of CQC-WFF Al
c90 => (('not' c90) => c91) is Element of CQC-WFF Al
c92 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c93 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c94 is Element of CQC-WFF Al
s . c93 is set
(s . c93) `1 is set
c95 is Element of CQC-WFF Al
s . c92 is set
(s . c92) `1 is set
c94 => c95 is Element of CQC-WFF Al
c96 is Element of CQC-WFF Al
'not' c96 is Element of CQC-WFF Al
c97 is Element of CQC-WFF Al
('not' c96) => c97 is Element of CQC-WFF Al
c96 => (('not' c96) => c97) is Element of CQC-WFF Al
c98 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
s . c98 is set
(s . c98) `1 is set
c99 is Element of CQC-WFF Al
c100 is Element of CQC-WFF Al
c99 => c100 is Element of CQC-WFF Al
c101 is Element of bound_QC-variables Al
still_not-bound_in c99 is Element of bool (bound_QC-variables Al)
All (c101,c100) is Element of CQC-WFF Al
c99 => (All (c101,c100)) is Element of CQC-WFF Al
c102 is Element of CQC-WFF Al
'not' c102 is Element of CQC-WFF Al
c103 is Element of CQC-WFF Al
('not' c102) => c103 is Element of CQC-WFF Al
c102 => (('not' c102) => c103) is Element of CQC-WFF Al
c104 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c107 is Element of QC-WFF Al
c105 is Element of bound_QC-variables Al
c107 . c105 is Element of QC-WFF Al
c106 is Element of bound_QC-variables Al
c107 . c106 is Element of QC-WFF Al
still_not-bound_in c107 is Element of bool (bound_QC-variables Al)
s . c104 is set
(s . c104) `1 is set
c108 is Element of CQC-WFF Al
c109 is Element of CQC-WFF Al
c108 => c109 is Element of CQC-WFF Al
c110 is Element of CQC-WFF Al
c109 '&' c110 is Element of CQC-WFF Al
'not' (c109 '&' c110) is Element of CQC-WFF Al
c108 '&' c110 is Element of CQC-WFF Al
'not' (c108 '&' c110) is Element of CQC-WFF Al
('not' (c109 '&' c110)) => ('not' (c108 '&' c110)) is Element of CQC-WFF Al
(c108 => c109) => (('not' (c109 '&' c110)) => ('not' (c108 '&' c110))) is Element of CQC-WFF Al
c111 is Element of CQC-WFF Al
c112 is Element of CQC-WFF Al
c111 '&' c112 is Element of CQC-WFF Al
c112 '&' c111 is Element of CQC-WFF Al
(c111 '&' c112) => (c112 '&' c111) is Element of CQC-WFF Al
c113 is Element of CQC-WFF Al
c114 is Element of CQC-WFF Al
c113 => c114 is Element of CQC-WFF Al
c115 is Element of CQC-WFF Al
c114 '&' c115 is Element of CQC-WFF Al
'not' (c114 '&' c115) is Element of CQC-WFF Al
c113 '&' c115 is Element of CQC-WFF Al
'not' (c113 '&' c115) is Element of CQC-WFF Al
('not' (c114 '&' c115)) => ('not' (c113 '&' c115)) is Element of CQC-WFF Al
(c113 => c114) => (('not' (c114 '&' c115)) => ('not' (c113 '&' c115))) is Element of CQC-WFF Al
c117 is Element of bound_QC-variables Al
c116 is Element of CQC-WFF Al
All (c117,c116) is Element of CQC-WFF Al
(All (c117,c116)) => c116 is Element of CQC-WFF Al
c118 is Element of CQC-WFF Al
c119 is Element of CQC-WFF Al
c118 => c119 is Element of CQC-WFF Al
c120 is Element of CQC-WFF Al
c119 '&' c120 is Element of CQC-WFF Al
'not' (c119 '&' c120) is Element of CQC-WFF Al
c118 '&' c120 is Element of CQC-WFF Al
'not' (c118 '&' c120) is Element of CQC-WFF Al
('not' (c119 '&' c120)) => ('not' (c118 '&' c120)) is Element of CQC-WFF Al
(c118 => c119) => (('not' (c119 '&' c120)) => ('not' (c118 '&' c120))) is Element of CQC-WFF Al
c121 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c122 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c123 is Element of CQC-WFF Al
s . c122 is set
(s . c122) `1 is set
c124 is Element of CQC-WFF Al
s . c121 is set
(s . c121) `1 is set
c123 => c124 is Element of CQC-WFF Al
c125 is Element of CQC-WFF Al
c126 is Element of CQC-WFF Al
c125 => c126 is Element of CQC-WFF Al
c127 is Element of CQC-WFF Al
c126 '&' c127 is Element of CQC-WFF Al
'not' (c126 '&' c127) is Element of CQC-WFF Al
c125 '&' c127 is Element of CQC-WFF Al
'not' (c125 '&' c127) is Element of CQC-WFF Al
('not' (c126 '&' c127)) => ('not' (c125 '&' c127)) is Element of CQC-WFF Al
(c125 => c126) => (('not' (c126 '&' c127)) => ('not' (c125 '&' c127))) is Element of CQC-WFF Al
c128 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
s . c128 is set
(s . c128) `1 is set
c129 is Element of CQC-WFF Al
c130 is Element of CQC-WFF Al
c129 => c130 is Element of CQC-WFF Al
c131 is Element of bound_QC-variables Al
still_not-bound_in c129 is Element of bool (bound_QC-variables Al)
All (c131,c130) is Element of CQC-WFF Al
c129 => (All (c131,c130)) is Element of CQC-WFF Al
c132 is Element of CQC-WFF Al
c133 is Element of CQC-WFF Al
c132 => c133 is Element of CQC-WFF Al
c134 is Element of CQC-WFF Al
c133 '&' c134 is Element of CQC-WFF Al
'not' (c133 '&' c134) is Element of CQC-WFF Al
c132 '&' c134 is Element of CQC-WFF Al
'not' (c132 '&' c134) is Element of CQC-WFF Al
('not' (c133 '&' c134)) => ('not' (c132 '&' c134)) is Element of CQC-WFF Al
(c132 => c133) => (('not' (c133 '&' c134)) => ('not' (c132 '&' c134))) is Element of CQC-WFF Al
c135 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c138 is Element of QC-WFF Al
c136 is Element of bound_QC-variables Al
c138 . c136 is Element of QC-WFF Al
c137 is Element of bound_QC-variables Al
c138 . c137 is Element of QC-WFF Al
still_not-bound_in c138 is Element of bool (bound_QC-variables Al)
s . c135 is set
(s . c135) `1 is set
c139 is Element of CQC-WFF Al
c140 is Element of CQC-WFF Al
c139 '&' c140 is Element of CQC-WFF Al
c140 '&' c139 is Element of CQC-WFF Al
(c139 '&' c140) => (c140 '&' c139) is Element of CQC-WFF Al
c142 is Element of bound_QC-variables Al
c141 is Element of CQC-WFF Al
All (c142,c141) is Element of CQC-WFF Al
(All (c142,c141)) => c141 is Element of CQC-WFF Al
c143 is Element of CQC-WFF Al
c144 is Element of CQC-WFF Al
c143 '&' c144 is Element of CQC-WFF Al
c144 '&' c143 is Element of CQC-WFF Al
(c143 '&' c144) => (c144 '&' c143) is Element of CQC-WFF Al
c145 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c146 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c147 is Element of CQC-WFF Al
s . c146 is set
(s . c146) `1 is set
c148 is Element of CQC-WFF Al
s . c145 is set
(s . c145) `1 is set
c147 => c148 is Element of CQC-WFF Al
c149 is Element of CQC-WFF Al
c150 is Element of CQC-WFF Al
c149 '&' c150 is Element of CQC-WFF Al
c150 '&' c149 is Element of CQC-WFF Al
(c149 '&' c150) => (c150 '&' c149) is Element of CQC-WFF Al
c151 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
s . c151 is set
(s . c151) `1 is set
c152 is Element of CQC-WFF Al
c153 is Element of CQC-WFF Al
c152 => c153 is Element of CQC-WFF Al
c154 is Element of bound_QC-variables Al
still_not-bound_in c152 is Element of bool (bound_QC-variables Al)
All (c154,c153) is Element of CQC-WFF Al
c152 => (All (c154,c153)) is Element of CQC-WFF Al
c155 is Element of CQC-WFF Al
c156 is Element of CQC-WFF Al
c155 '&' c156 is Element of CQC-WFF Al
c156 '&' c155 is Element of CQC-WFF Al
(c155 '&' c156) => (c156 '&' c155) is Element of CQC-WFF Al
c157 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c160 is Element of QC-WFF Al
c158 is Element of bound_QC-variables Al
c160 . c158 is Element of QC-WFF Al
c159 is Element of bound_QC-variables Al
c160 . c159 is Element of QC-WFF Al
still_not-bound_in c160 is Element of bool (bound_QC-variables Al)
s . c157 is set
(s . c157) `1 is set
c162 is Element of bound_QC-variables Al
c161 is Element of CQC-WFF Al
All (c162,c161) is Element of CQC-WFF Al
(All (c162,c161)) => c161 is Element of CQC-WFF Al
c163 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c164 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c165 is Element of CQC-WFF Al
s . c164 is set
(s . c164) `1 is set
c166 is Element of CQC-WFF Al
s . c163 is set
(s . c163) `1 is set
c165 => c166 is Element of CQC-WFF Al
c168 is Element of bound_QC-variables Al
c167 is Element of CQC-WFF Al
All (c168,c167) is Element of CQC-WFF Al
(All (c168,c167)) => c167 is Element of CQC-WFF Al
c169 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
s . c169 is set
(s . c169) `1 is set
c170 is Element of CQC-WFF Al
c171 is Element of CQC-WFF Al
c170 => c171 is Element of CQC-WFF Al
c172 is Element of bound_QC-variables Al
still_not-bound_in c170 is Element of bool (bound_QC-variables Al)
All (c172,c171) is Element of CQC-WFF Al
c170 => (All (c172,c171)) is Element of CQC-WFF Al
c174 is Element of bound_QC-variables Al
c173 is Element of CQC-WFF Al
All (c174,c173) is Element of CQC-WFF Al
(All (c174,c173)) => c173 is Element of CQC-WFF Al
c175 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c178 is Element of QC-WFF Al
c176 is Element of bound_QC-variables Al
c178 . c176 is Element of QC-WFF Al
c177 is Element of bound_QC-variables Al
c178 . c177 is Element of QC-WFF Al
still_not-bound_in c178 is Element of bool (bound_QC-variables Al)
s . c175 is set
(s . c175) `1 is set
c179 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c180 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c181 is Element of CQC-WFF Al
s . c180 is set
(s . c180) `1 is set
c182 is Element of CQC-WFF Al
s . c179 is set
(s . c179) `1 is set
c181 => c182 is Element of CQC-WFF Al
c183 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
s . c183 is set
(s . c183) `1 is set
c184 is Element of CQC-WFF Al
c185 is Element of CQC-WFF Al
c184 => c185 is Element of CQC-WFF Al
c186 is Element of bound_QC-variables Al
still_not-bound_in c184 is Element of bool (bound_QC-variables Al)
All (c186,c185) is Element of CQC-WFF Al
c184 => (All (c186,c185)) is Element of CQC-WFF Al
c187 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c188 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c189 is Element of CQC-WFF Al
s . c188 is set
(s . c188) `1 is set
c190 is Element of CQC-WFF Al
s . c187 is set
(s . c187) `1 is set
c189 => c190 is Element of CQC-WFF Al
c191 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c194 is Element of QC-WFF Al
c192 is Element of bound_QC-variables Al
c194 . c192 is Element of QC-WFF Al
c193 is Element of bound_QC-variables Al
c194 . c193 is Element of QC-WFF Al
still_not-bound_in c194 is Element of bool (bound_QC-variables Al)
s . c191 is set
(s . c191) `1 is set
c195 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
s . c195 is set
(s . c195) `1 is set
c196 is Element of CQC-WFF Al
c197 is Element of CQC-WFF Al
c196 => c197 is Element of CQC-WFF Al
c198 is Element of bound_QC-variables Al
still_not-bound_in c196 is Element of bool (bound_QC-variables Al)
All (c198,c197) is Element of CQC-WFF Al
c196 => (All (c198,c197)) is Element of CQC-WFF Al
c199 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
c202 is Element of QC-WFF Al
c200 is Element of bound_QC-variables Al
c202 . c200 is Element of QC-WFF Al
c201 is Element of bound_QC-variables Al
c202 . c201 is Element of QC-WFF Al
still_not-bound_in c202 is Element of bool (bound_QC-variables Al)
s . c199 is set
(s . c199) `1 is set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is Element of bool (CQC-WFF Al)
y is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
proj2 y is V16() finite set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is Element of bool (CQC-WFF Al)
y is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
len y is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
0 + 1 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is Element of bool (CQC-WFF Al)
y is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
y . 1 is set
(y . 1) `2 is set
len y is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
(y . 1) `1 is set
x is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
x is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
Z is Element of CQC-WFF Al
y . x is set
(y . x) `1 is set
Y is Element of CQC-WFF Al
y . x is set
(y . x) `1 is set
Z => Y is Element of CQC-WFF Al
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
(y . 1) `1 is set
x is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
y . x is set
(y . x) `1 is set
x is Element of CQC-WFF Al
Z is Element of CQC-WFF Al
x => Z is Element of CQC-WFF Al
Y is Element of bound_QC-variables Al
still_not-bound_in x is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
All (Y,Z) is Element of CQC-WFF Al
x => (All (Y,Z)) is Element of CQC-WFF Al
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
(y . 1) `1 is set
x is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
Y is Element of QC-WFF Al
x is Element of bound_QC-variables Al
Y . x is Element of QC-WFF Al
Z is Element of bound_QC-variables Al
Y . Z is Element of QC-WFF Al
still_not-bound_in Y is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
y . x is set
(y . x) `1 is set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
y is Element of bool (CQC-WFF Al)
x is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
len x is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
x is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
x ^ x is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
Seg (len x) is finite V42( len x) Element of bool NAT
dom x is finite Element of bool NAT
(x ^ x) . s is set
x . s is set
len (x ^ x) is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
len x is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
(len x) + (len x) is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
((x ^ x) . s) `2 is set
((x ^ x) . s) `1 is set
((x ^ x) . s) `2 is set
((x ^ x) . s) `1 is set
VERUM Al is Element of CQC-WFF Al
((x ^ x) . s) `2 is set
((x ^ x) . s) `1 is set
((x ^ x) . s) `2 is set
((x ^ x) . s) `1 is set
((x ^ x) . s) `2 is set
((x ^ x) . s) `1 is set
((x ^ x) . s) `2 is set
((x ^ x) . s) `1 is set
((x ^ x) . s) `2 is set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
((x ^ x) . s) `1 is set
((x ^ x) . s) `2 is set
((x ^ x) . s) `1 is set
(x . s) `1 is set
Z is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
Y is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
n is Element of CQC-WFF Al
x . Y is set
(x . Y) `1 is set
y is Element of CQC-WFF Al
x . Z is set
(x . Z) `1 is set
n => y is Element of CQC-WFF Al
(x ^ x) . Z is set
(x ^ x) . Y is set
((x ^ x) . s) `2 is set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
((x ^ x) . s) `1 is set
(x . s) `1 is set
Z is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
x . Z is set
(x . Z) `1 is set
Y is Element of CQC-WFF Al
n is Element of CQC-WFF Al
Y => n is Element of CQC-WFF Al
y is Element of bound_QC-variables Al
still_not-bound_in Y is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
All (y,n) is Element of CQC-WFF Al
Y => (All (y,n)) is Element of CQC-WFF Al
(x ^ x) . Z is set
((x ^ x) . s) `2 is set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
((x ^ x) . s) `1 is set
(x . s) `1 is set
Z is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
y is Element of QC-WFF Al
Y is Element of bound_QC-variables Al
y . Y is Element of QC-WFF Al
n is Element of bound_QC-variables Al
y . n is Element of QC-WFF Al
still_not-bound_in y is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
x . Z is set
(x . Z) `1 is set
(x ^ x) . Z is set
((x ^ x) . s) `2 is set
(x . s) `2 is set
(x . s) `1 is set
(x . s) `2 is set
(x . s) `1 is set
VERUM Al is Element of CQC-WFF Al
(x . s) `2 is set
(x . s) `1 is set
(x . s) `2 is set
(x . s) `1 is set
(x . s) `2 is set
(x . s) `1 is set
(x . s) `2 is set
(x . s) `1 is set
(x . s) `2 is set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
(x . s) `1 is set
(x . s) `2 is set
(x . s) `1 is set
((x ^ x) . s) `1 is set
Z is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
Y is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
n is Element of CQC-WFF Al
(x ^ x) . Y is set
((x ^ x) . Y) `1 is set
y is Element of CQC-WFF Al
(x ^ x) . Z is set
((x ^ x) . Z) `1 is set
n => y is Element of CQC-WFF Al
x . Z is set
x . Y is set
(x . s) `2 is set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
(x . s) `1 is set
((x ^ x) . s) `1 is set
Z is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
(x ^ x) . Z is set
((x ^ x) . Z) `1 is set
Y is Element of CQC-WFF Al
n is Element of CQC-WFF Al
Y => n is Element of CQC-WFF Al
y is Element of bound_QC-variables Al
still_not-bound_in Y is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
All (y,n) is Element of CQC-WFF Al
Y => (All (y,n)) is Element of CQC-WFF Al
x . Z is set
(x . s) `2 is set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
(x . s) `1 is set
((x ^ x) . s) `1 is set
Z is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
y is Element of QC-WFF Al
Y is Element of bound_QC-variables Al
y . Y is Element of QC-WFF Al
n is Element of bound_QC-variables Al
y . n is Element of QC-WFF Al
still_not-bound_in y is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
(x ^ x) . Z is set
((x ^ x) . Z) `1 is set
x . Z is set
(x . s) `2 is set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
y is Element of bool (CQC-WFF Al)
x is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
len x is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
x is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
x ^ x is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
len x is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
s + (len x) is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
Seg (len x) is finite V42( len x) Element of bool NAT
dom x is finite Element of bool NAT
x . s is set
(x ^ x) . (s + (len x)) is set
(len x) + (len x) is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
len (x ^ x) is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
((x ^ x) . (s + (len x))) `2 is set
((x ^ x) . (s + (len x))) `1 is set
((x ^ x) . (s + (len x))) `2 is set
((x ^ x) . (s + (len x))) `1 is set
VERUM Al is Element of CQC-WFF Al
((x ^ x) . (s + (len x))) `2 is set
((x ^ x) . (s + (len x))) `1 is set
((x ^ x) . (s + (len x))) `2 is set
((x ^ x) . (s + (len x))) `1 is set
((x ^ x) . (s + (len x))) `2 is set
((x ^ x) . (s + (len x))) `1 is set
((x ^ x) . (s + (len x))) `2 is set
((x ^ x) . (s + (len x))) `1 is set
((x ^ x) . (s + (len x))) `2 is set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
((x ^ x) . (s + (len x))) `1 is set
((x ^ x) . (s + (len x))) `2 is set
((x ^ x) . (s + (len x))) `1 is set
(x . s) `1 is set
Z is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
Y is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
n is Element of CQC-WFF Al
x . Y is set
(x . Y) `1 is set
y is Element of CQC-WFF Al
x . Z is set
(x . Z) `1 is set
n => y is Element of CQC-WFF Al
Z + (len x) is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
Y + (len x) is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
(x ^ x) . (Z + (len x)) is set
(x ^ x) . (Y + (len x)) is set
((x ^ x) . (s + (len x))) `2 is set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
((x ^ x) . (s + (len x))) `1 is set
(x . s) `1 is set
Z is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
x . Z is set
(x . Z) `1 is set
Y is Element of CQC-WFF Al
n is Element of CQC-WFF Al
Y => n is Element of CQC-WFF Al
y is Element of bound_QC-variables Al
still_not-bound_in Y is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
All (y,n) is Element of CQC-WFF Al
Y => (All (y,n)) is Element of CQC-WFF Al
(len x) + Z is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
(x ^ x) . ((len x) + Z) is set
((x ^ x) . (s + (len x))) `2 is set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
((x ^ x) . (s + (len x))) `1 is set
(x . s) `1 is set
Z is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
y is Element of QC-WFF Al
Y is Element of bound_QC-variables Al
y . Y is Element of QC-WFF Al
n is Element of bound_QC-variables Al
y . n is Element of QC-WFF Al
still_not-bound_in y is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
x . Z is set
(x . Z) `1 is set
(len x) + Z is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
(x ^ x) . ((len x) + Z) is set
((x ^ x) . (s + (len x))) `2 is set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is Element of bool (CQC-WFF Al)
y is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
x is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
y ^ x is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
len (y ^ x) is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
x is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
len y is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
len y is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
x - (len y) is ext-real V4() V15() set
Z is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
Z + (len y) is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
len x is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
(len x) + (len y) is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
(len y) + 1 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
len y is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is Element of bool (CQC-WFF Al)
y is Element of bool (CQC-WFF Al)
x is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
len x is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
x is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
x . x is set
(x . x) `2 is set
(x . x) `1 is set
x . x is set
(x . x) `2 is set
(x . x) `1 is set
VERUM Al is Element of CQC-WFF Al
x . x is set
(x . x) `2 is set
(x . x) `1 is set
x . x is set
(x . x) `2 is set
(x . x) `1 is set
x . x is set
(x . x) `2 is set
(x . x) `1 is set
x . x is set
(x . x) `2 is set
(x . x) `1 is set
x . x is set
(x . x) `2 is set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
(x . x) `1 is set
x . x is set
(x . x) `2 is set
(x . x) `1 is set
x . x is set
(x . x) `2 is set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
(x . x) `1 is set
x . x is set
(x . x) `2 is set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
(x . x) `1 is set
x . x is set
(x . x) `2 is set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
y is Element of bool (CQC-WFF Al)
(Al,y) is Element of bool (CQC-WFF Al)
x is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
len x is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
x . s is set
(x . s) `1 is set
x is ext-real V4() V8() V9() V10() V14() V15() finite V40() set
x . x is set
(x . x) `1 is set
(x . x) `2 is set
(x . x) `2 is set
VERUM Al is Element of CQC-WFF Al
(x . x) `2 is set
Z is Element of CQC-WFF Al
'not' Z is Element of CQC-WFF Al
('not' Z) => Z is Element of CQC-WFF Al
(('not' Z) => Z) => Z is Element of CQC-WFF Al
(x . x) `2 is set
Z is Element of CQC-WFF Al
'not' Z is Element of CQC-WFF Al
Y is Element of CQC-WFF Al
('not' Z) => Y is Element of CQC-WFF Al
Z => (('not' Z) => Y) is Element of CQC-WFF Al
(x . x) `2 is set
Z is Element of CQC-WFF Al
Y is Element of CQC-WFF Al
Z => Y is Element of CQC-WFF Al
n is Element of CQC-WFF Al
Y '&' n is Element of CQC-WFF Al
'not' (Y '&' n) is Element of CQC-WFF Al
Z '&' n is Element of CQC-WFF Al
'not' (Z '&' n) is Element of CQC-WFF Al
('not' (Y '&' n)) => ('not' (Z '&' n)) is Element of CQC-WFF Al
(Z => Y) => (('not' (Y '&' n)) => ('not' (Z '&' n))) is Element of CQC-WFF Al
(x . x) `2 is set
Z is Element of CQC-WFF Al
Y is Element of CQC-WFF Al
Z '&' Y is Element of CQC-WFF Al
Y '&' Z is Element of CQC-WFF Al
(Z '&' Y) => (Y '&' Z) is Element of CQC-WFF Al
(x . x) `2 is set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
Y is Element of bound_QC-variables Al
Z is Element of CQC-WFF Al
All (Y,Z) is Element of CQC-WFF Al
(All (Y,Z)) => Z is Element of CQC-WFF Al
(x . x) `2 is set
Z is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
Y is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
n is Element of CQC-WFF Al
x . Y is set
(x . Y) `1 is set
y is Element of CQC-WFF Al
x . Z is set
(x . Z) `1 is set
n => y is Element of CQC-WFF Al
(x . x) `2 is set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
Z is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
x . Z is set
(x . Z) `1 is set
Y is Element of CQC-WFF Al
n is Element of CQC-WFF Al
Y => n is Element of CQC-WFF Al
y is Element of bound_QC-variables Al
still_not-bound_in Y is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
All (y,n) is Element of CQC-WFF Al
Y => (All (y,n)) is Element of CQC-WFF Al
(x . x) `2 is set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
Z is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
y is Element of QC-WFF Al
Y is Element of bound_QC-variables Al
y . Y is Element of QC-WFF Al
n is Element of bound_QC-variables Al
y . n is Element of QC-WFF Al
still_not-bound_in y is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
x . Z is set
(x . Z) `1 is set
(x . x) `2 is set
x is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
x . x is set
(x . x) `1 is set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
len s is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
s . (len s) is set
(s . (len s)) `1 is set
0 + 1 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
Seg (len s) is finite V42( len s) Element of bool NAT
dom s is finite Element of bool NAT
proj2 s is V16() finite set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is Element of bool (CQC-WFF Al)
(Al,s) is Element of bool (CQC-WFF Al)
y is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
(Al,y) is Element of CQC-WFF Al
len y is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
y . (len y) is set
(y . (len y)) `1 is set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is Element of bool (CQC-WFF Al)
{ b1 where b1 is Element of CQC-WFF Al : ex b2 being V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():] st
( (Al,s,b2) & (Al,b2) = b1 ) } is set
{ b1 where b1 is Element of CQC-WFF Al : S1[b1] } is set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is Element of bool (CQC-WFF Al)
{ b1 where b1 is Element of CQC-WFF Al : ex b2 being V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():] st
( (Al,s,b2) & (Al,b2) = b1 ) } is set
y is set
x is Element of CQC-WFF Al
[x,0] is V27() set
{x,0} is finite set
{x} is non empty trivial finite V42(1) set
{{x,0},{x}} is finite V39() set
x is Element of [:(CQC-WFF Al),():]
<*x*> is non empty trivial V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite V42(1) FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
len <*x*> is ext-real V4() non empty V8() V9() V10() V14() V15() finite V40() Element of NAT
<*x*> . 1 is set
<*x*> . (len <*x*>) is set
(<*x*> . (len <*x*>)) `1 is set
(Al,<*x*>) is Element of CQC-WFF Al
Y is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
(<*x*> . 1) `2 is set
<*x*> . Y is set
(<*x*> . Y) `1 is set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
VERUM Al is Element of CQC-WFF Al
[:(CQC-WFF Al),():] is non empty set
s is Element of bool (CQC-WFF Al)
{ b1 where b1 is Element of CQC-WFF Al : ex b2 being V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():] st
( (Al,s,b2) & (Al,b2) = b1 ) } is set
[(VERUM Al),1] is V27() set
{(VERUM Al),1} is finite set
{(VERUM Al)} is non empty trivial finite V42(1) set
{{(VERUM Al),1},{(VERUM Al)}} is finite V39() set
y is Element of [:(CQC-WFF Al),():]
<*y*> is non empty trivial V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite V42(1) FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
len <*y*> is ext-real V4() non empty V8() V9() V10() V14() V15() finite V40() Element of NAT
<*y*> . 1 is set
<*y*> . (len <*y*>) is set
(<*y*> . (len <*y*>)) `1 is set
(Al,<*y*>) is Element of CQC-WFF Al
x is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
(<*y*> . 1) `2 is set
<*y*> . x is set
(<*y*> . x) `1 is set
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is Element of CQC-WFF Al
'not' s is Element of CQC-WFF Al
('not' s) => s is Element of CQC-WFF Al
(('not' s) => s) => s is Element of CQC-WFF Al
y is Element of bool (CQC-WFF Al)
{ b1 where b1 is Element of CQC-WFF Al : ex b2 being V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():] st
( (Al,y,b2) & (Al,b2) = b1 ) } is set
[((('not' s) => s) => s),2] is V27() set
{((('not' s) => s) => s),2} is finite set
{((('not' s) => s) => s)} is non empty trivial finite V42(1) set
{{((('not' s) => s) => s),2},{((('not' s) => s) => s)}} is finite V39() set
x is Element of [:(CQC-WFF Al),():]
<*x*> is non empty trivial V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite V42(1) FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
len <*x*> is ext-real V4() non empty V8() V9() V10() V14() V15() finite V40() Element of NAT
<*x*> . 1 is set
<*x*> . (len <*x*>) is set
(<*x*> . (len <*x*>)) `1 is set
(Al,<*x*>) is Element of CQC-WFF Al
Z is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
(<*x*> . 1) `2 is set
<*x*> . Z is set
(<*x*> . Z) `1 is set
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is Element of CQC-WFF Al
'not' s is Element of CQC-WFF Al
y is Element of CQC-WFF Al
('not' s) => y is Element of CQC-WFF Al
s => (('not' s) => y) is Element of CQC-WFF Al
x is Element of bool (CQC-WFF Al)
{ b1 where b1 is Element of CQC-WFF Al : ex b2 being V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():] st
( (Al,x,b2) & (Al,b2) = b1 ) } is set
[(s => (('not' s) => y)),3] is V27() set
{(s => (('not' s) => y)),3} is finite set
{(s => (('not' s) => y))} is non empty trivial finite V42(1) set
{{(s => (('not' s) => y)),3},{(s => (('not' s) => y))}} is finite V39() set
x is Element of [:(CQC-WFF Al),():]
<*x*> is non empty trivial V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite V42(1) FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
len <*x*> is ext-real V4() non empty V8() V9() V10() V14() V15() finite V40() Element of NAT
<*x*> . 1 is set
<*x*> . (len <*x*>) is set
(<*x*> . (len <*x*>)) `1 is set
(Al,<*x*>) is Element of CQC-WFF Al
Y is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
(<*x*> . 1) `2 is set
<*x*> . Y is set
(<*x*> . Y) `1 is set
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is Element of CQC-WFF Al
y is Element of CQC-WFF Al
s => y is Element of CQC-WFF Al
x is Element of CQC-WFF Al
y '&' x is Element of CQC-WFF Al
'not' (y '&' x) is Element of CQC-WFF Al
s '&' x is Element of CQC-WFF Al
'not' (s '&' x) is Element of CQC-WFF Al
('not' (y '&' x)) => ('not' (s '&' x)) is Element of CQC-WFF Al
(s => y) => (('not' (y '&' x)) => ('not' (s '&' x))) is Element of CQC-WFF Al
x is Element of bool (CQC-WFF Al)
{ b1 where b1 is Element of CQC-WFF Al : ex b2 being V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():] st
( (Al,x,b2) & (Al,b2) = b1 ) } is set
[((s => y) => (('not' (y '&' x)) => ('not' (s '&' x)))),4] is V27() set
{((s => y) => (('not' (y '&' x)) => ('not' (s '&' x)))),4} is finite set
{((s => y) => (('not' (y '&' x)) => ('not' (s '&' x))))} is non empty trivial finite V42(1) set
{{((s => y) => (('not' (y '&' x)) => ('not' (s '&' x)))),4},{((s => y) => (('not' (y '&' x)) => ('not' (s '&' x))))}} is finite V39() set
Z is Element of [:(CQC-WFF Al),():]
<*Z*> is non empty trivial V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite V42(1) FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
len <*Z*> is ext-real V4() non empty V8() V9() V10() V14() V15() finite V40() Element of NAT
<*Z*> . 1 is set
<*Z*> . (len <*Z*>) is set
(<*Z*> . (len <*Z*>)) `1 is set
(Al,<*Z*>) is Element of CQC-WFF Al
n is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
(<*Z*> . 1) `2 is set
<*Z*> . n is set
(<*Z*> . n) `1 is set
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is Element of CQC-WFF Al
y is Element of CQC-WFF Al
s '&' y is Element of CQC-WFF Al
y '&' s is Element of CQC-WFF Al
(s '&' y) => (y '&' s) is Element of CQC-WFF Al
x is Element of bool (CQC-WFF Al)
{ b1 where b1 is Element of CQC-WFF Al : ex b2 being V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():] st
( (Al,x,b2) & (Al,b2) = b1 ) } is set
[((s '&' y) => (y '&' s)),5] is V27() set
{((s '&' y) => (y '&' s)),5} is finite set
{((s '&' y) => (y '&' s))} is non empty trivial finite V42(1) set
{{((s '&' y) => (y '&' s)),5},{((s '&' y) => (y '&' s))}} is finite V39() set
x is Element of [:(CQC-WFF Al),():]
<*x*> is non empty trivial V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite V42(1) FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
len <*x*> is ext-real V4() non empty V8() V9() V10() V14() V15() finite V40() Element of NAT
<*x*> . 1 is set
<*x*> . (len <*x*>) is set
(<*x*> . (len <*x*>)) `1 is set
(Al,<*x*>) is Element of CQC-WFF Al
Y is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
(<*x*> . 1) `2 is set
<*x*> . Y is set
(<*x*> . Y) `1 is set
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is Element of CQC-WFF Al
y is Element of CQC-WFF Al
s => y is Element of CQC-WFF Al
x is Element of bool (CQC-WFF Al)
{ b1 where b1 is Element of CQC-WFF Al : ex b2 being V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():] st
( (Al,x,b2) & (Al,b2) = b1 ) } is set
x is Element of CQC-WFF Al
Z is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
(Al,Z) is Element of CQC-WFF Al
x is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
(Al,x) is Element of CQC-WFF Al
Z is Element of CQC-WFF Al
Y is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
(Al,Y) is Element of CQC-WFF Al
Z is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
(Al,Z) is Element of CQC-WFF Al
[y,7] is V27() set
{y,7} is finite set
{y} is non empty trivial finite V42(1) set
{{y,7},{y}} is finite V39() set
x ^ Z is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
Y is Element of [:(CQC-WFF Al),():]
<*Y*> is non empty trivial V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite V42(1) FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
(x ^ Z) ^ <*Y*> is non empty V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
len ((x ^ Z) ^ <*Y*>) is ext-real V4() non empty V8() V9() V10() V14() V15() finite V40() Element of NAT
len (x ^ Z) is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
len <*Y*> is ext-real V4() non empty V8() V9() V10() V14() V15() finite V40() Element of NAT
(len (x ^ Z)) + (len <*Y*>) is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
(len (x ^ Z)) + 1 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
len x is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
len Z is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
(len x) + (len Z) is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
((len x) + (len Z)) + 1 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
((x ^ Z) ^ <*Y*>) . (len ((x ^ Z) ^ <*Y*>)) is set
(((x ^ Z) ^ <*Y*>) . (len ((x ^ Z) ^ <*Y*>))) `1 is set
(Al,((x ^ Z) ^ <*Y*>)) is Element of CQC-WFF Al
y is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
((x ^ Z) ^ <*Y*>) . y is set
(((x ^ Z) ^ <*Y*>) . y) `2 is set
(((x ^ Z) ^ <*Y*>) . y) `1 is set
Seg (len x) is finite V42( len x) Element of bool NAT
dom x is finite Element of bool NAT
Z ^ <*Y*> is non empty V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
x ^ (Z ^ <*Y*>) is non empty V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
((x ^ Z) ^ <*Y*>) . (len x) is set
(((x ^ Z) ^ <*Y*>) . (len x)) `1 is set
x . (len x) is set
(x . (len x)) `1 is set
dom Z is finite Element of bool NAT
Seg (len Z) is finite V42( len Z) Element of bool NAT
Seg ((len x) + (len Z)) is finite V42((len x) + (len Z)) Element of bool NAT
Seg (len (x ^ Z)) is finite V42( len (x ^ Z)) Element of bool NAT
dom (x ^ Z) is finite Element of bool NAT
((x ^ Z) ^ <*Y*>) . ((len x) + (len Z)) is set
(((x ^ Z) ^ <*Y*>) . ((len x) + (len Z))) `1 is set
(x ^ Z) . ((len x) + (len Z)) is set
((x ^ Z) . ((len x) + (len Z))) `1 is set
Z . (len Z) is set
(Z . (len Z)) `1 is set
(len x) + 1 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is Element of CQC-WFF Al
y is Element of bound_QC-variables Al
All (y,s) is Element of CQC-WFF Al
(All (y,s)) => s is Element of CQC-WFF Al
x is Element of bool (CQC-WFF Al)
{ b1 where b1 is Element of CQC-WFF Al : ex b2 being V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():] st
( (Al,x,b2) & (Al,b2) = b1 ) } is set
[((All (y,s)) => s),6] is V27() set
{((All (y,s)) => s),6} is finite set
{((All (y,s)) => s)} is non empty trivial finite V42(1) set
{{((All (y,s)) => s),6},{((All (y,s)) => s)}} is finite V39() set
x is Element of [:(CQC-WFF Al),():]
<*x*> is non empty trivial V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite V42(1) FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
len <*x*> is ext-real V4() non empty V8() V9() V10() V14() V15() finite V40() Element of NAT
<*x*> . 1 is set
<*x*> . (len <*x*>) is set
(<*x*> . (len <*x*>)) `1 is set
(Al,<*x*>) is Element of CQC-WFF Al
Y is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
(<*x*> . 1) `2 is set
<*x*> . Y is set
(<*x*> . Y) `1 is set
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is Element of CQC-WFF Al
still_not-bound_in s is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
y is Element of CQC-WFF Al
s => y is Element of CQC-WFF Al
x is Element of bound_QC-variables Al
All (x,y) is Element of CQC-WFF Al
s => (All (x,y)) is Element of CQC-WFF Al
x is Element of bool (CQC-WFF Al)
{ b1 where b1 is Element of CQC-WFF Al : ex b2 being V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():] st
( (Al,x,b2) & (Al,b2) = b1 ) } is set
Z is Element of CQC-WFF Al
Y is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
(Al,Y) is Element of CQC-WFF Al
Z is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
(Al,Z) is Element of CQC-WFF Al
[(s => (All (x,y))),8] is V27() set
{(s => (All (x,y))),8} is finite set
{(s => (All (x,y)))} is non empty trivial finite V42(1) set
{{(s => (All (x,y))),8},{(s => (All (x,y)))}} is finite V39() set
Y is Element of [:(CQC-WFF Al),():]
<*Y*> is non empty trivial V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite V42(1) FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
Z ^ <*Y*> is non empty V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
len (Z ^ <*Y*>) is ext-real V4() non empty V8() V9() V10() V14() V15() finite V40() Element of NAT
len Z is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
len <*Y*> is ext-real V4() non empty V8() V9() V10() V14() V15() finite V40() Element of NAT
(len Z) + (len <*Y*>) is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
(len Z) + 1 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
y is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
(Z ^ <*Y*>) . y is set
((Z ^ <*Y*>) . y) `2 is set
((Z ^ <*Y*>) . y) `1 is set
Seg (len Z) is finite V42( len Z) Element of bool NAT
dom Z is finite Element of bool NAT
(Z ^ <*Y*>) . (len Z) is set
((Z ^ <*Y*>) . (len Z)) `1 is set
Z . (len Z) is set
(Z . (len Z)) `1 is set
(Al,(Z ^ <*Y*>)) is Element of CQC-WFF Al
(Z ^ <*Y*>) . ((len Z) + 1) is set
((Z ^ <*Y*>) . ((len Z) + 1)) `1 is set
Y `1 is set
Al is QC-alphabet
QC-WFF Al is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is Element of QC-WFF Al
still_not-bound_in s is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
y is Element of bound_QC-variables Al
s . y is Element of QC-WFF Al
x is Element of bound_QC-variables Al
s . x is Element of QC-WFF Al
x is Element of bool (CQC-WFF Al)
{ b1 where b1 is Element of CQC-WFF Al : ex b2 being V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():] st
( (Al,x,b2) & (Al,b2) = b1 ) } is set
Z is Element of CQC-WFF Al
Y is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
(Al,Y) is Element of CQC-WFF Al
Z is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
(Al,Z) is Element of CQC-WFF Al
[(s . x),9] is V27() set
{(s . x),9} is finite set
{(s . x)} is non empty trivial finite V42(1) set
{{(s . x),9},{(s . x)}} is finite V39() set
Y is Element of [:(CQC-WFF Al),():]
<*Y*> is non empty trivial V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite V42(1) FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
Z ^ <*Y*> is non empty V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
len (Z ^ <*Y*>) is ext-real V4() non empty V8() V9() V10() V14() V15() finite V40() Element of NAT
len Z is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
len <*Y*> is ext-real V4() non empty V8() V9() V10() V14() V15() finite V40() Element of NAT
(len Z) + (len <*Y*>) is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
(len Z) + 1 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
y is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
(Z ^ <*Y*>) . y is set
((Z ^ <*Y*>) . y) `2 is set
((Z ^ <*Y*>) . y) `1 is set
Seg (len Z) is finite V42( len Z) Element of bool NAT
dom Z is finite Element of bool NAT
(Z ^ <*Y*>) . (len Z) is set
((Z ^ <*Y*>) . (len Z)) `1 is set
Z . (len Z) is set
(Z . (len Z)) `1 is set
(Al,(Z ^ <*Y*>)) is Element of CQC-WFF Al
(Z ^ <*Y*>) . ((len Z) + 1) is set
((Z ^ <*Y*>) . ((len Z) + 1)) `1 is set
Y `1 is set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is Element of bool (CQC-WFF Al)
y is Element of bool (CQC-WFF Al)
{ b1 where b1 is Element of CQC-WFF Al : ex b2 being V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():] st
( (Al,y,b2) & (Al,b2) = b1 ) } is set
VERUM Al is Element of CQC-WFF Al
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
x is Element of CQC-WFF Al
'not' x is Element of CQC-WFF Al
('not' x) => x is Element of CQC-WFF Al
(('not' x) => x) => x is Element of CQC-WFF Al
still_not-bound_in x is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
x is Element of CQC-WFF Al
('not' x) => x is Element of CQC-WFF Al
x => (('not' x) => x) is Element of CQC-WFF Al
x => x is Element of CQC-WFF Al
x '&' x is Element of CQC-WFF Al
x '&' x is Element of CQC-WFF Al
(x '&' x) => (x '&' x) is Element of CQC-WFF Al
Z is Element of CQC-WFF Al
x '&' Z is Element of CQC-WFF Al
'not' (x '&' Z) is Element of CQC-WFF Al
x '&' Z is Element of CQC-WFF Al
'not' (x '&' Z) is Element of CQC-WFF Al
('not' (x '&' Z)) => ('not' (x '&' Z)) is Element of CQC-WFF Al
(x => x) => (('not' (x '&' Z)) => ('not' (x '&' Z))) is Element of CQC-WFF Al
Y is Element of QC-WFF Al
still_not-bound_in Y is Element of bool (bound_QC-variables Al)
n is Element of bound_QC-variables Al
All (n,x) is Element of CQC-WFF Al
(All (n,x)) => x is Element of CQC-WFF Al
All (n,x) is Element of CQC-WFF Al
x => (All (n,x)) is Element of CQC-WFF Al
Y . n is Element of QC-WFF Al
y is Element of bound_QC-variables Al
Y . y is Element of QC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is Element of bool (CQC-WFF Al)
{ b1 where b1 is Element of CQC-WFF Al : ex b2 being V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():] st
( (Al,s,b2) & (Al,b2) = b1 ) } is set
(Al,s) is Element of bool (CQC-WFF Al)
y is set
x is Element of CQC-WFF Al
x is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
(Al,x) is Element of CQC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is Element of bool (CQC-WFF Al)
{ b1 where b1 is Element of CQC-WFF Al : ex b2 being V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():] st
( (Al,s,b2) & (Al,b2) = b1 ) } is set
(Al,s) is Element of bool (CQC-WFF Al)
x is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
[:(CQC-WFF Al),():] is non empty set
s is Element of bool (CQC-WFF Al)
(Al,s) is Element of bool (CQC-WFF Al)
y is Element of CQC-WFF Al
{ b1 where b1 is Element of CQC-WFF Al : ex b2 being V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():] st
( (Al,s,b2) & (Al,b2) = b1 ) } is set
x is Element of CQC-WFF Al
x is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
(Al,x) is Element of CQC-WFF Al
x is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
(Al,x) is Element of CQC-WFF Al
{ b1 where b1 is Element of CQC-WFF Al : ex b2 being V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():] st
( (Al,s,b2) & (Al,b2) = b1 ) } is set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
s is Element of bool (CQC-WFF Al)
(Al,s) is Element of bool (CQC-WFF Al)
y is Element of CQC-WFF Al
[:(CQC-WFF Al),():] is non empty set
x is V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():]
(Al,x) is Element of CQC-WFF Al
proj2 x is V16() finite set
x is set
[:x,():] is set
Z is Element of bool (CQC-WFF Al)
Z /\ s is Element of bool (CQC-WFF Al)
Y is Element of bool (CQC-WFF Al)
(Al,Y) is Element of bool (CQC-WFF Al)
len x is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
n is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT
x . n is set
(x . n) `2 is set
(x . n) `1 is set
Seg (len x) is finite V42( len x) Element of bool NAT
dom x is finite Element of bool NAT
x . n is set
(x . n) `2 is set
(x . n) `1 is set
VERUM Al is Element of CQC-WFF Al
x . n is set
(x . n) `2 is set
(x . n) `1 is set
x . n is set
(x . n) `2 is set
(x . n) `1 is set
x . n is set
(x . n) `2 is set
(x . n) `1 is set
x . n is set
(x . n) `2 is set
(x . n) `1 is set
x . n is set
(x . n) `2 is set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
(x . n) `1 is set
x . n is set
(x . n) `2 is set
(x . n) `1 is set
x . n is set
(x . n) `2 is set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
(x . n) `1 is set
x . n is set
(x . n) `2 is set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
(x . n) `1 is set
x . n is set
(x . n) `2 is set
{ b1 where b1 is Element of CQC-WFF Al : ex b2 being V16() V19( NAT ) V20([:(CQC-WFF Al),():]) Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(CQC-WFF Al),():] st
( (Al,Y,b2) & (Al,b2) = b1 ) } is set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
(Al) is Element of bool (CQC-WFF Al)
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
s is Element of bool (CQC-WFF Al)
(Al,s) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
(Al) is Element of bool (CQC-WFF Al)
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
s is Element of bool (CQC-WFF Al)
(Al,s) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
(Al) is Element of bool (CQC-WFF Al)
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
VERUM Al is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
(Al) is Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
(Al) is Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
s is Element of CQC-WFF Al
'not' s is Element of CQC-WFF Al
('not' s) => s is Element of CQC-WFF Al
(('not' s) => s) => s is Element of CQC-WFF Al
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
(Al) is Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
s is Element of CQC-WFF Al
'not' s is Element of CQC-WFF Al
y is Element of CQC-WFF Al
('not' s) => y is Element of CQC-WFF Al
s => (('not' s) => y) is Element of CQC-WFF Al
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
(Al) is Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
s is Element of CQC-WFF Al
y is Element of CQC-WFF Al
s => y is Element of CQC-WFF Al
x is Element of CQC-WFF Al
y '&' x is Element of CQC-WFF Al
'not' (y '&' x) is Element of CQC-WFF Al
s '&' x is Element of CQC-WFF Al
'not' (s '&' x) is Element of CQC-WFF Al
('not' (y '&' x)) => ('not' (s '&' x)) is Element of CQC-WFF Al
(s => y) => (('not' (y '&' x)) => ('not' (s '&' x))) is Element of CQC-WFF Al
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
(Al) is Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
s is Element of CQC-WFF Al
y is Element of CQC-WFF Al
s '&' y is Element of CQC-WFF Al
y '&' s is Element of CQC-WFF Al
(s '&' y) => (y '&' s) is Element of CQC-WFF Al
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
(Al) is Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
s is Element of CQC-WFF Al
y is Element of CQC-WFF Al
s => y is Element of CQC-WFF Al
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
y is Element of bound_QC-variables Al
s is Element of CQC-WFF Al
All (y,s) is Element of CQC-WFF Al
(All (y,s)) => s is Element of CQC-WFF Al
(Al) is Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
s is Element of CQC-WFF Al
y is Element of CQC-WFF Al
s => y is Element of CQC-WFF Al
(Al) is Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
x is Element of bound_QC-variables Al
still_not-bound_in s is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
All (x,y) is Element of CQC-WFF Al
s => (All (x,y)) is Element of CQC-WFF Al
Al is QC-alphabet
QC-WFF Al is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
s is Element of QC-WFF Al
y is Element of bound_QC-variables Al
s . y is Element of QC-WFF Al
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
x is Element of bound_QC-variables Al
s . x is Element of QC-WFF Al
still_not-bound_in s is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
(Al) is Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
VERUM Al is Element of CQC-WFF Al
s is Element of bool (CQC-WFF Al)
(Al,s) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
s is Element of bool (CQC-WFF Al)
y is Element of CQC-WFF Al
'not' y is Element of CQC-WFF Al
('not' y) => y is Element of CQC-WFF Al
(('not' y) => y) => y is Element of CQC-WFF Al
(Al,s) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
s is Element of bool (CQC-WFF Al)
y is Element of CQC-WFF Al
'not' y is Element of CQC-WFF Al
x is Element of CQC-WFF Al
('not' y) => x is Element of CQC-WFF Al
y => (('not' y) => x) is Element of CQC-WFF Al
(Al,s) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
s is Element of bool (CQC-WFF Al)
y is Element of CQC-WFF Al
x is Element of CQC-WFF Al
y => x is Element of CQC-WFF Al
x is Element of CQC-WFF Al
x '&' x is Element of CQC-WFF Al
'not' (x '&' x) is Element of CQC-WFF Al
y '&' x is Element of CQC-WFF Al
'not' (y '&' x) is Element of CQC-WFF Al
('not' (x '&' x)) => ('not' (y '&' x)) is Element of CQC-WFF Al
(y => x) => (('not' (x '&' x)) => ('not' (y '&' x))) is Element of CQC-WFF Al
(Al,s) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
s is Element of bool (CQC-WFF Al)
y is Element of CQC-WFF Al
x is Element of CQC-WFF Al
y '&' x is Element of CQC-WFF Al
x '&' y is Element of CQC-WFF Al
(y '&' x) => (x '&' y) is Element of CQC-WFF Al
(Al,s) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
s is Element of bool (CQC-WFF Al)
y is Element of CQC-WFF Al
x is Element of CQC-WFF Al
y => x is Element of CQC-WFF Al
(Al,s) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
s is Element of bool (CQC-WFF Al)
y is Element of CQC-WFF Al
x is Element of bound_QC-variables Al
All (x,y) is Element of CQC-WFF Al
(All (x,y)) => y is Element of CQC-WFF Al
(Al,s) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
s is Element of bool (CQC-WFF Al)
y is Element of CQC-WFF Al
still_not-bound_in y is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
x is Element of CQC-WFF Al
y => x is Element of CQC-WFF Al
x is Element of bound_QC-variables Al
All (x,x) is Element of CQC-WFF Al
y => (All (x,x)) is Element of CQC-WFF Al
(Al,s) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
s is Element of bool (CQC-WFF Al)
y is Element of QC-WFF Al
still_not-bound_in y is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
x is Element of bound_QC-variables Al
y . x is Element of QC-WFF Al
x is Element of bound_QC-variables Al
y . x is Element of QC-WFF Al
(Al,s) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
QC-WFF Al is non empty set
Al is QC-alphabet
QC-WFF Al is non empty set
(Al) is Element of bool (CQC-WFF Al)
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
s is Element of QC-WFF Al
Al is QC-alphabet
QC-WFF Al is non empty set
s is Element of QC-WFF Al
(Al) is Element of bool (CQC-WFF Al)
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
s is Element of bool (CQC-WFF Al)
y is Element of CQC-WFF Al
(Al) is Element of bool (CQC-WFF Al)
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
(Al,s) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
VERUM Al is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
(Al) is Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
s is Element of CQC-WFF Al
'not' s is Element of CQC-WFF Al
('not' s) => s is Element of CQC-WFF Al
(('not' s) => s) => s is Element of CQC-WFF Al
(Al) is Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
s is Element of CQC-WFF Al
'not' s is Element of CQC-WFF Al
y is Element of CQC-WFF Al
('not' s) => y is Element of CQC-WFF Al
s => (('not' s) => y) is Element of CQC-WFF Al
(Al) is Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
s is Element of CQC-WFF Al
y is Element of CQC-WFF Al
s => y is Element of CQC-WFF Al
x is Element of CQC-WFF Al
y '&' x is Element of CQC-WFF Al
'not' (y '&' x) is Element of CQC-WFF Al
s '&' x is Element of CQC-WFF Al
'not' (s '&' x) is Element of CQC-WFF Al
('not' (y '&' x)) => ('not' (s '&' x)) is Element of CQC-WFF Al
(s => y) => (('not' (y '&' x)) => ('not' (s '&' x))) is Element of CQC-WFF Al
(Al) is Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
s is Element of CQC-WFF Al
y is Element of CQC-WFF Al
s '&' y is Element of CQC-WFF Al
y '&' s is Element of CQC-WFF Al
(s '&' y) => (y '&' s) is Element of CQC-WFF Al
(Al) is Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
s is Element of CQC-WFF Al
y is Element of CQC-WFF Al
s => y is Element of CQC-WFF Al
(Al) is Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
s is Element of CQC-WFF Al
y is Element of bound_QC-variables Al
All (y,s) is Element of CQC-WFF Al
(All (y,s)) => s is Element of CQC-WFF Al
(Al) is Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
s is Element of CQC-WFF Al
still_not-bound_in s is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
y is Element of CQC-WFF Al
s => y is Element of CQC-WFF Al
x is Element of bound_QC-variables Al
All (x,y) is Element of CQC-WFF Al
s => (All (x,y)) is Element of CQC-WFF Al
(Al) is Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)
Al is QC-alphabet
QC-WFF Al is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
s is Element of QC-WFF Al
still_not-bound_in s is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
y is Element of bound_QC-variables Al
s . y is Element of QC-WFF Al
x is Element of bound_QC-variables Al
s . x is Element of QC-WFF Al
(Al) is Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
{} (CQC-WFF Al) is ext-real non positive non negative V4() empty proper V8() V9() V10() V12() V13() V14() V15() functional finite V39() V40() V42( {} ) FinSequence-membered Element of bool (CQC-WFF Al)
(Al,({} (CQC-WFF Al))) is Element of bool (CQC-WFF Al)