:: HENMODEL semantic presentation

REAL is set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool REAL

bool REAL is non empty set

omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set

bool omega is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

BOOLEAN is set

{} is set

the empty Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V32() V37() integer finite V43() cardinal {} -element FinSequence-membered set is empty Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V32() V37() integer finite V43() cardinal {} -element FinSequence-membered set

1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal Element of NAT

2 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal Element of NAT

3 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal Element of NAT

0 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

Seg 1 is non empty trivial finite 1 -element Element of bool NAT

TRUE is Element of BOOLEAN

Proof_Step_Kinds is set

4 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal Element of NAT

5 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal Element of NAT

6 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal Element of NAT

7 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal Element of NAT

8 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal Element of NAT

9 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal Element of NAT

Al is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

union Al is epsilon-transitive epsilon-connected ordinal set

k is non empty finite Element of bool NAT

[:Al,k:] is finite set

bool [:Al,k:] is non empty finite V43() set

P is Relation-like Al -defined k -valued Function-like quasi_total finite Element of bool [:Al,k:]

rng P is finite Element of bool k

bool k is non empty finite V43() set

dom P is finite Element of bool Al

bool Al is non empty finite V43() set

P . (union Al) is set

union (rng P) is set

ll is set

CX is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

succ CX is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega

CX is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

succ CX is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega

P . CX is set

ll is set

CX is set

JH is set

P . JH is set

rel is epsilon-transitive epsilon-connected ordinal set

fin9 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

succ fin9 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega

fin9 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

succ fin9 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega

rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

P . rel is set

P . fin9 is set

a is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

i is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

{ b

a is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

Al is non empty finite Element of bool NAT

union Al is set

RelIncl Al is Relation-like finite set

k is epsilon-transitive epsilon-connected ordinal set

RelIncl k is Relation-like set

P is Relation-like Function-like set

dom P is set

field (RelIncl Al) is finite set

ll is set

rng P is set

field (RelIncl k) is set

P . ll is set

CX is Relation-like Function-like set

dom CX is set

JH is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

CX . JH is set

rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

CX . rel is set

rng CX is set

{ b

[rel,JH] is V26() Element of [:NAT,NAT:]

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

{rel,JH} is finite V43() set

{rel} is non empty trivial finite V43() 1 -element set

{{rel,JH},{rel}} is finite V43() set

[(CX . rel),(CX . JH)] is V26() set

{(CX . rel),(CX . JH)} is finite set

{(CX . rel)} is non empty trivial finite 1 -element set

{{(CX . rel),(CX . JH)},{(CX . rel)}} is finite V43() set

rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

fin9 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

JH is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

RelIncl JH is Relation-like finite set

field (RelIncl JH) is finite set

rel is epsilon-transitive epsilon-connected ordinal set

succ rel is non empty epsilon-transitive epsilon-connected ordinal set

rel is epsilon-transitive epsilon-connected ordinal set

succ rel is non empty epsilon-transitive epsilon-connected ordinal set

rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

succ rel is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega

rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

succ rel is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega

rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

succ rel is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega

rng CX is set

[:JH,Al:] is finite set

bool [:JH,Al:] is non empty finite V43() set

rel is Relation-like JH -defined Al -valued Function-like quasi_total finite Element of bool [:JH,Al:]

dom rel is finite Element of bool JH

bool JH is non empty finite V43() set

a is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

fin9 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

rel . fin9 is set

rel . a is set

rng rel is finite Element of bool Al

bool Al is non empty finite V43() set

union JH is epsilon-transitive epsilon-connected ordinal set

rel . (union JH) is set

union (rng rel) is set

fin9 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

succ fin9 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega

fin9 is set

a is set

rel . a is set

i is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

{ b

C is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

Al is non empty set

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

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

k is Relation-like NAT -defined Al -valued Function-like quasi_total Element of bool [:NAT,Al:]

dom k is Element of bool NAT

rng k is Element of bool Al

bool Al is non empty set

union (rng k) is set

P is finite set

{ b

min* { b

ll is Relation-like Function-like set

dom ll is set

rng ll is set

JH is set

CX is finite set

rel is set

ll . rel is set

{ b

min* { b

rel is set

JH is non empty finite Element of bool NAT

union JH is set

rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

k . rel is Element of Al

fin9 is set

a is set

i is set

k . i is set

C is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

{ b

F is set

F is non empty set

F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

k . F is Element of Al

ll . fin9 is set

F is non empty Element of bool NAT

min* F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

{ b

k . F is Element of Al

F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

k . F is Element of Al

F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

k . F is Element of Al

ll is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

k . ll is Element of Al

CX is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

k . CX is Element of Al

JH is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

k . JH is Element of Al

Al is non empty Relation-like 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 non empty Relation-like 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 non empty Relation-like 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 non empty Relation-like 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

Al is non empty Relation-like 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

Al is non empty Relation-like 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

k is Element of bool (CQC-WFF Al)

P is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

rng P is finite Element of bool (CQC-WFF Al)

ll is Element of CQC-WFF Al

<*ll*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

P ^ <*ll*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

'not' ll is Element of CQC-WFF Al

<*('not' ll)*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

P ^ <*('not' ll)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

Al is non empty Relation-like 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

k is Element of CQC-WFF Al

<*k*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

P is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

P ^ <*k*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

ll is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

P ^ ll is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

(P ^ ll) ^ <*k*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

Ant (P ^ <*k*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

Ant ((P ^ ll) ^ <*k*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

Suc ((P ^ ll) ^ <*k*>) is Element of CQC-WFF Al

Suc (P ^ <*k*>) is Element of CQC-WFF Al

Al is non empty Relation-like 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

k is Element of bool (CQC-WFF Al)

P is Element of CQC-WFF Al

'not' P is Element of CQC-WFF Al

<*('not' P)*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

ll is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

rng ll is finite Element of bool (CQC-WFF Al)

ll ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

CX is Element of CQC-WFF Al

<*P*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

JH is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

rng JH is finite Element of bool (CQC-WFF Al)

JH ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

JH ^ ll is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

rel is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

rng rel is finite Element of bool (CQC-WFF Al)

<*CX*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

rel ^ <*CX*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

(rng JH) \/ (rng ll) is finite Element of bool (CQC-WFF Al)

(JH ^ ll) ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

(JH ^ ll) ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

VERUM Al is Element of CQC-WFF Al

'not' (VERUM Al) is Element of CQC-WFF Al

Al is non empty Relation-like 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

k is Element of bool (CQC-WFF Al)

P is Element of CQC-WFF Al

'not' P is Element of CQC-WFF Al

<*P*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

ll is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

rng ll is finite Element of bool (CQC-WFF Al)

ll ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

<*('not' P)*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

CX is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

rng CX is finite Element of bool (CQC-WFF Al)

CX ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

ll ^ CX is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

rng (ll ^ CX) is finite Element of bool (CQC-WFF Al)

JH is Element of bool (CQC-WFF Al)

(rng ll) \/ (rng CX) is finite Element of bool (CQC-WFF Al)

(ll ^ CX) ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

(ll ^ CX) ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

Al is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

Al ^ k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len (Al ^ k) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

Seg (len (Al ^ k)) is finite len (Al ^ k) -element Element of bool NAT

len Al is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

Seg (len Al) is finite len Al -element Element of bool NAT

len k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

seq ((len Al),(len k)) is Element of bool NAT

(Seg (len Al)) \/ (seq ((len Al),(len k))) is Element of bool NAT

dom (Al ^ k) is finite Element of bool NAT

dom Al is finite Element of bool NAT

(dom Al) \/ (seq ((len Al),(len k))) is Element of bool NAT

Al is non empty Relation-like 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

k is Element of bool (CQC-WFF Al)

P is Element of CQC-WFF Al

{P} is non empty trivial finite 1 -element Element of bool (CQC-WFF Al)

k \/ {P} is Element of bool (CQC-WFF Al)

<*P*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

ll is Element of CQC-WFF Al

<*ll*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

CX is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

rng CX is finite Element of bool (CQC-WFF Al)

CX ^ <*ll*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

CX - {P} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

CX " {P} is finite Element of bool NAT

dom CX is finite Element of bool NAT

rel is finite set

card rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega

IdFinS (P,(card rel)) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite card rel -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

Seg (card rel) is finite card rel -element Element of bool NAT

K253((Seg (card rel)),P) is Relation-like Seg (card rel) -defined {P} -valued Function-like quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg (card rel)),{P}:]

{P} is non empty trivial finite 1 -element set

[:(Seg (card rel)),{P}:] is finite set

bool [:(Seg (card rel)),{P}:] is non empty finite V43() set

(CX - {P}) ^ (IdFinS (P,(card rel))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len (IdFinS (P,(card rel))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

rel is finite set

len CX is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

Seg (len CX) is finite len CX -element Element of bool NAT

i is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

len (CX - {P}) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

i - (len (CX - {P})) is ext-real V32() V37() integer set

seq ((len (CX - {P})),(card rel)) is Element of bool NAT

1 + (len (CX - {P})) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

C is ext-real V32() V37() integer set

(card rel) + (len (CX - {P})) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

Sgm rel is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

dom (Sgm rel) is finite Element of bool NAT

i is set

C is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

CX . C is set

rel \ rel is finite Element of bool rel

bool rel is non empty finite V43() set

Seg (len (CX - {P})) is finite len (CX - {P}) -element Element of bool NAT

Sgm (rel \ rel) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

F is finite set

card F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega

card rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega

(card rel) - (card rel) is ext-real V32() V37() integer set

card (Seg (len CX)) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega

(card (Seg (len CX))) - (card rel) is ext-real V32() V37() integer set

(len CX) - (card rel) is ext-real V32() V37() integer set

len ((CX - {P}) ^ (IdFinS (P,(card rel)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

Seg (len ((CX - {P}) ^ (IdFinS (P,(card rel))))) is finite len ((CX - {P}) ^ (IdFinS (P,(card rel)))) -element Element of bool NAT

F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

(Sgm (rel \ rel)) . F is set

F - (len (CX - {P})) is ext-real V32() V37() integer set

(Sgm rel) . (F - (len (CX - {P}))) is set

F is set

F is set

F is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

dom F is finite Element of bool NAT

F is set

Sgm F is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

dom (Sgm F) is finite Element of bool NAT

Seg (card F) is finite card F -element Element of bool NAT

rng F is finite set

F is set

F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

F . F is set

(Sgm F) . F is set

rng (Sgm F) is finite Element of bool NAT

rng (Sgm rel) is finite Element of bool NAT

F - (len (CX - {P})) is ext-real V32() V37() integer set

(Sgm rel) . (F - (len (CX - {P}))) is set

(Seg (len (CX - {P}))) \/ (seq ((len (CX - {P})),(card rel))) is Element of bool NAT

F is set

F is set

F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

(Sgm F) . F is set

len (Sgm F) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

F . F is set

F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

(Sgm rel) . F is set

j is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

j + (len (CX - {P})) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

len (Sgm rel) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

(len (CX - {P})) + (len (IdFinS (P,(card rel)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

dom ((CX - {P}) ^ (IdFinS (P,(card rel)))) is finite Element of bool NAT

(j + (len (CX - {P}))) - (len (CX - {P})) is ext-real V32() V37() integer set

(Sgm rel) . ((j + (len (CX - {P}))) - (len (CX - {P}))) is set

F . (j + (len (CX - {P}))) is set

(len (CX - {P})) + (len (IdFinS (P,(card rel)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

((len CX) - (card rel)) + (len (IdFinS (P,(card rel)))) is ext-real V32() V37() integer set

((len CX) - (card rel)) + (card rel) is ext-real V32() V37() integer set

[:rel,rel:] is finite set

bool [:rel,rel:] is non empty finite V43() set

F is Relation-like rel -defined rel -valued finite Element of bool [:rel,rel:]

rng F is finite Element of bool rel

F is Relation-like rel -defined rel -valued Function-like quasi_total finite Element of bool [:rel,rel:]

j is set

dom F is finite set

F . j is set

h is set

F . h is set

dom F is finite Element of bool rel

(Seg (len (CX - {P}))) \/ (seq ((len (CX - {P})),(card rel))) is Element of bool NAT

(Sgm F) . j is set

rng (Sgm F) is finite Element of bool NAT

k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

k - (len (CX - {P})) is ext-real V32() V37() integer set

(Sgm rel) . (k - (len (CX - {P}))) is set

rng (Sgm rel) is finite Element of bool NAT

(Sgm F) . h is set

k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

k - (len (CX - {P})) is ext-real V32() V37() integer set

g is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

g - (len (CX - {P})) is ext-real V32() V37() integer set

(Sgm rel) . (g - (len (CX - {P}))) is set

(Sgm rel) . (k - (len (CX - {P}))) is set

(g - (len (CX - {P}))) + (len (CX - {P})) is ext-real V32() V37() integer set

(k - (len (CX - {P}))) + (len (CX - {P})) is ext-real V32() V37() integer set

[:(dom CX),(dom CX):] is finite set

bool [:(dom CX),(dom CX):] is non empty finite V43() set

j is Relation-like dom CX -defined dom CX -valued Function-like quasi_total bijective finite Element of bool [:(dom CX),(dom CX):]

dom j is finite Element of bool (dom CX)

bool (dom CX) is non empty finite V43() set

h is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

j . h is set

Per (CX,j) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

dom (Per (CX,j)) is finite Element of bool NAT

dom ((CX - {P}) ^ (IdFinS (P,(card rel)))) is finite Element of bool NAT

k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

j * CX is Relation-like dom CX -defined CQC-WFF Al -valued Function-like finite Element of bool [:(dom CX),(CQC-WFF Al):]

[:(dom CX),(CQC-WFF Al):] is set

bool [:(dom CX),(CQC-WFF Al):] is non empty set

dom (j * CX) is finite Element of bool (dom CX)

dom (IdFinS (P,(card rel))) is finite card rel -element Element of bool NAT

g is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

(len (CX - {P})) + g is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

j . k is set

k - (len (CX - {P})) is ext-real V32() V37() integer set

(Sgm rel) . (k - (len (CX - {P}))) is set

rng (Sgm rel) is finite Element of bool NAT

CX . (j . k) is set

(j * CX) . k is set

(Per (CX,j)) . k is set

(IdFinS (P,(card rel))) . g is set

((CX - {P}) ^ (IdFinS (P,(card rel)))) . k is set

dom (CX - {P}) is finite Element of bool NAT

(Sgm F) . k is set

CX . ((Sgm F) . k) is set

(Sgm F) * CX is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite Element of bool [:NAT,(CQC-WFF Al):]

[:NAT,(CQC-WFF Al):] is non empty non trivial non finite set

bool [:NAT,(CQC-WFF Al):] is non empty non trivial non finite set

((Sgm F) * CX) . k is set

(CX - {P}) . k is set

(j * CX) . h is set

k is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

k . h is set

(CX - {P}) . h is set

rng (CX - {P}) is finite set

(rng CX) \ {P} is finite Element of bool (CQC-WFF Al)

dom k is finite Element of bool NAT

g is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

(len (CX - {P})) + g is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

k ^ <*ll*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

g is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

g ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

(g ^ <*P*>) ^ <*ll*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

g is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

rng g is finite Element of bool (CQC-WFF Al)

(k \/ {P}) \ {P} is Element of bool (CQC-WFF Al)

k \ {P} is Element of bool (CQC-WFF Al)

JH is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

JH ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

(JH ^ <*P*>) ^ <*ll*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

rel is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

rng rel is finite Element of bool (CQC-WFF Al)

rel ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

(rel ^ <*P*>) ^ <*ll*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

fin9 is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

rng fin9 is finite Element of bool (CQC-WFF Al)

fin9 ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

(fin9 ^ <*P*>) ^ <*ll*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

Al is non empty Relation-like 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

k is Element of bool (CQC-WFF Al)

P is Element of CQC-WFF Al

'not' P is Element of CQC-WFF Al

{('not' P)} is non empty trivial finite 1 -element Element of bool (CQC-WFF Al)

k \/ {('not' P)} is Element of bool (CQC-WFF Al)

<*P*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

ll is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

rng ll is finite Element of bool (CQC-WFF Al)

ll ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

<*('not' P)*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

ll ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

(ll ^ <*('not' P)*>) ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

Ant ((ll ^ <*('not' P)*>) ^ <*('not' P)*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

dom <*('not' P)*> is non empty trivial finite 1 -element Element of bool NAT

len ll is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

(len ll) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

dom (Ant ((ll ^ <*('not' P)*>) ^ <*('not' P)*>)) is finite Element of bool NAT

Suc ((ll ^ <*('not' P)*>) ^ <*('not' P)*>) is Element of CQC-WFF Al

(Ant ((ll ^ <*('not' P)*>) ^ <*('not' P)*>)) . ((len ll) + 1) is set

0 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

len (ll ^ <*('not' P)*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

Ant (ll ^ <*('not' P)*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

Suc (ll ^ <*('not' P)*>) is Element of CQC-WFF Al

rng (ll ^ <*('not' P)*>) is finite Element of bool (CQC-WFF Al)

(rng ll) \/ {('not' P)} is finite Element of bool (CQC-WFF Al)

(ll ^ <*('not' P)*>) ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

<*P*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

ll is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

rng ll is finite Element of bool (CQC-WFF Al)

ll ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

ll - {('not' P)} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

ll " {('not' P)} is finite Element of bool NAT

dom ll is finite Element of bool NAT

JH is finite set

card JH is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega

IdFinS (('not' P),(card JH)) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite card JH -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

Seg (card JH) is finite card JH -element Element of bool NAT

K253((Seg (card JH)),('not' P)) is Relation-like Seg (card JH) -defined {('not' P)} -valued Function-like quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg (card JH)),{('not' P)}:]

{('not' P)} is non empty trivial finite 1 -element set

[:(Seg (card JH)),{('not' P)}:] is finite set

bool [:(Seg (card JH)),{('not' P)}:] is non empty finite V43() set

(ll - {('not' P)}) ^ (IdFinS (('not' P),(card JH))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len (IdFinS (('not' P),(card JH))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

rel is finite set

len ll is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

Seg (len ll) is finite len ll -element Element of bool NAT

a is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

len (ll - {('not' P)}) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

a - (len (ll - {('not' P)})) is ext-real V32() V37() integer set

seq ((len (ll - {('not' P)})),(card JH)) is Element of bool NAT

1 + (len (ll - {('not' P)})) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

i is ext-real V32() V37() integer set

(card JH) + (len (ll - {('not' P)})) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

C is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

Sgm JH is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

dom (Sgm JH) is finite Element of bool NAT

a is set

i is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

ll . i is set

rel \ JH is finite Element of bool rel

bool rel is non empty finite V43() set

Seg (len (ll - {('not' P)})) is finite len (ll - {('not' P)}) -element Element of bool NAT

Sgm (rel \ JH) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

C is finite set

card C is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega

card rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega

(card rel) - (card JH) is ext-real V32() V37() integer set

card (Seg (len ll)) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega

(card (Seg (len ll))) - (card JH) is ext-real V32() V37() integer set

(len ll) - (card JH) is ext-real V32() V37() integer set

len ((ll - {('not' P)}) ^ (IdFinS (('not' P),(card JH)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

Seg (len ((ll - {('not' P)}) ^ (IdFinS (('not' P),(card JH))))) is finite len ((ll - {('not' P)}) ^ (IdFinS (('not' P),(card JH)))) -element Element of bool NAT

F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

(Sgm (rel \ JH)) . F is set

F - (len (ll - {('not' P)})) is ext-real V32() V37() integer set

(Sgm JH) . (F - (len (ll - {('not' P)}))) is set

F is set

F is set

F is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

dom F is finite Element of bool NAT

F is set

Sgm C is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

dom (Sgm C) is finite Element of bool NAT

Seg (card C) is finite card C -element Element of bool NAT

rng F is finite set

F is set

F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

F . F is set

(Sgm C) . F is set

rng (Sgm C) is finite Element of bool NAT

rng (Sgm JH) is finite Element of bool NAT

F - (len (ll - {('not' P)})) is ext-real V32() V37() integer set

(Sgm JH) . (F - (len (ll - {('not' P)}))) is set

(Seg (len (ll - {('not' P)}))) \/ (seq ((len (ll - {('not' P)})),(card JH))) is Element of bool NAT

F is set

F is set

F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

(Sgm C) . F is set

len (Sgm C) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

F . F is set

F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

(Sgm JH) . F is set

F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

F + (len (ll - {('not' P)})) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

len (Sgm JH) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

(len (ll - {('not' P)})) + (len (IdFinS (('not' P),(card JH)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

dom ((ll - {('not' P)}) ^ (IdFinS (('not' P),(card JH)))) is finite Element of bool NAT

(F + (len (ll - {('not' P)}))) - (len (ll - {('not' P)})) is ext-real V32() V37() integer set

(Sgm JH) . ((F + (len (ll - {('not' P)}))) - (len (ll - {('not' P)}))) is set

F . (F + (len (ll - {('not' P)}))) is set

(len (ll - {('not' P)})) + (len (IdFinS (('not' P),(card JH)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

((len ll) - (card JH)) + (len (IdFinS (('not' P),(card JH)))) is ext-real V32() V37() integer set

((len ll) - (card JH)) + (card JH) is ext-real V32() V37() integer set

[:rel,rel:] is finite set

bool [:rel,rel:] is non empty finite V43() set

F is Relation-like rel -defined rel -valued finite Element of bool [:rel,rel:]

rng F is finite Element of bool rel

F is Relation-like rel -defined rel -valued Function-like quasi_total finite Element of bool [:rel,rel:]

F is set

dom F is finite set

F . F is set

j is set

F . j is set

dom F is finite Element of bool rel

(Seg (len (ll - {('not' P)}))) \/ (seq ((len (ll - {('not' P)})),(card JH))) is Element of bool NAT

(Sgm C) . F is set

rng (Sgm C) is finite Element of bool NAT

h is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

h - (len (ll - {('not' P)})) is ext-real V32() V37() integer set

(Sgm JH) . (h - (len (ll - {('not' P)}))) is set

rng (Sgm JH) is finite Element of bool NAT

(Sgm C) . j is set

h is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

h - (len (ll - {('not' P)})) is ext-real V32() V37() integer set

k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

k - (len (ll - {('not' P)})) is ext-real V32() V37() integer set

(Sgm JH) . (k - (len (ll - {('not' P)}))) is set

(Sgm JH) . (h - (len (ll - {('not' P)}))) is set

[:(dom ll),(dom ll):] is finite set

bool [:(dom ll),(dom ll):] is non empty finite V43() set

F is Relation-like dom ll -defined dom ll -valued Function-like quasi_total bijective finite Element of bool [:(dom ll),(dom ll):]

dom F is finite Element of bool (dom ll)

bool (dom ll) is non empty finite V43() set

j is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

F . j is set

Per (ll,F) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

dom (Per (ll,F)) is finite Element of bool NAT

dom ((ll - {('not' P)}) ^ (IdFinS (('not' P),(card JH)))) is finite Element of bool NAT

h is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

F * ll is Relation-like dom ll -defined CQC-WFF Al -valued Function-like finite Element of bool [:(dom ll),(CQC-WFF Al):]

[:(dom ll),(CQC-WFF Al):] is set

bool [:(dom ll),(CQC-WFF Al):] is non empty set

dom (F * ll) is finite Element of bool (dom ll)

dom (IdFinS (('not' P),(card JH))) is finite card JH -element Element of bool NAT

k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

(len (ll - {('not' P)})) + k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

F . h is set

h - (len (ll - {('not' P)})) is ext-real V32() V37() integer set

(Sgm JH) . (h - (len (ll - {('not' P)}))) is set

rng (Sgm JH) is finite Element of bool NAT

ll . (F . h) is set

(F * ll) . h is set

(Per (ll,F)) . h is set

(IdFinS (('not' P),(card JH))) . k is set

((ll - {('not' P)}) ^ (IdFinS (('not' P),(card JH)))) . h is set

dom (ll - {('not' P)}) is finite Element of bool NAT

(Sgm C) . h is set

ll . ((Sgm C) . h) is set

(Sgm C) * ll is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite Element of bool [:NAT,(CQC-WFF Al):]

[:NAT,(CQC-WFF Al):] is non empty non trivial non finite set

bool [:NAT,(CQC-WFF Al):] is non empty non trivial non finite set

((Sgm C) * ll) . h is set

(ll - {('not' P)}) . h is set

(F * ll) . j is set

h is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

h . j is set

(ll - {('not' P)}) . j is set

rng (ll - {('not' P)}) is finite set

(rng ll) \ {('not' P)} is finite Element of bool (CQC-WFF Al)

dom h is finite Element of bool NAT

k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

(len (ll - {('not' P)})) + k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

h ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

g is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

<*('not' P)*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

g ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

(g ^ <*('not' P)*>) ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

rng g is finite Element of bool (CQC-WFF Al)

(k \/ {('not' P)}) \ {('not' P)} is Element of bool (CQC-WFF Al)

k \ {('not' P)} is Element of bool (CQC-WFF Al)

g ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

(g ^ <*P*>) ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

Al is non empty Relation-like 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

k is Element of bool (CQC-WFF Al)

P is Element of CQC-WFF Al

'not' P is Element of CQC-WFF Al

{P} is non empty trivial finite 1 -element Element of bool (CQC-WFF Al)

k \/ {P} is Element of bool (CQC-WFF Al)

<*('not' P)*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

ll is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

rng ll is finite Element of bool (CQC-WFF Al)

ll ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

<*P*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

ll ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

(ll ^ <*P*>) ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

Ant ((ll ^ <*P*>) ^ <*P*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

dom <*P*> is non empty trivial finite 1 -element Element of bool NAT

len ll is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

(len ll) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

dom (Ant ((ll ^ <*P*>) ^ <*P*>)) is finite Element of bool NAT

Suc ((ll ^ <*P*>) ^ <*P*>) is Element of CQC-WFF Al

(Ant ((ll ^ <*P*>) ^ <*P*>)) . ((len ll) + 1) is set

0 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

len (ll ^ <*P*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

Ant (ll ^ <*P*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

Suc (ll ^ <*P*>) is Element of CQC-WFF Al

rng (ll ^ <*P*>) is finite Element of bool (CQC-WFF Al)

(rng ll) \/ {P} is finite Element of bool (CQC-WFF Al)

(ll ^ <*P*>) ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

<*('not' P)*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

ll is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

rng ll is finite Element of bool (CQC-WFF Al)

ll ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

ll - {P} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

ll " {P} is finite Element of bool NAT

dom ll is finite Element of bool NAT

JH is finite set

card JH is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega

IdFinS (P,(card JH)) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite card JH -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al

Seg (card JH) is finite card JH -element Element of bool NAT

K253((Seg (card JH)),P) is Relation-like Seg (card JH) -defined {P} -valued Function-like quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg (card JH)),{P}:]

{P} is non empty trivial finite 1 -element set

[:(Seg (card JH)),{P}:] is finite set

bool [:(Seg (card JH)),{P}:] is non empty finite V43() set

(ll - {P}) ^ (IdFinS (P,(card JH))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len (IdFinS (P,(card JH))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

rel is finite set

len ll is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

Seg (len ll) is finite len ll -element Element of bool NAT

a is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

len (ll - {P}) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

a - (len (ll - {P})) is ext-real V32() V37() integer set

seq ((len (ll - {P})),(card JH)) is Element of bool NAT

1 + (len (ll - {P})) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

i is ext-real V32() V37() integer set

(card JH) + (len (ll - {P})) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

C is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

Sgm JH is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

dom (Sgm JH) is finite Element of bool NAT

a is set

i is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

ll . i is set

rel \ JH is finite Element of bool rel

bool rel is non empty finite V43() set

Seg (len (ll - {P})) is finite len (ll - {P}) -element Element of bool NAT

Sgm (rel \ JH) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

C is finite set

card C is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega

card rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega

(card rel) - (card JH) is ext-real V32() V37() integer set

card (Seg (len ll)) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega

(card (Seg (len ll))) - (card JH) is ext-real V32() V37() integer set

(len ll) - (card JH) is ext-real V32() V37() integer set

len ((ll - {P}) ^ (IdFinS (P,(card JH)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

Seg (len ((ll - {P}) ^ (IdFinS (P,(card JH))))) is finite len ((ll - {P}) ^ (IdFinS (P,(card JH)))) -element Element of bool NAT

F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

(Sgm (rel \ JH)) . F is set

F - (len (ll - {P})) is ext-real V32() V37() integer set

(Sgm JH) . (F - (len (ll - {P}))) is set

F is set

F is set

F is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

dom F is finite Element of bool NAT

F is set

Sgm C is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

dom (Sgm C) is finite Element of bool NAT

Seg (card C) is finite card C -element Element of bool NAT

rng F is finite set

F is set

F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

F . F is set

(Sgm C) . F is set

rng (Sgm C) is finite Element of bool NAT

rng (Sgm JH) is finite Element of bool NAT

F - (len (ll - {P})) is ext-real V32() V37() integer set

(Sgm JH) . (F - (len (ll - {P}))) is set

(Seg (len (ll - {P}))) \/ (seq ((len (ll - {P})),(card JH))) is Element of bool NAT

F is set

F is set

F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

(Sgm C) . F is set

len (Sgm C) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

F . F is set

F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

(Sgm JH) . F is set

F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

F + (len (ll - {P})) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

len (Sgm JH) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

(len (ll - {P})) + (len (IdFinS (P,(card JH)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

dom ((ll - {P}) ^ (IdFinS (P,(card JH)))) is finite Element of bool NAT

(F + (len (ll - {P}))) - (len (ll - {P})) is ext-real V32() V37() integer set

(Sgm JH) . ((F + (len (ll - {P}))) - (len (ll - {P}))) is set

F . (F + (len (ll - {P}))) is set

(len (ll - {P})) + (len (IdFinS (P,(card JH)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

((len ll) - (card JH)) + (len (IdFinS (P,(card JH)))) is ext-real V32() V37() integer set

((len ll) - (card JH)) + (card JH) is ext-real V32() V37() integer set

[:rel,rel:] is finite set

bool [:rel,rel:] is non empty finite V43() set

F is Relation-like rel -defined rel -valued finite Element of bool [:rel,rel:]

rng F is finite Element of bool rel

F is Relation-like rel -defined rel -valued Function-like quasi_total finite Element of bool [:rel,rel:]

F is set

dom F is finite set

F . F is set

j is set

F . j is set

dom F is finite Element of bool rel

(Seg (len (ll - {P}))) \/ (seq ((len (ll - {P})),(card JH))) is Element of bool NAT

(Sgm C) . F is set

rng (Sgm C) is finite Element of bool NAT

h is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

h - (len (ll - {P})) is ext-real V32() V37() integer set

(Sgm JH) . (h - (len (ll - {P}))) is set

rng (Sgm JH) is finite Element of bool NAT

(Sgm C) . j is set

h is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

h - (len (ll - {P})) is ext-real V32() V37() integer set

k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

k - (len (ll - {P})) is ext-real V32() V37() integer set

(Sgm JH) . (k - (len (ll - {P}))) is set

(Sgm JH) . (h - (len (ll - {P}))) is set

(k - (len (ll - {P}))) + (len (ll - {P})) is ext-real V32() V37() integer set

(h - (len (ll - {P}))) + (len (ll - {P})) is ext-real V32() V37() integer set

[:(dom ll),(dom ll):] is finite set

bool [:(dom ll),(dom ll):] is non empty finite V43() set

F is Relation-like dom ll -defined dom ll -valued Function-like quasi_total bijective finite Element of bool [:(dom ll),(dom ll):]

dom F is finite Element of bool (dom ll)

bool (dom ll) is non empty finite V43() set

j is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set

F .