:: CALCUL_1 semantic presentation

REAL is set

bool REAL is non empty set

bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
K294() is set

{4} is non empty trivial finite V37() 1 -element set

Seg 1 is non empty trivial finite 1 -element Element of bool NAT
{1} is non empty trivial finite V37() 1 -element set
Seg 2 is non empty finite 2 -element Element of bool NAT
{1,2} is non empty finite V37() set

{ } is set
f is non empty set

[:NAT,f:] is Relation-like non empty non trivial non finite set
bool [:NAT,f:] is non empty non trivial non finite set

proj2 f1 is finite set
rng p is finite Element of bool f
bool f is non empty set
F is set

[:NAT,f:] is Relation-like non empty non trivial non finite set

Seg f1 is finite f1 -element Element of bool NAT

[:NAT,f:] is Relation-like non empty non trivial non finite set
bool [:NAT,f:] is non empty non trivial non finite set

Seg y0 is finite y0 -element Element of bool NAT

[:NAT,f:] is Relation-like non empty non trivial non finite set
bool [:NAT,f:] is non empty non trivial non finite set

Seg f1 is finite f1 -element Element of bool NAT

CQC-WFF f is non empty Element of bool ()
QC-WFF f is non empty set
bool () is non empty set

p . (len p) is set
VERUM f is Element of CQC-WFF f

rng p is finite Element of bool ()
bool () is non empty set

p is set

x is set
f . x is set

f . y0 is set

p is set

f . x is set

CQC-WFF f is non empty Element of bool ()
QC-WFF f is non empty set
bool () is non empty set

CQC-WFF f is non empty Element of bool ()
QC-WFF f is non empty set
bool () is non empty set

rng p is finite Element of bool ()
bool () is non empty set

rng x is finite Element of bool ()
f is Element of bool NAT

[:NAT,():] is Relation-like non empty non trivial non finite set
bool [:NAT,():] is non empty non trivial non finite set

rng (x | f) is finite Element of bool ()
proj2 (Seq (x | f)) is finite set
dom (x | f) is finite Element of bool f
bool f is non empty set

(x | f) * (Sgm (dom (x | f))) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite Element of bool [:NAT,():]
rng ((x | f) * (Sgm (dom (x | f)))) is finite Element of bool ()
y0 is set

p . f1 is set
[f1,(p . f1)] is V22() set
{f1,(p . f1)} is non empty finite set
{f1} is non empty trivial finite V37() 1 -element set
{{f1,(p . f1)},{f1}} is non empty finite V37() set
(Seq (x | f)) . f1 is set
dom (Seq (x | f)) is finite Element of bool NAT

CQC-WFF f is non empty Element of bool ()
QC-WFF f is non empty set
bool () is non empty set

(len ((),p)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT

[:NAT,():] is Relation-like non empty non trivial non finite set
bool [:NAT,():] is non empty non trivial non finite set
dom ((),p) is finite Element of bool NAT

(dom p) /\ (Seg f) is finite Element of bool NAT
Seg (len ((),p)) is finite len ((),p) -element Element of bool NAT

(Seg (len p)) /\ (Seg f) is finite Element of bool NAT

CQC-WFF f is non empty Element of bool ()
QC-WFF f is non empty set
bool () is non empty set

(f,p) is Element of CQC-WFF f

rng p is finite Element of bool ()
bool () is non empty set
rng ((),p) is finite Element of bool ()
{(f,p)} is non empty trivial finite 1 -element Element of bool ()
(rng ((),p)) \/ {(f,p)} is non empty finite Element of bool ()

(len ((),p)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT

dom ((),p) is finite Element of bool NAT
Seg (len ((),p)) is finite len ((),p) -element Element of bool NAT

[:NAT,():] is Relation-like non empty non trivial non finite set
bool [:NAT,():] is non empty non trivial non finite set

p . x is set
((),p) . x is set
(((),p) ^ <*(f,p)*>) . x is set
dom <*(f,p)*> is non empty trivial finite 1 -element Element of bool NAT
<*(f,p)*> . 1 is set

(len ((),p)) + (len <*(f,p)*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
len (((),p) ^ <*(f,p)*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
rng <*(f,p)*> is non empty trivial finite 1 -element Element of bool ()
(rng ((),p)) \/ (rng <*(f,p)*>) is non empty finite Element of bool ()

CQC-WFF f is non empty Element of bool ()
QC-WFF f is non empty set
bool () is non empty set

(len ((),p)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT

QC-WFF f is non empty set
CQC-WFF f is non empty Element of bool ()
bool () is non empty set
p is Element of CQC-WFF f

(f,(x ^ <*p*>)) is Element of CQC-WFF f

(x ^ <*p*>) . (len (x ^ <*p*>)) is set
f1 is set

x . F is set
[F,(x . F)] is V22() set
{F,(x . F)} is non empty finite set
{F} is non empty trivial finite V37() 1 -element set
{{F,(x . F)},{F}} is non empty finite V37() set
dom (x ^ <*p*>) is non empty finite Element of bool NAT
(x ^ <*p*>) . F is set

[:NAT,():] is Relation-like non empty non trivial non finite set
bool [:NAT,():] is non empty non trivial non finite set

CQC-WFF f is non empty Element of bool ()
QC-WFF f is non empty set
bool () is non empty set

[:NAT,():] is Relation-like non empty non trivial non finite set
bool [:NAT,():] is non empty non trivial non finite set

CQC-WFF f is non empty Element of bool ()
QC-WFF f is non empty set
bool () is non empty set

[:NAT,():] is Relation-like non empty non trivial non finite set
bool [:NAT,():] is non empty non trivial non finite set

f is set

p is set

((len x) + ()) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT

f is set

dom (p ^ <*f*>) is non empty finite Element of bool NAT

{(p + f)} is non empty trivial finite V37() 1 -element Element of bool NAT
(Seg p) \/ {(p + f)} is non empty finite Element of bool NAT

len (Sgm ((Seg p) \/ {(p + f)})) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT

card ((Seg p) \/ {(p + f)}) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT

Seg (p + f) is finite p + f -element Element of bool NAT

{(p + f)} is non empty trivial finite V37() 1 -element Element of bool NAT
(Seg p) \/ {(p + f)} is non empty finite Element of bool NAT

dom (Sgm ((Seg p) \/ {(p + f)})) is finite Element of bool NAT

Seg (p + 1) is non empty finite p + 1 -element Element of bool NAT
len (Sgm ((Seg p) \/ {(p + f)})) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT

CQC-WFF f is non empty Element of bool ()
QC-WFF f is non empty set
bool () is non empty set

(f,p) is Element of CQC-WFF f

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

(len ((),p)) + ((len x) + 1) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
{((len ((),p)) + ((len x) + 1))} is non empty trivial finite V37() 1 -element Element of bool NAT
(Seg (len ((),p))) \/ {((len ((),p)) + ((len x) + 1))} is non empty finite Element of bool NAT
((((),p) ^ x) ^ <*(f,p)*>) | ((Seg (len ((),p))) \/ {((len ((),p)) + ((len x) + 1))}) is Relation-like NAT -defined (Seg (len ((),p))) \/ {((len ((),p)) + ((len x) + 1))} -defined NAT -defined CQC-WFF f -valued Function-like finite FinSubsequence-like Element of bool [:NAT,():]
[:NAT,():] is Relation-like non empty non trivial non finite set
bool [:NAT,():] is non empty non trivial non finite set
Seq (((((),p) ^ x) ^ <*(f,p)*>) | ((Seg (len ((),p))) \/ {((len ((),p)) + ((len x) + 1))})) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a is set

((len ((),p)) + (len x)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
len ((((),p) ^ x) ^ <*(f,p)*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT

(len (((),p) ^ x)) + (len <*(f,p)*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
((len ((),p)) + (len x)) + (len <*(f,p)*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
dom ((((),p) ^ x) ^ <*(f,p)*>) is non empty finite Element of bool NAT

dom b is Element of bool NAT
(dom ((((),p) ^ x) ^ <*(f,p)*>)) /\ ((Seg (len ((),p))) \/ {((len ((),p)) + ((len x) + 1))}) is finite Element of bool NAT

dom (Sgm (dom b)) is finite Element of bool NAT
(len ((),p)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
Seg ((len ((),p)) + 1) is non empty finite (len ((),p)) + 1 -element Element of bool NAT

a is set
a is set

((len ((),p)) + 1) + (len x) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
a is set
a is set
k is set
[a,k] is V22() set
{a,k} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,k},{a}} is non empty finite V37() set

Seg ((len ((),p)) + ((len x) + 1)) is non empty finite (len ((),p)) + ((len x) + 1) -element Element of bool NAT

(Sgm (Seg (len ((),p)))) ^ (Sgm {((len ((),p)) + ((len x) + 1))}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

(Sgm (Seg (len ((),p)))) ^ <*((len ((),p)) + ((len x) + 1))*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

id (Seg (len ((),p))) is Relation-like Seg (len ((),p)) -defined Seg (len ((),p)) -valued Function-like one-to-one V14( Seg (len ((),p))) finite Element of bool [:(Seg (len ((),p))),(Seg (len ((),p))):]
[:(Seg (len ((),p))),(Seg (len ((),p))):] is Relation-like finite set
bool [:(Seg (len ((),p))),(Seg (len ((),p))):] is non empty finite V37() set
(idseq (len ((),p))) ^ <*((len ((),p)) + ((len x) + 1))*> is Relation-like NAT -defined Function-like non empty finite (len ((),p)) + 1 -element FinSequence-like FinSubsequence-like set
(len ((),p)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT

dom ((),p) is finite Element of bool NAT
dom (idseq (len ((),p))) is finite len ((),p) -element Element of bool NAT
(Sgm (dom b)) . p is set
(idseq (len ((),p))) . p is set

(Seq b) . p is set
b . p is set
b | (Seg (len ((),p))) is Relation-like NAT -defined Seg (len ((),p)) -defined NAT -defined Function-like finite FinSubsequence-like set
(b | (Seg (len ((),p)))) . p is set
((((),p) ^ x) ^ <*(f,p)*>) | (Seg (len ((),p))) is Relation-like NAT -defined Seg (len ((),p)) -defined NAT -defined CQC-WFF f -valued Function-like finite FinSubsequence-like Element of bool [:NAT,():]
(((((),p) ^ x) ^ <*(f,p)*>) | (Seg (len ((),p)))) . p is set
((),p) . p is set

p . p is set
dom (((((),p) ^ x) ^ <*(f,p)*>) | ((Seg (len ((),p))) \/ {((len ((),p)) + ((len x) + 1))})) is finite Element of bool ((Seg (len ((),p))) \/ {((len ((),p)) + ((len x) + 1))})
bool ((Seg (len ((),p))) \/ {((len ((),p)) + ((len x) + 1))}) is non empty finite V37() set
Sgm (dom (((((),p) ^ x) ^ <*(f,p)*>) | ((Seg (len ((),p))) \/ {((len ((),p)) + ((len x) + 1))}))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
rng (Sgm (dom (((((),p) ^ x) ^ <*(f,p)*>) | ((Seg (len ((),p))) \/ {((len ((),p)) + ((len x) + 1))})))) is finite Element of bool NAT
(((((),p) ^ x) ^ <*(f,p)*>) | ((Seg (len ((),p))) \/ {((len ((),p)) + ((len x) + 1))})) * (Sgm (dom (((((),p) ^ x) ^ <*(f,p)*>) | ((Seg (len ((),p))) \/ {((len ((),p)) + ((len x) + 1))})))) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite Element of bool [:NAT,():]
dom ((((((),p) ^ x) ^ <*(f,p)*>) | ((Seg (len ((),p))) \/ {((len ((),p)) + ((len x) + 1))})) * (Sgm (dom (((((),p) ^ x) ^ <*(f,p)*>) | ((Seg (len ((),p))) \/ {((len ((),p)) + ((len x) + 1))}))))) is finite Element of bool NAT
dom (Seq b) is finite Element of bool NAT
dom <*(f,p)*> is non empty trivial finite 1 -element Element of bool NAT

b . ((len ((),p)) + ((len x) + 1)) is set
((((),p) ^ x) ^ <*(f,p)*>) . (((len ((),p)) + (len x)) + 1) is set
<*(f,p)*> . 1 is set
p . (len p) is set
p . a is set

CQC-WFF f is non empty Element of bool ()
QC-WFF f is non empty set
bool () is non empty set
p is set
x is set

dom <*p,x*> is non empty finite 2 -element Element of bool NAT

(f ^ <*p,x*>) . ((len f) + 1) is set

(f ^ <*p,x*>) . ((len f) + 2) is set

<*p,x*> . 2 is set
<*p,x*> . 1 is set

CQC-WFF f is non empty Element of bool ()
QC-WFF f is non empty set
bool () is non empty set
bound_QC-variables f is non empty Element of bool ()
QC-variables f is non empty set
bool () is non empty set
bool is non empty set

x is set
f is set
f is set

F is Element of CQC-WFF f
p . f1 is set
y0 is set

x is Element of bool
f is Element of bool
y0 is set

F is Element of CQC-WFF f
p . f1 is set

F is Element of CQC-WFF f
p . f1 is set

CQC-WFF f is non empty Element of bool ()
QC-WFF f is non empty set
bool () is non empty set
[:NAT,():] is Relation-like REAL -defined QC-WFF f -valued non empty non trivial non finite Element of bool [:REAL,():]

bool [:REAL,():] is non empty set
bool [:NAT,():] is non empty non trivial non finite set
p is set
x is set
f is set
p is set
x is set
f is set

(f) is set

p . x is set
(p . x) `2 is set
CQC-WFF f is non empty Element of bool ()
QC-WFF f is non empty set
bool () is non empty set
(p . x) `1 is set
VERUM f is Element of CQC-WFF f

QC-variables f is non empty set
bound_QC-variables f is non empty Element of bool ()
bool () is non empty set

(f,f) is Element of CQC-WFF f

(f,f1) is Element of CQC-WFF f

(f,b) is Element of CQC-WFF f
(f,a) is Element of CQC-WFF f
p . F is set
(p . F) `1 is set

(f,a) is Element of CQC-WFF f

(f,((),x)) is Element of CQC-WFF f
'not' (f,((),x)) is Element of CQC-WFF f
(f,((),y)) is Element of CQC-WFF f
(f,x) is Element of CQC-WFF f
(f,y) is Element of CQC-WFF f
p . p is set
(p . p) `1 is set
p . k is set
(p . k) `1 is set

(f,c15) is Element of CQC-WFF f

(f,((),c18)) is Element of CQC-WFF f
c20 is Element of CQC-WFF f
'not' c20 is Element of CQC-WFF f
(f,c18) is Element of CQC-WFF f
'not' (f,c18) is Element of CQC-WFF f
(f,c19) is Element of CQC-WFF f
p . c17 is set
(p . c17) `1 is set
p . c16 is set
(p . c16) `1 is set

(f,c21) is Element of CQC-WFF f

p . c23 is set
(p . c23) `1 is set
p . c22 is set
(p . c22) `1 is set
(f,c24) is Element of CQC-WFF f
(f,c25) is Element of CQC-WFF f
(f,c24) '&' (f,c25) is Element of CQC-WFF f

((),c24) ^ <*((f,c24) '&' (f,c25))*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f

(f,c26) is Element of CQC-WFF f

c29 is Element of CQC-WFF f
c30 is Element of CQC-WFF f
c29 '&' c30 is Element of CQC-WFF f

(f,c28) is Element of CQC-WFF f
p . c27 is set
(p . c27) `1 is set

(f,c31) is Element of CQC-WFF f

c34 is Element of CQC-WFF f
c35 is Element of CQC-WFF f
c34 '&' c35 is Element of CQC-WFF f

(f,c33) is Element of CQC-WFF f
p . c32 is set
(p . c32) `1 is set

(f,c36) is Element of CQC-WFF f

(f,c38) is Element of CQC-WFF f
c40 is Element of bound_QC-variables f
c39 is Element of CQC-WFF f
All (c40,c39) is Element of CQC-WFF f
p . c37 is set
(p . c37) `1 is set

c41 is Element of bound_QC-variables f
c39 . (c40,c41) is Element of CQC-WFF f

((),c38) ^ <*(c39 . (c40,c41))*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f

(f,c42) is Element of CQC-WFF f

(f,c44) is Element of CQC-WFF f
c45 is Element of CQC-WFF f
c46 is Element of bound_QC-variables f
c47 is Element of bound_QC-variables f
c45 . (c46,c47) is Element of CQC-WFF f

(f,((),c44)) is Element of bool
bool is non empty set
All (c46,c45) is Element of CQC-WFF f
still_not-bound_in (All (c46,c45)) is Element of bool
p . c43 is set
(p . c43) `1 is set

(f,c50) is Element of CQC-WFF f
(f,c51) is Element of CQC-WFF f
p . c49 is set
(p . c49) `1 is set

(f,((),c55)) is Element of CQC-WFF f
'not' (f,((),c55)) is Element of CQC-WFF f
(f,((),c56)) is Element of CQC-WFF f
(f,c55) is Element of CQC-WFF f
(f,c56) is Element of CQC-WFF f
p . c54 is set
(p . c54) `1 is set
p . c53 is set
(p . c53) `1 is set

(f,((),c60)) is Element of CQC-WFF f
c62 is Element of CQC-WFF f
'not' c62 is Element of CQC-WFF f
(f,c60) is Element of CQC-WFF f
'not' (f,c60) is Element of CQC-WFF f
(f,c61) is Element of CQC-WFF f
p . c59 is set
(p . c59) `1 is set
p . c58 is set
(p . c58) `1 is set

p . c65 is set
(p . c65) `1 is set
p . c64 is set
(p . c64) `1 is set
(f,c66) is Element of CQC-WFF f
(f,c67) is Element of CQC-WFF f
(f,c66) '&' (f,c67) is Element of CQC-WFF f

((),c66) ^ <*((f,c66) '&' (f,c67))*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f

c71 is Element of CQC-WFF f
c72 is Element of CQC-WFF f
c71 '&' c72 is Element of CQC-WFF f

(f,c70) is Element of CQC-WFF f
p . c69 is set
(p . c69) `1 is set

c76 is Element of CQC-WFF f
c77 is Element of CQC-WFF f
c76 '&' c77 is Element of CQC-WFF f

(f,c75) is Element of CQC-WFF f
p . c74 is set
(p . c74) `1 is set

(f,c80) is Element of CQC-WFF f
c82 is Element of bound_QC-variables f
c81 is Element of CQC-WFF f
All (c82,c81) is Element of CQC-WFF f
p . c79 is set
(p . c79) `1 is set

c83 is Element of bound_QC-variables f
c81 . (c82,c83) is Element of CQC-WFF f

((),c80) ^ <*(c81 . (c82,c83))*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f