REAL is set
NAT is non empty V8() V9() V10() Element of bool REAL
bool REAL is non empty set
NAT is non empty V8() V9() V10() set
bool NAT is non empty set
bool NAT is non empty set
VAR is non empty Element of bool NAT
5 is ext-real positive non negative non empty V8() V9() V10() V14() Element of NAT
{ b1 where b1 is ext-real non negative V8() V9() V10() V14() Element of NAT : 5 <= b1 } is set
bool VAR is non empty set
1 is ext-real positive non negative non empty V8() V9() V10() V14() Element of NAT
2 is ext-real positive non negative non empty V8() V9() V10() V14() Element of NAT
3 is ext-real positive non negative non empty V8() V9() V10() V14() Element of NAT
Seg 1 is non empty finite V40(1) Element of bool NAT
{1} is non empty finite set
Seg 2 is non empty finite V40(2) Element of bool NAT
{1,2} is non empty finite set
Seg 3 is non empty finite V40(3) Element of bool NAT
{1,2,3} is non empty finite set
{} is ext-real non positive non negative empty V8() V9() V10() V12() V13() V14() functional finite V37() FinSequence-membered set
the ext-real non positive non negative empty V8() V9() V10() V12() V13() V14() functional finite V37() FinSequence-membered set is ext-real non positive non negative empty V8() V9() V10() V12() V13() V14() functional finite V37() FinSequence-membered set
WFF is non empty set
0 is ext-real non positive non negative empty V8() V9() V10() V12() V13() V14() functional finite V37() FinSequence-membered Element of NAT
4 is ext-real positive non negative non empty V8() V9() V10() V14() Element of NAT
H is Element of VAR
x is Element of VAR
H '=' x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*0*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*H*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ <*H*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
1 + 1 is ext-real positive non negative non empty V8() V9() V10() V14() Element of NAT
<*x*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*0*> ^ <*H*>) ^ <*x*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(1 + 1) + 1 is ext-real positive non negative non empty V8() V9() V10() V14() Element of NAT
Var1 (H '=' x) is Element of VAR
Var2 (H '=' x) is Element of VAR
(Var1 (H '=' x)) '=' (Var2 (H '=' x)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*(Var1 (H '=' x))*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ <*(Var1 (H '=' x))*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*(Var2 (H '=' x))*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*0*> ^ <*(Var1 (H '=' x))*>) ^ <*(Var2 (H '=' x))*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
H is Element of VAR
x is Element of VAR
H 'in' x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*1*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*H*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ <*H*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
1 + 1 is ext-real positive non negative non empty V8() V9() V10() V14() Element of NAT
<*x*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ <*H*>) ^ <*x*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(1 + 1) + 1 is ext-real positive non negative non empty V8() V9() V10() V14() Element of NAT
Var1 (H 'in' x) is Element of VAR
Var2 (H 'in' x) is Element of VAR
(Var1 (H 'in' x)) 'in' (Var2 (H 'in' x)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*(Var1 (H 'in' x))*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ <*(Var1 (H 'in' x))*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*(Var2 (H 'in' x))*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ <*(Var1 (H 'in' x))*>) ^ <*(Var2 (H 'in' x))*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
the_argument_of ('not' H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
H '&' x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*3*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*3*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ H) ^ x is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
the_left_argument_of (H '&' x) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
the_right_argument_of (H '&' x) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
(the_left_argument_of (H '&' x)) '&' (the_right_argument_of (H '&' x)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*3*> ^ (the_left_argument_of (H '&' x)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ (the_left_argument_of (H '&' x))) ^ (the_right_argument_of (H '&' x)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
H 'or' x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ x is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
('not' H) '&' ('not' x) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*3*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*3*> ^ ('not' H) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ ('not' H)) ^ ('not' x) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' (('not' H) '&' ('not' x)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (('not' H) '&' ('not' x)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
the_left_argument_of (H 'or' x) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
the_right_argument_of (H 'or' x) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
(the_left_argument_of (H 'or' x)) 'or' (the_right_argument_of (H 'or' x)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' (the_left_argument_of (H 'or' x)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (the_left_argument_of (H 'or' x)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' (the_right_argument_of (H 'or' x)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (the_right_argument_of (H 'or' x)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
('not' (the_left_argument_of (H 'or' x))) '&' ('not' (the_right_argument_of (H 'or' x))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*3*> ^ ('not' (the_left_argument_of (H 'or' x))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ ('not' (the_left_argument_of (H 'or' x)))) ^ ('not' (the_right_argument_of (H 'or' x))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' (('not' (the_left_argument_of (H 'or' x))) '&' ('not' (the_right_argument_of (H 'or' x)))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (('not' (the_left_argument_of (H 'or' x))) '&' ('not' (the_right_argument_of (H 'or' x)))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
H => x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> ^ x is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
H '&' ('not' x) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*3*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*3*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ H) ^ ('not' x) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' (H '&' ('not' x)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (H '&' ('not' x)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
the_antecedent_of (H => x) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
the_consequent_of (H => x) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
(the_antecedent_of (H => x)) => (the_consequent_of (H => x)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' (the_consequent_of (H => x)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (the_consequent_of (H => x)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(the_antecedent_of (H => x)) '&' ('not' (the_consequent_of (H => x))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*3*> ^ (the_antecedent_of (H => x)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ (the_antecedent_of (H => x))) ^ ('not' (the_consequent_of (H => x))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' ((the_antecedent_of (H => x)) '&' ('not' (the_consequent_of (H => x)))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ ((the_antecedent_of (H => x)) '&' ('not' (the_consequent_of (H => x)))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
H <=> x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
H => x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> ^ x is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
H '&' ('not' x) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*3*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*3*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ H) ^ ('not' x) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' (H '&' ('not' x)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (H '&' ('not' x)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x => H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x '&' ('not' H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*3*> ^ x is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ x) ^ ('not' H) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' (x '&' ('not' H)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (x '&' ('not' H)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(H => x) '&' (x => H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*3*> ^ (H => x) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ (H => x)) ^ (x => H) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
the_left_side_of (H <=> x) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
the_right_side_of (H <=> x) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
(the_left_side_of (H <=> x)) <=> (the_right_side_of (H <=> x)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
(the_left_side_of (H <=> x)) => (the_right_side_of (H <=> x)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' (the_right_side_of (H <=> x)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (the_right_side_of (H <=> x)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(the_left_side_of (H <=> x)) '&' ('not' (the_right_side_of (H <=> x))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*3*> ^ (the_left_side_of (H <=> x)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ (the_left_side_of (H <=> x))) ^ ('not' (the_right_side_of (H <=> x))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' ((the_left_side_of (H <=> x)) '&' ('not' (the_right_side_of (H <=> x)))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ ((the_left_side_of (H <=> x)) '&' ('not' (the_right_side_of (H <=> x)))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(the_right_side_of (H <=> x)) => (the_left_side_of (H <=> x)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' (the_left_side_of (H <=> x)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (the_left_side_of (H <=> x)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(the_right_side_of (H <=> x)) '&' ('not' (the_left_side_of (H <=> x))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*3*> ^ (the_right_side_of (H <=> x)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ (the_right_side_of (H <=> x))) ^ ('not' (the_left_side_of (H <=> x))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' ((the_right_side_of (H <=> x)) '&' ('not' (the_left_side_of (H <=> x)))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ ((the_right_side_of (H <=> x)) '&' ('not' (the_left_side_of (H <=> x)))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
((the_left_side_of (H <=> x)) => (the_right_side_of (H <=> x))) '&' ((the_right_side_of (H <=> x)) => (the_left_side_of (H <=> x))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*3*> ^ ((the_left_side_of (H <=> x)) => (the_right_side_of (H <=> x))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ ((the_left_side_of (H <=> x)) => (the_right_side_of (H <=> x)))) ^ ((the_right_side_of (H <=> x)) => (the_left_side_of (H <=> x))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
x is Element of VAR
All (x,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*4*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*x*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*x*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
1 + 1 is ext-real positive non negative non empty V8() V9() V10() V14() Element of NAT
(<*4*> ^ <*x*>) ^ H is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
bound_in (All (x,H)) is Element of VAR
the_scope_of (All (x,H)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All ((bound_in (All (x,H))),(the_scope_of (All (x,H)))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*(bound_in (All (x,H)))*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*(bound_in (All (x,H)))*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*(bound_in (All (x,H)))*>) ^ (the_scope_of (All (x,H))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
x is Element of VAR
Ex (x,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (x,('not' H)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*4*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*x*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*x*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
1 + 1 is ext-real positive non negative non empty V8() V9() V10() V14() Element of NAT
(<*4*> ^ <*x*>) ^ ('not' H) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' (All (x,('not' H))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (All (x,('not' H))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
bound_in (Ex (x,H)) is Element of VAR
the_scope_of (Ex (x,H)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
Ex ((bound_in (Ex (x,H))),(the_scope_of (Ex (x,H)))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' (the_scope_of (Ex (x,H))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (the_scope_of (Ex (x,H))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All ((bound_in (Ex (x,H))),('not' (the_scope_of (Ex (x,H))))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*(bound_in (Ex (x,H)))*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*(bound_in (Ex (x,H)))*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*(bound_in (Ex (x,H)))*>) ^ ('not' (the_scope_of (Ex (x,H)))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' (All ((bound_in (Ex (x,H))),('not' (the_scope_of (Ex (x,H)))))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (All ((bound_in (Ex (x,H))),('not' (the_scope_of (Ex (x,H)))))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
H 'or' x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ x is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
('not' H) '&' ('not' x) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*3*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*3*> ^ ('not' H) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ ('not' H)) ^ ('not' x) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' (('not' H) '&' ('not' x)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (('not' H) '&' ('not' x)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
('not' H) => x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
x is Element of VAR
y is Element of VAR
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (x,y,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (y,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*4*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*y*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*y*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
1 + 1 is ext-real positive non negative non empty V8() V9() V10() V14() Element of NAT
(<*4*> ^ <*y*>) ^ H is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (x,(All (y,H))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*x*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*x*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*x*>) ^ (All (y,H)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
z is Element of VAR
b is Element of VAR
a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (z,b,a) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (b,a) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*b*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*b*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*b*>) ^ a is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (z,(All (b,a))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*z*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*z*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*z*>) ^ (All (b,a)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
bound_in (All (z,b,a)) is Element of VAR
H1 is Element of VAR
H2 is Element of VAR
s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (H1,H2,s) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (H2,s) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*H2*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*H2*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*H2*>) ^ s is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (H1,(All (H2,s))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*H1*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*H1*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*H1*>) ^ (All (H2,s)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
the_scope_of (All (H1,H2,s)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
x is Element of VAR
y is Element of VAR
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
Ex (x,y,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
Ex (y,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (y,('not' H)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*4*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*y*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*y*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
1 + 1 is ext-real positive non negative non empty V8() V9() V10() V14() Element of NAT
(<*4*> ^ <*y*>) ^ ('not' H) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' (All (y,('not' H))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (All (y,('not' H))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Ex (x,(Ex (y,H))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' (Ex (y,H)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (Ex (y,H)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (x,('not' (Ex (y,H)))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*x*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*x*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*x*>) ^ ('not' (Ex (y,H))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' (All (x,('not' (Ex (y,H))))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (All (x,('not' (Ex (y,H))))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
z is Element of VAR
b is Element of VAR
a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
Ex (z,b,a) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
Ex (b,a) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ a is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (b,('not' a)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*b*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*b*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*b*>) ^ ('not' a) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' (All (b,('not' a))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (All (b,('not' a))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Ex (z,(Ex (b,a))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' (Ex (b,a)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (Ex (b,a)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (z,('not' (Ex (b,a)))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*z*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*z*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*z*>) ^ ('not' (Ex (b,a))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' (All (z,('not' (Ex (b,a))))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (All (z,('not' (Ex (b,a))))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
bound_in (Ex (z,b,a)) is Element of VAR
H1 is Element of VAR
H2 is Element of VAR
s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
Ex (H1,H2,s) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
Ex (H2,s) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ s is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (H2,('not' s)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*H2*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*H2*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*H2*>) ^ ('not' s) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' (All (H2,('not' s))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (All (H2,('not' s))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Ex (H1,(Ex (H2,s))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' (Ex (H2,s)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (Ex (H2,s)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (H1,('not' (Ex (H2,s)))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*H1*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*H1*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*H1*>) ^ ('not' (Ex (H2,s))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' (All (H1,('not' (Ex (H2,s))))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (All (H1,('not' (Ex (H2,s))))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
the_scope_of (Ex (H1,H2,s)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
x is Element of VAR
y is Element of VAR
a is Element of VAR
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (x,y,a,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (y,a,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (a,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*4*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*a*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*a*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
1 + 1 is ext-real positive non negative non empty V8() V9() V10() V14() Element of NAT
(<*4*> ^ <*a*>) ^ H is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (y,(All (a,H))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*y*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*y*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*y*>) ^ (All (a,H)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (x,(All (y,a,H))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*x*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*x*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*x*>) ^ (All (y,a,H)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (x,(All (y,(All (a,H))))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
(<*4*> ^ <*x*>) ^ (All (y,(All (a,H)))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
b is Element of VAR
s is Element of VAR
H1 is Element of VAR
z is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (b,s,H1,z) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (s,H1,z) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (H1,z) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*H1*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*H1*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*H1*>) ^ z is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (s,(All (H1,z))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*s*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*s*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*s*>) ^ (All (H1,z)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (b,(All (s,H1,z))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*b*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*b*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*b*>) ^ (All (s,H1,z)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (b,s,(All (H1,z))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (b,(All (s,(All (H1,z))))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
(<*4*> ^ <*b*>) ^ (All (s,(All (H1,z)))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
y is Element of VAR
a is Element of VAR
All (y,a,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (a,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*4*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*a*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*a*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
1 + 1 is ext-real positive non negative non empty V8() V9() V10() V14() Element of NAT
(<*4*> ^ <*a*>) ^ H is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (y,(All (a,H))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*y*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*y*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*y*>) ^ (All (a,H)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
z is Element of VAR
b is Element of VAR
All (z,b,x) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (b,x) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*b*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*b*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*b*>) ^ x is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (z,(All (b,x))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*z*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*z*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*z*>) ^ (All (b,x)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
y is Element of VAR
a is Element of VAR
z is Element of VAR
All (y,a,z,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (a,z,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (z,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*4*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*z*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*z*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
1 + 1 is ext-real positive non negative non empty V8() V9() V10() V14() Element of NAT
(<*4*> ^ <*z*>) ^ H is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (a,(All (z,H))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*a*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*a*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*a*>) ^ (All (z,H)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (y,(All (a,z,H))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*y*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*y*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*y*>) ^ (All (a,z,H)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
b is Element of VAR
s is Element of VAR
H1 is Element of VAR
All (b,s,H1,x) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (s,H1,x) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (H1,x) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*H1*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*H1*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*H1*>) ^ x is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (s,(All (H1,x))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*s*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*s*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*s*>) ^ (All (H1,x)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (b,(All (s,H1,x))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*b*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*b*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*b*>) ^ (All (s,H1,x)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
y is Element of VAR
a is Element of VAR
z is Element of VAR
All (y,a,z,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (a,z,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (z,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*4*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*z*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*z*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
1 + 1 is ext-real positive non negative non empty V8() V9() V10() V14() Element of NAT
(<*4*> ^ <*z*>) ^ H is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (a,(All (z,H))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*a*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*a*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*a*>) ^ (All (z,H)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (y,(All (a,z,H))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*y*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*y*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*y*>) ^ (All (a,z,H)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
b is Element of VAR
s is Element of VAR
All (b,s,x) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (s,x) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*s*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*s*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*s*>) ^ x is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (b,(All (s,x))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*b*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*b*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*b*>) ^ (All (s,x)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (y,a,(All (z,H))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
All (y,(All (a,(All (z,H))))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
(<*4*> ^ <*y*>) ^ (All (a,(All (z,H)))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
y is Element of VAR
a is Element of VAR
Ex (y,a,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
Ex (a,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (a,('not' H)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*4*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*a*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*a*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
1 + 1 is ext-real positive non negative non empty V8() V9() V10() V14() Element of NAT
(<*4*> ^ <*a*>) ^ ('not' H) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' (All (a,('not' H))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (All (a,('not' H))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Ex (y,(Ex (a,H))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' (Ex (a,H)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (Ex (a,H)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (y,('not' (Ex (a,H)))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*y*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*y*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*y*>) ^ ('not' (Ex (a,H))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' (All (y,('not' (Ex (a,H))))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (All (y,('not' (Ex (a,H))))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
z is Element of VAR
b is Element of VAR
Ex (z,b,x) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
Ex (b,x) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ x is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (b,('not' x)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*b*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*b*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*b*>) ^ ('not' x) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' (All (b,('not' x))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (All (b,('not' x))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Ex (z,(Ex (b,x))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' (Ex (b,x)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (Ex (b,x)) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (z,('not' (Ex (b,x)))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*z*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*z*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ <*z*>) ^ ('not' (Ex (b,x))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
'not' (All (z,('not' (Ex (b,x))))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> ^ (All (z,('not' (Ex (b,x))))) is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is Element of VAR
y is Element of VAR
a is Element of VAR
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
Ex (x,y,a,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
Ex (y,a,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
Ex (a,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
'not' H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*2*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
All (a,('not' H)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ZF-formula-like FinSequence of NAT
<*4*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*a*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ <*a*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
1 + 1 is ext-real positive non negative non empty V8() V9() V10() V14()