:: CALCUL_2 semantic presentation

REAL is set

K19(REAL) is set

K19(omega) is non finite set
K19(NAT) is non finite set
K283() is set
{} is set

Seg 1 is non empty V12() finite 1 -element Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b1 & b1 <= p + Al ) } is set

(Al,p) is set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b1 & b1 <= p + Al ) } is set
n is set

(p,q) is Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + p <= b1 & b1 <= q + p ) } is set

(Al,0) is Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b1 & b1 <= 0 + Al ) } is set
the Element of (Al,0) is Element of (Al,0)

(p,Al) is Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + p <= b1 & b1 <= Al + p ) } is set

(q,Al) is Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + q <= b1 & b1 <= Al + q ) } is set
(q,p) is Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + q <= b1 & b1 <= p + q ) } is set
n is set

(Al,p) is Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b1 & b1 <= p + Al ) } is set

{((Al + p) + 1)} is non empty V12() 1 -element set
(Al,p) \/ {((Al + p) + 1)} is set

(Al,(p + 1)) is Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b1 & b1 <= (p + 1) + Al ) } is set

q is set

q is set

(Al,p) is Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b1 & b1 <= p + Al ) } is set

(Al,q) is Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b1 & b1 <= q + Al ) } is set

(Al,(q + 1)) is Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b1 & b1 <= (q + 1) + Al ) } is set

{q} is non empty V12() 1 -element set
q \/ {q} is set

{(n + 1)} is non empty V12() 1 -element set
f is set
f is set
(Al,q) \/ {(n + 1)} is set
(Al,0) is Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b1 & b1 <= 0 + Al ) } is set

(Al,p) is Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b1 & b1 <= p + Al ) } is set

CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set

(Al,p) is finite Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b1 & b1 <= p + Al ) } is set

Seg (Al + p) is finite Al + p -element Element of K19(NAT)
q is set

Seg Al is finite Al -element Element of K19(NAT)

(Al,p) is finite Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b1 & b1 <= p + Al ) } is set
q is set

dom (Al ^ p) is Element of K19(NAT)
dom Al is Element of K19(NAT)

((len Al),(len p)) is finite Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + (len Al) <= b1 & b1 <= (len p) + (len Al) ) } is set
(dom Al) \/ ((len Al),(len p)) is Element of K19(NAT)
q is set

q is set

CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set

((len p),(len q)) is finite Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + (len p) <= b1 & b1 <= (len q) + (len p) ) } is set

Seg ((len p) + (len q)) is finite (len p) + (len q) -element Element of K19(NAT)

CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set

((len p),(len q)) is finite Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + (len p) <= b1 & b1 <= (len q) + (len p) ) } is set

dom (Sgm ((len p),(len q))) is Element of K19(NAT)
dom q is Element of K19(NAT)

CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set

((len p),(len q)) is finite Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + (len p) <= b1 & b1 <= (len q) + (len p) ) } is set

rng (Sgm ((len p),(len q))) is Element of K19(NAT)

Seg ((len p) + (len q)) is finite (len p) + (len q) -element Element of K19(NAT)

CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set

((len q),(len n)) is finite Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + (len q) <= b1 & b1 <= (len n) + (len q) ) } is set

dom (Sgm ((len q),(len n))) is Element of K19(NAT)
(Sgm ((len q),(len n))) . p is set
dom n is Element of K19(NAT)

(Sgm ((len q),(len n))) . g is set

rng (Sgm ((len q),(len n))) is Element of K19(NAT)
(len q) + (f + 1) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT

(Sgm ((len q),(len n))) . f is set

Seg ((len q) + (len n)) is finite (len q) + (len n) -element Element of K19(NAT)

((len q) + f) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT

(1 + (len q)) + f is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT

(Sgm ((len q),(len n))) . F is set

(Sgm ((len q),(len n))) . f is set

CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set

((len p),(len q)) is finite Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + (len p) <= b1 & b1 <= (len q) + (len p) ) } is set

dom (p ^ q) is Element of K19(NAT)
n is set

CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set

((len p),(len q)) is finite Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + (len p) <= b1 & b1 <= (len q) + (len p) ) } is set
(p ^ q) | ((len p),(len q)) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
K20(NAT,(CQC-WFF Al)) is non finite set
K19(K20(NAT,(CQC-WFF Al))) is non finite set
dom ((p ^ q) | ((len p),(len q))) is Element of K19(NAT)
dom (p ^ q) is Element of K19(NAT)
(dom (p ^ q)) /\ ((len p),(len q)) is Element of K19(NAT)

CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set

((len p),(len q)) is finite Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + (len p) <= b1 & b1 <= (len q) + (len p) ) } is set
(p ^ q) | ((len p),(len q)) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
K20(NAT,(CQC-WFF Al)) is non finite set
K19(K20(NAT,(CQC-WFF Al))) is non finite set
Seq ((p ^ q) | ((len p),(len q))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(Sgm ((len p),(len q))) * (p ^ q) is Relation-like NAT -defined CQC-WFF Al -valued Function-like Element of K19(K20(NAT,(CQC-WFF Al)))

dom n is Element of K19(NAT)

(Sgm (dom n)) * n is Relation-like Function-like set
(Sgm ((len p),(len q))) * n is Relation-like Function-like set
rng (Sgm ((len p),(len q))) is Element of K19(NAT)
(p ^ q) | (rng (Sgm ((len p),(len q)))) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
(Sgm ((len p),(len q))) * ((p ^ q) | (rng (Sgm ((len p),(len q))))) is Relation-like Function-like set
(Sgm ((len p),(len q))) * (p ^ q) is Relation-like Function-like set

CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set

((len p),(len q)) is finite Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + (len p) <= b1 & b1 <= (len q) + (len p) ) } is set
(p ^ q) | ((len p),(len q)) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
K20(NAT,(CQC-WFF Al)) is non finite set
K19(K20(NAT,(CQC-WFF Al))) is non finite set
Seq ((p ^ q) | ((len p),(len q))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (Seq ((p ^ q) | ((len p),(len q)))) is Element of K19(NAT)
dom q is Element of K19(NAT)

rng (Sgm ((len p),(len q))) is Element of K19(NAT)
dom (p ^ q) is Element of K19(NAT)
(Sgm ((len p),(len q))) * (p ^ q) is Relation-like NAT -defined CQC-WFF Al -valued Function-like Element of K19(K20(NAT,(CQC-WFF Al)))
dom ((Sgm ((len p),(len q))) * (p ^ q)) is Element of K19(NAT)
dom (Sgm ((len p),(len q))) is Element of K19(NAT)

CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set

((len q),(len p)) is finite Element of K19(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + (len q) <= b1 & b1 <= (len p) + (len q) ) } is set
(q ^ p) | ((len q),(len p)) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
K20(NAT,(CQC-WFF Al)) is non finite set
K19(K20(NAT,(CQC-WFF Al))) is non finite set
Seq ((q ^ p) | ((len q),(len p))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (Seq ((q ^ p) | ((len q),(len p)))) is Element of K19(NAT)

(Seq ((q ^ p) | ((len q),(len p)))) . n is set
p . n is set
dom p is Element of K19(NAT)

dom (Sgm ((len q),(len p))) is Element of K19(NAT)
(Sgm ((len q),(len p))) * (q ^ p) is Relation-like NAT -defined CQC-WFF Al -valued Function-like Element of K19(K20(NAT,(CQC-WFF Al)))
((Sgm ((len q),(len p))) * (q ^ p)) . n is set
(Sgm ((len q),(len p))) . n is set
(q ^ p) . ((Sgm ((len q),(len p))) . n) is set

(q ^ p) . ((len q) + n) is set
dom p is Element of K19(NAT)
Al is non empty set

dom p is Element of K19(NAT)
K20((dom p),(dom p)) is set
K19(K20((dom p),(dom p))) is set

q * p is Relation-like dom p -defined Al -valued Function-like Element of K19(K20((dom p),Al))
K20((dom p),Al) is set
K19(K20((dom p),Al)) is set
rng q is Element of K19((dom p))
K19((dom p)) is set
dom (q * p) is Element of K19((dom p))
dom q is Element of K19((dom p))

Seg f is finite f -element Element of K19(NAT)

rng n is set
rng p is Element of K19(Al)
K19(Al) is set

CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set

dom p is Element of K19(NAT)
K20((dom p),(dom p)) is set
K19(K20((dom p),(dom p))) is set

q * p is Relation-like dom p -defined CQC-WFF Al -valued Function-like Element of K19(K20((dom p),(CQC-WFF Al)))
K20((dom p),(CQC-WFF Al)) is set
K19(K20((dom p),(CQC-WFF Al))) is set
dom ((CQC-WFF Al),p,q) is Element of K19(NAT)
rng q is Element of K19((dom p))
K19((dom p)) is set
dom (q * p) is Element of K19((dom p))
dom q is Element of K19((dom p))

QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
K19((QC-WFF Al)) is set
p is Element of CQC-WFF Al

Suc (q ^ <*p*>) is Element of CQC-WFF Al
Suc ((n ^ q) ^ <*p*>) is Element of CQC-WFF Al

CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set

p . 1 is set
VERUM Al is Element of CQC-WFF Al
dom p is Element of K19(NAT)
q is Element of CQC-WFF Al
q is Element of CQC-WFF Al
n is Element of CQC-WFF Al
f is Element of CQC-WFF Al
g is Element of CQC-WFF Al

CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set

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

p . (q + 1) is set
dom p is Element of K19(NAT)
f is Element of CQC-WFF Al
n is Element of CQC-WFF Al
n => f is Element of CQC-WFF Al

q . 1 is set
dom q is Element of K19(NAT)
q . (len p) is set
n is Element of CQC-WFF Al
q is Element of CQC-WFF Al
n is Element of CQC-WFF Al

f . (len p) is set

f . 1 is set

f . (len p) is set

f . 1 is set

g . (len p) is set

g . 1 is set

g . (len p) is set

g . 1 is set

p1 is Element of CQC-WFF Al

p . (h + 1) is set
p1 is Element of CQC-WFF Al
F is Element of CQC-WFF Al
H is Element of CQC-WFF Al
p1 => p1 is Element of CQC-WFF Al
pk is Element of CQC-WFF Al
p1 is Element of CQC-WFF Al
p1 is Element of CQC-WFF Al
pk => p1 is Element of CQC-WFF Al

QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
K19((QC-WFF Al)) is set
p is Element of CQC-WFF Al

dom (q ^ <*p*>) is Element of K19(NAT)

(q ^ <*p*>) . ((len q) + 1) is set
Suc ((q ^ <*p*>) ^ <*p*>) is Element of CQC-WFF Al

QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
K19((QC-WFF Al)) is set
p is Element of CQC-WFF Al

q is Element of CQC-WFF Al
p '&' q is Element of CQC-WFF Al

Suc (n ^ <*(p '&' q)*>) is Element of CQC-WFF Al

QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
K19((QC-WFF Al)) is set
p is Element of CQC-WFF Al
q is Element of CQC-WFF Al
p '&' q is Element of CQC-WFF Al

Suc (n ^ <*(p '&' q)*>) is Element of CQC-WFF Al

QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
K19((QC-WFF Al)) is set
p is Element of CQC-WFF Al

q is Element of CQC-WFF Al

QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
K19((QC-WFF Al)) is set
p is Element of CQC-WFF Al

'not' p is Element of CQC-WFF Al

q is Element of CQC-WFF Al

Suc (n ^ <*p*>) is Element of CQC-WFF Al

QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
K19((QC-WFF Al)) is set
p is Element of CQC-WFF Al

'not' p is Element of CQC-WFF Al

q is Element of CQC-WFF Al

Suc (Ant ((n ^ <*p*>) ^ <*q*>)) is Element of CQC-WFF Al
'not' (Suc (Ant ((n ^ <*p*>) ^ <*q*>))) is Element of CQC-WFF Al
Suc (Ant ((n ^ <*()*>) ^ <*q*>)) is Element of CQC-WFF Al

len ((n ^ <*()*>) ^ <*q*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
Suc ((n ^ <*p*>) ^ <*q*>) is Element of CQC-WFF Al
Suc ((n ^ <*()*>) ^ <*q*>) is Element of CQC-WFF Al

QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
K19((QC-WFF Al)) is set
p is Element of CQC-WFF Al

q is Element of CQC-WFF Al

p => q is Element of CQC-WFF Al

'not' q is Element of CQC-WFF Al
p '&' () is Element of CQC-WFF Al

Suc ((n ^ <*p*>) ^ <*q*>) is Element of CQC-WFF Al
Suc (((n ^ <*(p '&' ())*>) ^ <*p*>) ^ <*q*>) is Element of CQC-WFF Al

Suc (Ant ((n ^ <*p*>) ^ <*q*>)) is Element of CQC-WFF Al

'not' (p '&' ()) is Element of CQC-WFF Al

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

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

CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set

(Al,(Rev p)) is Element of CQC-WFF Al

(Al,(Rev p)) is Element of CQC-WFF Al

f . (len (Rev p)) is set

f . 1 is set

f . g is set

f . (g + 1) is set

dom f is Element of K19(NAT)

Seg F is finite F -element Element of K19(NAT)
(q ^ p) | (Seg F) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
K20(NAT,(CQC-WFF Al)) is non finite set
K19(K20(NAT,(CQC-WFF Al))) is non finite set

H is Element of CQC-WFF Al

(len (q ^ p)) - g is ext-real V25() V26() V33() set
((len (q ^ p)) + g) - g is ext-real V25() V26() V33() set

Seg q1 is finite q1 -element Element of K19(NAT)
(q ^ p) | (Seg q1) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))

Seg q1 is finite q1 -element Element of K19(NAT)
(q ^ p) | (Seg q1) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))

Seg q1 is finite q1 -element Element of K19(NAT)
(q ^ p) | (Seg q1) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))

Seg q1 is finite q1 -element Element of K19(NAT)
(q ^ p) | (Seg q1) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))

dom (q ^ p) is Element of K19(NAT)
(q ^ p) . q1 is set

(p1 ^ <*((q ^ p) . q1)*>) ^ <*(f . g)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
(Rev p) . (g + 1) is set
q1 is Element of CQC-WFF Al
g1 is Element of CQC-WFF Al
q1 => g1 is Element of CQC-WFF Al
dom (Rev p) is Element of K19(NAT)
dom p is Element of K19(NAT)
(len p) - (g + 1) is ext-real V25() V26() V33() set
((len p) - (g + 1)) + 1 is