:: CQC_THE1 semantic presentation

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

{ b

{ b

{(Al + 1)} is non empty trivial finite V39() V42(1) set

{ b

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

{ b

{ b

{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

{ b

Al + 1 is ext-real V4() V8() V9() V10() V14() V15() finite V40() Element of NAT

{ b

{(Al + 1)} is non empty trivial finite V39() V42(1) set

{ b

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

{ b

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

c

y '&' c

'not' (y '&' c

n '&' c

'not' (n '&' c

('not' (y '&' c

(n => y) => (('not' (y '&' c

c

c

c

c

(c

c

c

All (c

(All (c

c

c

c

s . c

(s . c

c

s . c

(s . c

c

c

s . c

(s . c

c

c

c

c

still_not-bound_in c

bool (bound_QC-variables Al) is non empty set

All (c

c

c

c

c

c

c

c

still_not-bound_in c

s . c

(s . c

c

'not' c

('not' c

(('not' c

c

'not' c

c

('not' c

c

c

c

c

c

c

'not' (c

c

'not' (c

('not' (c

(c

c

c

c

c

(c

c

c

All (c

(All (c

c

c

c

s . c

(s . c

c

s . c

(s . c

c

c

s . c

(s . c

c

c

c

c

still_not-bound_in c

All (c

c

c

c

c

c

c

c

still_not-bound_in c

s . c

(s . c

c

'not' c

('not' c

(('not' c

c

'not' c

c

('not' c

c

c

'not' c

('not' c

(('not' c

c

c

c

c

c

'not' (c

c

'not' (c

('not' (c

(c

c

'not' c

('not' c

(('not' c

c

c

c

c

(c

c

'not' c

('not' c

(('not' c

c

c

All (c

(All (c

c

'not' c

('not' c

(('not' c

c

c

c

s . c

(s . c

c

s . c

(s . c

c

c

'not' c

('not' c

(('not' c

c

s . c

(s . c

c

c

c

c

still_not-bound_in c

All (c

c

c

'not' c

('not' c

(('not' c

c

c

c

c

c

c

still_not-bound_in c

s . c

(s . c

c

'not' c

c

('not' c

c

c

c

c

c

c

'not' (c

c

'not' (c

('not' (c

(c

c

'not' c

c

('not' c

c

c

c

c

c

(c

c

'not' c

c

('not' c

c

c

c

All (c

(All (c

c

'not' c

c

('not' c

c

c

c

c

s . c

(s . c

c

s . c

(s . c

c

c

'not' c

c

('not' c

c

c

s . c

(s . c

c

c

c

c

still_not-bound_in c

All (c

c

c

'not' c

c

('not' c

c

c

c

c

c

c

c

still_not-bound_in c

s . c

(s . c

c

c

c

c

c

'not' (c

c

'not' (c

('not' (c

(c

c

c

c

c

(c

c

c

c

c

c

'not' (c

c

'not' (c

('not' (c

(c

c

c

All (c

(All (c

c

c

c

c

c

'not' (c

c

'not' (c

('not' (c

(c

c

c

c

s . c

(s . c

c

s . c

(s . c

c

c

c

c

c

c

'not' (c

c

'not' (c

('not' (c

(c

c

s . c

(s . c

c

c

c

c

still_not-bound_in c

All (c

c

c

c

c

c

c

'not' (c

c

'not' (c

('not' (c

(c

c

c

c

c

c

c

still_not-bound_in c

s . c

(s . c

c

c

c

c

(c

c

c

All (c

(All (c

c

c

c

c

(c

c

c

c

s . c

(s . c

c

s . c

(s . c

c

c

c

c

c

(c

c

s . c

(s . c

c

c

c

c

still_not-bound_in c

All (c

c

c

c

c

c

(c

c

c

c

c

c

c

still_not-bound_in c

s . c

(s . c

c

c

All (c

(All (c

c

c

c

s . c

(s . c

c

s . c

(s . c

c

c

c

All (c

(All (c

c

s . c

(s . c

c

c

c

c

still_not-bound_in c

All (c

c

c

c

All (c

(All (c

c

c

c

c

c

c

still_not-bound_in c

s . c

(s . c

c

c

c

s . c

(s . c

c

s . c

(s . c

c

c

s . c

(s . c

c

c

c

c

still_not-bound_in c

All (c

c

c

c

c

s . c

(s . c

c

s . c

(s . c

c

c

c

c

c

c

c

still_not-bound_in c

s . c

(s . c

c

s . c

(s . c

c

c

c

c

still_not-bound_in c

All (c

c

c

c

c

c

c

c

still_not-bound_in c

s . c

(s . c

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)

{ b

( (Al,s,b

{ b

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)

{ b

( (Al,s,b

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)

{ b

( (Al,s,b

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

{ b

( (Al,y,b

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