REAL is set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL
bool REAL is non empty set
INT is set
Funcs (NAT,INT) is non empty functional FUNCTION_DOMAIN of NAT , INT
K490() is non empty Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
K518() is V32() V144() set
K459(K490(),K518()) is V41() V99() V100() V101() V102() L6()
the U1 of K459(K490(),K518()) is set
[:(Funcs (NAT,INT)), the U1 of K459(K490(),K518()):] is set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() Function-like functional ext-real non positive non negative V104() Element of NAT
(Funcs (NAT,INT)) \ (0,0) is functional Element of bool (Funcs (NAT,INT))
bool (Funcs (NAT,INT)) is non empty set
COMPLEX is set
NAT is non empty epsilon-transitive epsilon-connected ordinal set
bool NAT is non empty set
bool NAT is non empty set
RAT is set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() Function-like functional ext-real non positive non negative V104() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
{{},1} is non empty set
K328() is set
bool K328() is non empty set
K329() is Element of bool K328()
BOOLEAN is non empty set
{0,1} is non empty set
K418() is V41() V114() L7()
the U1 of K418() is set
K332( the U1 of K418()) is non empty M18( the U1 of K418())
K417(K418()) is Element of bool K332( the U1 of K418())
bool K332( the U1 of K418()) is non empty set
[:K417(K418()),NAT:] is set
bool [:K417(K418()),NAT:] is non empty set
[:NAT,K417(K418()):] is set
bool [:NAT,K417(K418()):] is non empty set
ExtREAL is set
HP-WFF is non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed set
bool HP-WFF is non empty set
Seg 1 is Element of bool NAT
{1} is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
Seg 2 is Element of bool NAT
{1,2} is non empty set
FALSE is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
TRUE is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
p is set
q is Relation-like NAT -defined p -valued Function-like FinSequence-like FinSequence of p
len q is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
q . F is set
q /. F is Element of p
Seg (len q) is Element of bool NAT
dom q is Element of bool NAT
p is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
q is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
p => q is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' p is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - p is V11() V12() ext-real set
('not' p) 'or' q is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' ('not' p) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - ('not' p) is V11() V12() ext-real set
'not' q is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - q is V11() V12() ext-real set
('not' ('not' p)) '&' ('not' q) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
('not' ('not' p)) * ('not' q) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
'not' (('not' ('not' p)) '&' ('not' q)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (('not' ('not' p)) '&' ('not' q)) is V11() V12() ext-real set
F is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
q '&' F is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
q * F is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
p => (q '&' F) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
('not' p) 'or' (q '&' F) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' (q '&' F) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (q '&' F) is V11() V12() ext-real set
('not' ('not' p)) '&' ('not' (q '&' F)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
('not' ('not' p)) * ('not' (q '&' F)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
'not' (('not' ('not' p)) '&' ('not' (q '&' F))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (('not' ('not' p)) '&' ('not' (q '&' F))) is V11() V12() ext-real set
(p => (q '&' F)) => (p => q) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' (p => (q '&' F)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (p => (q '&' F)) is V11() V12() ext-real set
('not' (p => (q '&' F))) 'or' (p => q) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' ('not' (p => (q '&' F))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - ('not' (p => (q '&' F))) is V11() V12() ext-real set
'not' (p => q) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (p => q) is V11() V12() ext-real set
('not' ('not' (p => (q '&' F)))) '&' ('not' (p => q)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
('not' ('not' (p => (q '&' F)))) * ('not' (p => q)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
'not' (('not' ('not' (p => (q '&' F)))) '&' ('not' (p => q))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (('not' ('not' (p => (q '&' F)))) '&' ('not' (p => q))) is V11() V12() ext-real set
p is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
q is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
p '&' q is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
p * q is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
F is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
q => F is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' q is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - q is V11() V12() ext-real set
('not' q) 'or' F is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' ('not' q) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - ('not' q) is V11() V12() ext-real set
'not' F is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - F is V11() V12() ext-real set
('not' ('not' q)) '&' ('not' F) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
('not' ('not' q)) * ('not' F) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
'not' (('not' ('not' q)) '&' ('not' F)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (('not' ('not' q)) '&' ('not' F)) is V11() V12() ext-real set
p => (q => F) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' p is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - p is V11() V12() ext-real set
('not' p) 'or' (q => F) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' ('not' p) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - ('not' p) is V11() V12() ext-real set
'not' (q => F) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (q => F) is V11() V12() ext-real set
('not' ('not' p)) '&' ('not' (q => F)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
('not' ('not' p)) * ('not' (q => F)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
'not' (('not' ('not' p)) '&' ('not' (q => F))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (('not' ('not' p)) '&' ('not' (q => F))) is V11() V12() ext-real set
(p '&' q) => F is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' (p '&' q) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (p '&' q) is V11() V12() ext-real set
('not' (p '&' q)) 'or' F is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' ('not' (p '&' q)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - ('not' (p '&' q)) is V11() V12() ext-real set
('not' ('not' (p '&' q))) '&' ('not' F) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
('not' ('not' (p '&' q))) * ('not' F) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
'not' (('not' ('not' (p '&' q))) '&' ('not' F)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (('not' ('not' (p '&' q))) '&' ('not' F)) is V11() V12() ext-real set
(p => (q => F)) => ((p '&' q) => F) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' (p => (q => F)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (p => (q => F)) is V11() V12() ext-real set
('not' (p => (q => F))) 'or' ((p '&' q) => F) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' ('not' (p => (q => F))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - ('not' (p => (q => F))) is V11() V12() ext-real set
'not' ((p '&' q) => F) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - ((p '&' q) => F) is V11() V12() ext-real set
('not' ('not' (p => (q => F)))) '&' ('not' ((p '&' q) => F)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
('not' ('not' (p => (q => F)))) * ('not' ((p '&' q) => F)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
'not' (('not' ('not' (p => (q => F)))) '&' ('not' ((p '&' q) => F))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (('not' ('not' (p => (q => F)))) '&' ('not' ((p '&' q) => F))) is V11() V12() ext-real set
p is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
q is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
p '&' q is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
p * q is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
F is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
(p '&' q) => F is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' (p '&' q) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (p '&' q) is V11() V12() ext-real set
('not' (p '&' q)) 'or' F is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' ('not' (p '&' q)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - ('not' (p '&' q)) is V11() V12() ext-real set
'not' F is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - F is V11() V12() ext-real set
('not' ('not' (p '&' q))) '&' ('not' F) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
('not' ('not' (p '&' q))) * ('not' F) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
'not' (('not' ('not' (p '&' q))) '&' ('not' F)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (('not' ('not' (p '&' q))) '&' ('not' F)) is V11() V12() ext-real set
q => F is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' q is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - q is V11() V12() ext-real set
('not' q) 'or' F is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' ('not' q) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - ('not' q) is V11() V12() ext-real set
('not' ('not' q)) '&' ('not' F) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
('not' ('not' q)) * ('not' F) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
'not' (('not' ('not' q)) '&' ('not' F)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (('not' ('not' q)) '&' ('not' F)) is V11() V12() ext-real set
p => (q => F) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' p is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - p is V11() V12() ext-real set
('not' p) 'or' (q => F) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' ('not' p) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - ('not' p) is V11() V12() ext-real set
'not' (q => F) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (q => F) is V11() V12() ext-real set
('not' ('not' p)) '&' ('not' (q => F)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
('not' ('not' p)) * ('not' (q => F)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
'not' (('not' ('not' p)) '&' ('not' (q => F))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (('not' ('not' p)) '&' ('not' (q => F))) is V11() V12() ext-real set
((p '&' q) => F) => (p => (q => F)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' ((p '&' q) => F) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - ((p '&' q) => F) is V11() V12() ext-real set
('not' ((p '&' q) => F)) 'or' (p => (q => F)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' ('not' ((p '&' q) => F)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - ('not' ((p '&' q) => F)) is V11() V12() ext-real set
'not' (p => (q => F)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (p => (q => F)) is V11() V12() ext-real set
('not' ('not' ((p '&' q) => F))) '&' ('not' (p => (q => F))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
('not' ('not' ((p '&' q) => F))) * ('not' (p => (q => F))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
'not' (('not' ('not' ((p '&' q) => F))) '&' ('not' (p => (q => F)))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (('not' ('not' ((p '&' q) => F))) '&' ('not' (p => (q => F)))) is V11() V12() ext-real set
p is Relation-like Function-like FinSequence-like Element of HP-WFF
p is Relation-like Function-like FinSequence-like Element of HP-WFF
p => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
VERUM '&' p is Relation-like Function-like FinSequence-like Element of HP-WFF
(VERUM) is Relation-like Function-like FinSequence-like Element of HP-WFF
VERUM => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
() is Relation-like Function-like FinSequence-like Element of HP-WFF
p is Relation-like Function-like FinSequence-like Element of HP-WFF
q is Relation-like Function-like FinSequence-like Element of HP-WFF
q => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
p => (q => VERUM) is Relation-like Function-like FinSequence-like Element of HP-WFF
(p => (q => VERUM)) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
p is Relation-like Function-like FinSequence-like Element of HP-WFF
(p) is Relation-like Function-like FinSequence-like Element of HP-WFF
p => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
q is Relation-like Function-like FinSequence-like Element of HP-WFF
(q) is Relation-like Function-like FinSequence-like Element of HP-WFF
q => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
((p),(q)) is Relation-like Function-like FinSequence-like Element of HP-WFF
(q) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
(p) => ((q) => VERUM) is Relation-like Function-like FinSequence-like Element of HP-WFF
((p) => ((q) => VERUM)) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
(((p),(q))) is Relation-like Function-like FinSequence-like Element of HP-WFF
((p),(q)) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
p is Relation-like Function-like FinSequence-like Element of HP-WFF
(p) is Relation-like Function-like FinSequence-like Element of HP-WFF
p => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
() '&' (p) is Relation-like Function-like FinSequence-like Element of HP-WFF
((),(() '&' (p))) is Relation-like Function-like FinSequence-like Element of HP-WFF
(() '&' (p)) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
() => ((() '&' (p)) => VERUM) is Relation-like Function-like FinSequence-like Element of HP-WFF
(() => ((() '&' (p)) => VERUM)) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
((p),((),(() '&' (p)))) is Relation-like Function-like FinSequence-like Element of HP-WFF
((p)) is Relation-like Function-like FinSequence-like Element of HP-WFF
(p) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
(((),(() '&' (p)))) is Relation-like Function-like FinSequence-like Element of HP-WFF
((),(() '&' (p))) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
(((p)),(((),(() '&' (p))))) is Relation-like Function-like FinSequence-like Element of HP-WFF
(((),(() '&' (p)))) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
((p)) => ((((),(() '&' (p)))) => VERUM) is Relation-like Function-like FinSequence-like Element of HP-WFF
(((p)) => ((((),(() '&' (p)))) => VERUM)) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
((((p)),(((),(() '&' (p)))))) is Relation-like Function-like FinSequence-like Element of HP-WFF
(((p)),(((),(() '&' (p))))) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
(((p),((),(() '&' (p))))) is Relation-like Function-like FinSequence-like Element of HP-WFF
((p),((),(() '&' (p)))) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
p is Relation-like Function-like FinSequence-like Element of HP-WFF
(p) is Relation-like Function-like FinSequence-like Element of HP-WFF
p => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
((p)) is Relation-like Function-like FinSequence-like Element of HP-WFF
((p)) is Relation-like Function-like FinSequence-like Element of HP-WFF
(p) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
() '&' ((p)) is Relation-like Function-like FinSequence-like Element of HP-WFF
((),(() '&' ((p)))) is Relation-like Function-like FinSequence-like Element of HP-WFF
(() '&' ((p))) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
() => ((() '&' ((p))) => VERUM) is Relation-like Function-like FinSequence-like Element of HP-WFF
(() => ((() '&' ((p))) => VERUM)) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
(((p)),((),(() '&' ((p))))) is Relation-like Function-like FinSequence-like Element of HP-WFF
(((p))) is Relation-like Function-like FinSequence-like Element of HP-WFF
((p)) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
(((),(() '&' ((p))))) is Relation-like Function-like FinSequence-like Element of HP-WFF
((),(() '&' ((p)))) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
((((p))),(((),(() '&' ((p)))))) is Relation-like Function-like FinSequence-like Element of HP-WFF
(((),(() '&' ((p))))) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
(((p))) => ((((),(() '&' ((p))))) => VERUM) is Relation-like Function-like FinSequence-like Element of HP-WFF
((((p))) => ((((),(() '&' ((p))))) => VERUM)) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
(((((p))),(((),(() '&' ((p))))))) is Relation-like Function-like FinSequence-like Element of HP-WFF
((((p))),(((),(() '&' ((p)))))) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
((((p)),((),(() '&' ((p)))))) is Relation-like Function-like FinSequence-like Element of HP-WFF
(((p)),((),(() '&' ((p))))) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
(((p))) is Relation-like Function-like FinSequence-like Element of HP-WFF
((p)) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
q is Relation-like Function-like FinSequence-like Element of HP-WFF
p is Relation-like Function-like FinSequence-like Element of HP-WFF
p '&' q is Relation-like Function-like FinSequence-like Element of HP-WFF
(p,(p '&' q)) is Relation-like Function-like FinSequence-like Element of HP-WFF
(p '&' q) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
p => ((p '&' q) => VERUM) is Relation-like Function-like FinSequence-like Element of HP-WFF
(p => ((p '&' q) => VERUM)) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
(q,(p,(p '&' q))) is Relation-like Function-like FinSequence-like Element of HP-WFF
(q) is Relation-like Function-like FinSequence-like Element of HP-WFF
q => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
((p,(p '&' q))) is Relation-like Function-like FinSequence-like Element of HP-WFF
(p,(p '&' q)) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
((q),((p,(p '&' q)))) is Relation-like Function-like FinSequence-like Element of HP-WFF
((p,(p '&' q))) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
(q) => (((p,(p '&' q))) => VERUM) is Relation-like Function-like FinSequence-like Element of HP-WFF
((q) => (((p,(p '&' q))) => VERUM)) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
(((q),((p,(p '&' q))))) is Relation-like Function-like FinSequence-like Element of HP-WFF
((q),((p,(p '&' q)))) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
p is Relation-like Function-like FinSequence-like Element of HP-WFF
(p) is Relation-like Function-like FinSequence-like Element of HP-WFF
p => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
q is Relation-like Function-like FinSequence-like Element of HP-WFF
(q) is Relation-like Function-like FinSequence-like Element of HP-WFF
q => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
((p),(q)) is Relation-like Function-like FinSequence-like Element of HP-WFF
(p) '&' (q) is Relation-like Function-like FinSequence-like Element of HP-WFF
((p),((p) '&' (q))) is Relation-like Function-like FinSequence-like Element of HP-WFF
((p) '&' (q)) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
(p) => (((p) '&' (q)) => VERUM) is Relation-like Function-like FinSequence-like Element of HP-WFF
((p) => (((p) '&' (q)) => VERUM)) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
((q),((p),((p) '&' (q)))) is Relation-like Function-like FinSequence-like Element of HP-WFF
((q)) is Relation-like Function-like FinSequence-like Element of HP-WFF
(q) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
(((p),((p) '&' (q)))) is Relation-like Function-like FinSequence-like Element of HP-WFF
((p),((p) '&' (q))) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
(((q)),(((p),((p) '&' (q))))) is Relation-like Function-like FinSequence-like Element of HP-WFF
(((p),((p) '&' (q)))) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
((q)) => ((((p),((p) '&' (q)))) => VERUM) is Relation-like Function-like FinSequence-like Element of HP-WFF
(((q)) => ((((p),((p) '&' (q)))) => VERUM)) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
((((q)),(((p),((p) '&' (q)))))) is Relation-like Function-like FinSequence-like Element of HP-WFF
(((q)),(((p),((p) '&' (q))))) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
(((p),(q))) is Relation-like Function-like FinSequence-like Element of HP-WFF
((p),(q)) => VERUM is Relation-like Function-like FinSequence-like Element of HP-WFF
p is set
q is set
q is functional Element of bool HP-WFF
F is set
G is set
f is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
prop f is Relation-like Function-like FinSequence-like Element of HP-WFF
p is functional Element of bool HP-WFF
q is functional Element of bool HP-WFF
F is set
G is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
prop G is Relation-like Function-like FinSequence-like Element of HP-WFF
F is set
G is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
prop G is Relation-like Function-like FinSequence-like Element of HP-WFF
() is functional Element of bool HP-WFF
bool () is non empty set
[:NAT,(bool ()):] is non empty set
bool [:NAT,(bool ()):] is non empty set
[:NAT,HP-WFF:] is non empty set
[:[:NAT,HP-WFF:],BOOLEAN:] is non empty set
bool [:[:NAT,HP-WFF:],BOOLEAN:] is non empty set
p is non empty Relation-like NAT -defined bool () -valued Function-like total quasi_total Element of bool [:NAT,(bool ()):]
Funcs (NAT,BOOLEAN) is non empty functional FUNCTION_DOMAIN of NAT , BOOLEAN
[:NAT,BOOLEAN:] is non empty set
bool [:NAT,BOOLEAN:] is non empty set
FALSE is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
NAT --> FALSE is non empty T-Sequence-like Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
F is Relation-like Function-like FinSequence-like Element of HP-WFF
G is Relation-like Function-like FinSequence-like Element of HP-WFF
f is set
i is set
q is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
j is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
r is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
r + B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
q . (r + B) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
r is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
r + B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
q . (r + B) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
r + B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
q . (r + B) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
r is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
r + B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
q . (r + B) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
r is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
F is Relation-like Function-like FinSequence-like Element of HP-WFF
G is Relation-like Function-like FinSequence-like Element of HP-WFF
f is set
i is set
j is set
q is set
r is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
B is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
Gp is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
r is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
B is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
Gp is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
XGp is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
XA is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
Xq is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
XGp is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
XA is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
Xq is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
GB is set
s4 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
Xq . s4 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
Xq . GB is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
Gp . GB is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
s5 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
s4 + s5 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
B . (s4 + s5) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
s4 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
Xq . s4 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
s5 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
s4 + s5 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
B . (s4 + s5) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
Gp . s4 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
Xq . GB is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
Gp . GB is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
s4 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
Xq . s4 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
r is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
B is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
Gp is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
XGp is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
XA is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
Xq is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
F is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
prop F is Relation-like Function-like FinSequence-like Element of HP-WFF
G is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
p . G is functional Element of bool ()
TRUE is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
G is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
p . G is functional Element of bool ()
G is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
p . G is functional Element of bool ()
G is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
f is Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total Element of Funcs (NAT,BOOLEAN)
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
f . i is set
p . i is functional Element of bool ()
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
p . j is functional Element of bool ()
f . j is set
[:NAT,(Funcs (NAT,BOOLEAN)):] is non empty set
bool [:NAT,(Funcs (NAT,BOOLEAN)):] is non empty set
F is non empty Relation-like NAT -defined Funcs (NAT,BOOLEAN) -valued Function-like total quasi_total Element of bool [:NAT,(Funcs (NAT,BOOLEAN)):]
G is Relation-like Function-like FinSequence-like Element of HP-WFF
f is Relation-like Function-like FinSequence-like Element of HP-WFF
i is set
j is set
q is set
r is set
B is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
Gp is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
XGp is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
B is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
Gp is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
XGp is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
XA is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
Xq is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
GB is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
XA is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
Xq is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
GB is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
s4 is set
GB . s4 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
s5 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
B . s5 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
Xq . s5 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
(B . s5) => (Xq . s5) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' (B . s5) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (B . s5) is V11() V12() ext-real set
('not' (B . s5)) 'or' (Xq . s5) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' ('not' (B . s5)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - ('not' (B . s5)) is V11() V12() ext-real set
'not' (Xq . s5) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (Xq . s5) is V11() V12() ext-real set
('not' ('not' (B . s5))) '&' ('not' (Xq . s5)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
('not' ('not' (B . s5))) * ('not' (Xq . s5)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
'not' (('not' ('not' (B . s5))) '&' ('not' (Xq . s5))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (('not' ('not' (B . s5))) '&' ('not' (Xq . s5))) is V11() V12() ext-real set
XGp . s4 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
B is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
Gp is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
XGp is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
XA is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
Xq is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
GB is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
G is Relation-like Function-like FinSequence-like Element of HP-WFF
f is Relation-like Function-like FinSequence-like Element of HP-WFF
i is set
j is set
q is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
r is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
B is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
Gp is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
B . Gp is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
q . Gp is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
r . Gp is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
(q . Gp) => (r . Gp) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' (q . Gp) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (q . Gp) is V11() V12() ext-real set
('not' (q . Gp)) 'or' (r . Gp) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' ('not' (q . Gp)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - ('not' (q . Gp)) is V11() V12() ext-real set
'not' (r . Gp) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (r . Gp) is V11() V12() ext-real set
('not' ('not' (q . Gp))) '&' ('not' (r . Gp)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
('not' ('not' (q . Gp))) * ('not' (r . Gp)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
'not' (('not' ('not' (q . Gp))) '&' ('not' (r . Gp))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (('not' ('not' (q . Gp))) '&' ('not' (r . Gp))) is V11() V12() ext-real set
G is Relation-like HP-WFF -defined Function-like total set
G . VERUM is set
f is Relation-like Function-like FinSequence-like Element of HP-WFF
i is Relation-like Function-like FinSequence-like Element of HP-WFF
G . f is set
G . i is set
f => i is Relation-like Function-like FinSequence-like Element of HP-WFF
G . (f => i) is set
j is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
q is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
r is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
j is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
q is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
r is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
f is Relation-like Function-like FinSequence-like Element of HP-WFF
i is Relation-like Function-like FinSequence-like Element of HP-WFF
G . f is set
G . i is set
f '&' i is Relation-like Function-like FinSequence-like Element of HP-WFF
G . (f '&' i) is set
j is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
q is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
r is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
j is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
q is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
r is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
f is set
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
prop j is Relation-like Function-like FinSequence-like Element of HP-WFF
G . (prop j) is set
F . j is Relation-like Function-like Element of Funcs (NAT,BOOLEAN)
i is Relation-like Function-like FinSequence-like Element of HP-WFF
G . f is set
i is Relation-like Function-like FinSequence-like Element of HP-WFF
G . f is set
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
prop j is Relation-like Function-like FinSequence-like Element of HP-WFF
i is Relation-like Function-like FinSequence-like Element of HP-WFF
G . f is set
j is Relation-like Function-like FinSequence-like Element of HP-WFF
q is Relation-like Function-like FinSequence-like Element of HP-WFF
j '&' q is Relation-like Function-like FinSequence-like Element of HP-WFF
i is Relation-like Function-like FinSequence-like Element of HP-WFF
G . f is set
j is Relation-like Function-like FinSequence-like Element of HP-WFF
q is Relation-like Function-like FinSequence-like Element of HP-WFF
j => q is Relation-like Function-like FinSequence-like Element of HP-WFF
i is Relation-like Function-like FinSequence-like Element of HP-WFF
dom G is set
[:HP-WFF,(Funcs (NAT,BOOLEAN)):] is non empty set
bool [:HP-WFF,(Funcs (NAT,BOOLEAN)):] is non empty set
f is non empty Relation-like HP-WFF -defined Funcs (NAT,BOOLEAN) -valued Function-like total quasi_total Element of bool [:HP-WFF,(Funcs (NAT,BOOLEAN)):]
i is non empty Relation-like [:NAT,HP-WFF:] -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:[:NAT,HP-WFF:],BOOLEAN:]
q is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is Relation-like Function-like FinSequence-like Element of HP-WFF
[q,j] is Element of [:NAT,HP-WFF:]
{q,j} is non empty set
{q} is non empty set
{{q,j},{q}} is non empty set
i . [q,j] is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
i . (q,j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
f . j is Relation-like Function-like Element of Funcs (NAT,BOOLEAN)
(f . j) . q is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
q is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
prop j is Relation-like Function-like FinSequence-like Element of HP-WFF
[q,(prop j)] is Element of [:NAT,HP-WFF:]
{q,(prop j)} is non empty set
{q} is non empty set
{{q,(prop j)},{q}} is non empty set
i . [q,(prop j)] is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
f . (prop j) is Relation-like Function-like Element of Funcs (NAT,BOOLEAN)
(f . (prop j)) . q is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
F . j is Relation-like Function-like Element of Funcs (NAT,BOOLEAN)
(F . j) . q is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
p . q is functional Element of bool ()
j is Relation-like Function-like FinSequence-like Element of HP-WFF
f . j is Relation-like Function-like Element of Funcs (NAT,BOOLEAN)
q is Relation-like Function-like FinSequence-like Element of HP-WFF
f . q is Relation-like Function-like Element of Funcs (NAT,BOOLEAN)
B is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
Gp is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
j '&' q is Relation-like Function-like FinSequence-like Element of HP-WFF
f . (j '&' q) is Relation-like Function-like Element of Funcs (NAT,BOOLEAN)
XGp is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
XA is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
Xq is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
j => q is Relation-like Function-like FinSequence-like Element of HP-WFF
f . (j => q) is Relation-like Function-like Element of Funcs (NAT,BOOLEAN)
GB is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
s4 is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
s5 is non empty Relation-like NAT -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:NAT,BOOLEAN:]
r is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
[r,(j => q)] is Element of [:NAT,HP-WFF:]
{r,(j => q)} is non empty set
{r} is non empty set
{{r,(j => q)},{r}} is non empty set
i . [r,(j => q)] is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
(f . (j => q)) . r is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
(f . j) . r is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
s4 . r is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
((f . j) . r) => (s4 . r) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' ((f . j) . r) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - ((f . j) . r) is V11() V12() ext-real set
('not' ((f . j) . r)) 'or' (s4 . r) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' ('not' ((f . j) . r)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - ('not' ((f . j) . r)) is V11() V12() ext-real set
'not' (s4 . r) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (s4 . r) is V11() V12() ext-real set
('not' ('not' ((f . j) . r))) '&' ('not' (s4 . r)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
('not' ('not' ((f . j) . r))) * ('not' (s4 . r)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
'not' (('not' ('not' ((f . j) . r))) '&' ('not' (s4 . r))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (('not' ('not' ((f . j) . r))) '&' ('not' (s4 . r))) is V11() V12() ext-real set
[r,j] is Element of [:NAT,HP-WFF:]
{r,j} is non empty set
{{r,j},{r}} is non empty set
i . [r,j] is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
(f . q) . r is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
(i . [r,j]) => ((f . q) . r) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' (i . [r,j]) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (i . [r,j]) is V11() V12() ext-real set
('not' (i . [r,j])) 'or' ((f . q) . r) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' ('not' (i . [r,j])) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - ('not' (i . [r,j])) is V11() V12() ext-real set
'not' ((f . q) . r) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - ((f . q) . r) is V11() V12() ext-real set
('not' ('not' (i . [r,j]))) '&' ('not' ((f . q) . r)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
('not' ('not' (i . [r,j]))) * ('not' ((f . q) . r)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
'not' (('not' ('not' (i . [r,j]))) '&' ('not' ((f . q) . r))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (('not' ('not' (i . [r,j]))) '&' ('not' ((f . q) . r))) is V11() V12() ext-real set
[r,q] is Element of [:NAT,HP-WFF:]
{r,q} is non empty set
{{r,q},{r}} is non empty set
i . [r,q] is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
(i . [r,j]) => (i . [r,q]) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
('not' (i . [r,j])) 'or' (i . [r,q]) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' (i . [r,q]) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (i . [r,q]) is V11() V12() ext-real set
('not' ('not' (i . [r,j]))) '&' ('not' (i . [r,q])) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
('not' ('not' (i . [r,j]))) * ('not' (i . [r,q])) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
'not' (('not' ('not' (i . [r,j]))) '&' ('not' (i . [r,q]))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (('not' ('not' (i . [r,j]))) '&' ('not' (i . [r,q]))) is V11() V12() ext-real set
[r,(j '&' q)] is Element of [:NAT,HP-WFF:]
{r,(j '&' q)} is non empty set
{{r,(j '&' q)},{r}} is non empty set
i . [r,(j '&' q)] is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
Xq . r is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
r + i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
XA . (r + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
r + j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
[(r + j),j] is Element of [:NAT,HP-WFF:]
{(r + j),j} is non empty set
{(r + j)} is non empty set
{{(r + j),j},{(r + j)}} is non empty set
i . [(r + j),j] is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
(f . j) . (r + j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
[(r + i),q] is Element of [:NAT,HP-WFF:]
{(r + i),q} is non empty set
{(r + i)} is non empty set
{{(r + i),q},{(r + i)}} is non empty set
i . [(r + i),q] is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
r + i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
[(r + i),q] is Element of [:NAT,HP-WFF:]
{(r + i),q} is non empty set
{(r + i)} is non empty set
{{(r + i),q},{(r + i)}} is non empty set
i . [(r + i),q] is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
r + i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
[(r + i),q] is Element of [:NAT,HP-WFF:]
{(r + i),q} is non empty set
{(r + i)} is non empty set
{{(r + i),q},{(r + i)}} is non empty set
i . [(r + i),q] is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
XA . (r + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
r + j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
XGp . (r + j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
[(r + j),j] is Element of [:NAT,HP-WFF:]
{(r + j),j} is non empty set
{(r + j)} is non empty set
{{(r + j),j},{(r + j)}} is non empty set
i . [(r + j),j] is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
[j,VERUM] is Element of [:NAT,HP-WFF:]
{j,VERUM} is non empty set
{j} is non empty set
{{j,VERUM},{j}} is non empty set
i . [j,VERUM] is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
f . VERUM is Relation-like Function-like Element of Funcs (NAT,BOOLEAN)
(f . VERUM) . j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
[j,VERUM] is Element of [:NAT,HP-WFF:]
{j,VERUM} is non empty set
{j} is non empty set
{{j,VERUM},{j}} is non empty set
i . [j,VERUM] is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
q is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
prop r is Relation-like Function-like FinSequence-like Element of HP-WFF
[q,(prop r)] is Element of [:NAT,HP-WFF:]
{q,(prop r)} is non empty set
{q} is non empty set
{{q,(prop r)},{q}} is non empty set
i . [q,(prop r)] is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
p . q is functional Element of bool ()
Gp is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
prop Gp is Relation-like Function-like FinSequence-like Element of HP-WFF
B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
p . B is functional Element of bool ()
[B,(prop Gp)] is Element of [:NAT,HP-WFF:]
{B,(prop Gp)} is non empty set
{B} is non empty set
{{B,(prop Gp)},{B}} is non empty set
i . [B,(prop Gp)] is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
XGp is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
XA is Relation-like Function-like FinSequence-like Element of HP-WFF
Xq is Relation-like Function-like FinSequence-like Element of HP-WFF
XA => Xq is Relation-like Function-like FinSequence-like Element of HP-WFF
[XGp,(XA => Xq)] is Element of [:NAT,HP-WFF:]
{XGp,(XA => Xq)} is non empty set
{XGp} is non empty set
{{XGp,(XA => Xq)},{XGp}} is non empty set
i . [XGp,(XA => Xq)] is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
[XGp,XA] is Element of [:NAT,HP-WFF:]
{XGp,XA} is non empty set
{{XGp,XA},{XGp}} is non empty set
i . [XGp,XA] is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
[XGp,Xq] is Element of [:NAT,HP-WFF:]
{XGp,Xq} is non empty set
{{XGp,Xq},{XGp}} is non empty set
i . [XGp,Xq] is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
(i . [XGp,XA]) => (i . [XGp,Xq]) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' (i . [XGp,XA]) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (i . [XGp,XA]) is V11() V12() ext-real set
('not' (i . [XGp,XA])) 'or' (i . [XGp,Xq]) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
'not' ('not' (i . [XGp,XA])) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - ('not' (i . [XGp,XA])) is V11() V12() ext-real set
'not' (i . [XGp,Xq]) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (i . [XGp,Xq]) is V11() V12() ext-real set
('not' ('not' (i . [XGp,XA]))) '&' ('not' (i . [XGp,Xq])) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
('not' ('not' (i . [XGp,XA]))) * ('not' (i . [XGp,Xq])) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
'not' (('not' ('not' (i . [XGp,XA]))) '&' ('not' (i . [XGp,Xq]))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean set
1 - (('not' ('not' (i . [XGp,XA]))) '&' ('not' (i . [XGp,Xq]))) is V11() V12() ext-real set
GB is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
s4 is Relation-like Function-like FinSequence-like Element of HP-WFF
s5 is Relation-like Function-like FinSequence-like Element of HP-WFF
s4 '&' s5 is Relation-like Function-like FinSequence-like Element of HP-WFF
[GB,(s4 '&' s5)] is Element of [:NAT,HP-WFF:]
{GB,(s4 '&' s5)} is non empty set
{GB} is non empty set
{{GB,(s4 '&' s5)},{GB}} is non empty set
i . [GB,(s4 '&' s5)] is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
c21 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
i + c21 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
c20 is Relation-like Function-like FinSequence-like Element of HP-WFF
[(i + c21),c20] is Element of [:NAT,HP-WFF:]
{(i + c21),c20} is non empty set
{(i + c21)} is non empty set
{{(i + c21),c20},{(i + c21)}} is non empty set
i . [(i + c21),c20] is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
j is Relation-like Function-like FinSequence-like Element of HP-WFF
j '&' c20 is Relation-like Function-like FinSequence-like Element of HP-WFF
[i,(j '&' c20)] is Element of [:NAT,HP-WFF:]
{i,(j '&' c20)} is non empty set
{i} is non empty set
{{i,(j '&' c20)},{i}} is non empty set
i . [i,(j '&' c20)] is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative boolean Element of BOOLEAN
q is non empty Relation-like [:NAT,HP-WFF:] -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:[:NAT,HP-WFF:],BOOLEAN:]
F is non empty Relation-like [:NAT,HP-WFF:] -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:[:NAT,HP-WFF:],BOOLEAN:]
G is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
prop G is Relation-like Function-like FinSequence-like Element of HP-WFF
f is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
p . f is functional Element of bool ()
[f,(prop G)] is Element of [:NAT,HP-WFF:]
{f,(prop G)