:: REWRITE2 semantic presentation

REAL is set

K6(REAL) is set

K6(NAT) is set
K6(NAT) is set

{0,1} is non empty Element of K6(NAT)
{0,1} ^omega is non empty functional set
K6(()) is set

K6(([#] (NAT,REAL))) is set
K346() is set

Seg 1 is non empty finite V39(1) Element of K6(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty set
Seg 2 is non empty finite V39(2) Element of K6(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty set

dom S is Element of K6(NAT)

Seg E is finite V39(E) Element of K6(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT : ( 1 <= b1 & b1 <= E ) } is set

dom (s | E) is Element of K6(NAT)
dom s is non empty Element of K6(NAT)

(s | E) . t is set
s . t is set
(s | E) . (t + 1) is set
s . (t + 1) is set
[((s | E) . t),((s | E) . (t + 1))] is set
{((s | E) . t),((s | E) . (t + 1))} is non empty set
{((s | E) . t)} is non empty set
{{((s | E) . t),((s | E) . (t + 1))},{((s | E) . t)}} is non empty set

dom s is non empty Element of K6(NAT)
s . 1 is set
s . E is set

Seg E is finite V39(E) Element of K6(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT : ( 1 <= b1 & b1 <= E ) } is set

(s | E) . 1 is set
(s | E) . (len (s | E)) is set

S is set
dom E is set
E . S is set

[1,E] is set
{1,E} is non empty set
{{1,E},{1}} is non empty set
{[1,E]} is non empty Relation-like Function-like set
S is set
dom <*E*> is non empty set
<*E*> . S is set
dom <*E*> is non empty Element of K6(NAT)
{1} is non empty Element of K6(NAT)

S is set
E . S is set
dom E is set
dom E is set
dom E is set

S is set

dom E is set
dom E is set
dom E is set
E is set
E ^omega is non empty functional set

s is set
dom S is set

dom S is Element of K6(NAT)

s is set
dom (E ^ S) is Element of K6(NAT)

dom E is Element of K6(NAT)

(E ^ S) . t is set
(E ^ S) . s is set
dom S is Element of K6(NAT)

(E ^ S) . ((len E) + w) is set

(E ^ S) . s is set

dom E is Element of K6(NAT)
dom S is Element of K6(NAT)

dom S is set

s is set

t is set

dom s is set
t is set
s . t is set

dom t is set
w is set

dom s is set

dom t is set
w is set

s is set

t is set

dom s is set
t is set
s . t is set

dom t is set
w is set

dom s is set

dom t is set
w is set

(E,S) is Relation-like Function-like () set
dom S is Element of K6(NAT)

Seg s is finite V39(s) Element of K6(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT : ( 1 <= b1 & b1 <= s ) } is set
dom (E,S) is set
(E,S) is Relation-like Function-like () set
dom S is Element of K6(NAT)

Seg s is finite V39(s) Element of K6(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT : ( 1 <= b1 & b1 <= s ) } is set
dom (E,S) is set

dom (E,S) is Element of K6(NAT)
dom S is Element of K6(NAT)
dom (E,S) is Element of K6(NAT)
E is set

K237(E) is non empty functional M11(E)

dom S is Element of K6(NAT)

dom ((<%> E),S) is Element of K6(NAT)

dom ((<%> E),S) is Element of K6(NAT)

dom (E,(S,s)) is Element of K6(NAT)
dom (S,s) is Element of K6(NAT)
dom s is Element of K6(NAT)

dom ((E ^ S),s) is Element of K6(NAT)

dom (E,(S,s)) is Element of K6(NAT)
dom (S,s) is Element of K6(NAT)

dom ((S ^ E),s) is Element of K6(NAT)

dom (E,(S,s)) is Element of K6(NAT)
dom (S,s) is Element of K6(NAT)
dom s is Element of K6(NAT)
dom (E,s) is Element of K6(NAT)

dom (S,(E,s)) is Element of K6(NAT)

dom (E,(S ^ s)) is Element of K6(NAT)
dom (S ^ s) is Element of K6(NAT)
dom S is Element of K6(NAT)
dom (E,S) is Element of K6(NAT)

((E,S) ^ (E,s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set
dom S is Element of K6(NAT)

dom s is Element of K6(NAT)
dom (E,s) is Element of K6(NAT)

(S ^ s) . ((len S) + w) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set
E ^ ((S ^ s) . ((len S) + w)) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

((E,S) ^ (E,s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set
dom S is Element of K6(NAT)

((E,S) ^ (E,s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

((E,S) ^ (E,s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set
len (E,(S ^ s)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

(len (E,S)) + (len s) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

(len (E,S)) + (len (E,s)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT
len ((E,S) ^ (E,s)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT
dom ((E,S) ^ (E,s)) is Element of K6(NAT)

dom (E,(S ^ s)) is Element of K6(NAT)
dom S is Element of K6(NAT)
dom (E,S) is Element of K6(NAT)

((E,S) ^ (E,s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set
dom S is Element of K6(NAT)

dom s is Element of K6(NAT)
dom (E,s) is Element of K6(NAT)

(S ^ s) . ((len S) + w) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set
((S ^ s) . ((len S) + w)) ^ E is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

((E,S) ^ (E,s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set
dom S is Element of K6(NAT)

((E,S) ^ (E,s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

((E,S) ^ (E,s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set
len (E,(S ^ s)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

(len (E,S)) + (len s) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

(len (E,S)) + (len (E,s)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT
len ((E,S) ^ (E,s)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT
dom ((E,S) ^ (E,s)) is Element of K6(NAT)
E is set
E ^omega is non empty functional set

dom S is Element of K6(NAT)
dom S is Element of K6(NAT)
dom S is Element of K6(NAT)
E is set
E ^omega is non empty functional set

dom (S,s) is Element of K6(NAT)
dom s is Element of K6(NAT)

K237(E) is non empty functional M11(E)

dom (S,s) is Element of K6(NAT)
dom s is Element of K6(NAT)

K237(E) is non empty functional M11(E)

E \/ (E ~) is Relation-like set
(E ~) ~ is Relation-like set
((E ~) ~) \/ (E ~) is Relation-like set
(((E ~) ~) \/ (E ~)) ~ is Relation-like set
(E \/ (E ~)) ~ is Relation-like set
E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
the Relation-like Element of K6(([#] ((),()))) is Relation-like Element of K6(([#] ((),())))
the Relation-like Element of K6(([#] ((),()))) ~ is Relation-like Element of K6(([#] ((),())))
the Relation-like Element of K6(([#] ((),()))) \/ ( the Relation-like Element of K6(([#] ((),()))) ~) is Relation-like symmetric Element of K6(([#] ((),())))
E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))

K237(E) is non empty functional M11(E)

E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))

K237(E) is non empty functional M11(E)

E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))

K237(E) is non empty functional M11(E)

(w ^ (x ^ u)) ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

((w ^ x) ^ u) ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(w ^ (x ^ t)) ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

((w ^ x) ^ t) ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(x ^ t) ^ (u ^ w) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)
(x ^ u) ^ (u ^ w) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)
E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))

K237(E) is non empty functional M11(E)

E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))

K237(E) is non empty functional M11(E)

E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))

K237(E) is non empty functional M11(E)

E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))

S ~ is Relation-like Element of K6(([#] ((),())))
[s,t] is Element of [#] ((),())
{s,t} is non empty functional set
{s} is non empty functional set
{{s,t},{s}} is non empty set
[t,s] is Element of [#] ((),())
{t,s} is non empty functional set
{t} is non empty functional set
{{t,s},{t}} is non empty set
E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))

K237(E) is non empty functional M11(E)

E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))
s is Relation-like Element of K6(([#] ((),())))

[t,w] is Element of [#] ((),())
{t,w} is non empty functional set
{t} is non empty functional set
{{t,w},{t}} is non empty set
E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))
s is Relation-like Element of K6(([#] ((),())))

K237(E) is non empty functional M11(E)

E is set
E ^omega is non empty functional set
{} ((),()) is Relation-like Element of K6(([#] ((),())))
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set

K237(E) is non empty functional M11(E)

[x,u] is Element of [#] ((),())
{x,u} is non empty functional set
{x} is non empty functional set
{{x,u},{x}} is non empty set
E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))
s is Relation-like Element of K6(([#] ((),())))
S \/ s is Relation-like Element of K6(([#] ((),())))

K237(E) is non empty functional M11(E)

[t,u] is Element of [#] ((),())
{t,u} is non empty functional set
{t} is non empty functional set
{{t,u},{t}} is non empty set
E is set

[#] (E,E) is Relation-like set
K6(([#] (E,E))) is set
E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))
s is Relation-like Element of K6(([#] ((),())))

[t,w] is Element of [#] ((),())
{t,w} is non empty functional set
{t} is non empty functional set
{{t,w},{t}} is non empty set

[x,u] is Element of [#] ((),())
{x,u} is non empty functional set
{x} is non empty functional set
{{x,u},{x}} is non empty set
s is Relation-like Element of K6(([#] ((),())))
t is Relation-like Element of K6(([#] ((),())))

[w,x] is Element of [#] ((),())
{w,x} is non empty functional set
{w} is non empty functional set
{{w,x},{w}} is non empty set
E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))
(E,S) is Relation-like Element of K6(([#] ((),())))
s is set
t is set
w is set
[t,w] is set
{t,w} is non empty set
{t} is non empty set
{{t,w},{t}} is non empty set

E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))
(E,S) is Relation-like Element of K6(([#] ((),())))

dom (E,s,t) is Element of K6(NAT)

dom t is Element of K6(NAT)
(E,(E,s,t),(w + 1)) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega
(E,t,(w + 1)) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega
(E,t,(w + 1)) ^ s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)
K237(E) is non empty functional M11(E)

[(E,t,w),(E,t,(w + 1))] is Element of [#] ((),())
{(E,t,w),(E,t,(w + 1))} is non empty functional set
{(E,t,w)} is non empty functional set
{{(E,t,w),(E,t,(w + 1))},{(E,t,w)}} is non empty set

(E,(E,s,t),w) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega
[(E,(E,s,t),w),(E,(E,s,t),(w + 1))] is Element of [#] ((),())
{(E,(E,s,t),w),(E,(E,s,t),(w + 1))} is non empty functional set
{(E,(E,s,t),w)} is non empty functional set
{{(E,(E,s,t),w),(E,(E,s,t),(w + 1))},{(E,(E,s,t),w)}} is non empty set

dom (E,s,t) is Element of K6(NAT)

(E,(E,s,t),(w + 1)) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega
(E,t,(w + 1)) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega
s ^ (E,t,(w + 1)) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

[(E,t,w),(E,t,(w + 1))] is Element of [#] ((),())
{(E,t,w),(E,t,(w + 1))} is non empty functional set
{(E,t,w)} is non empty functional set
{{(E,t,w),(E,t,(w + 1))},{(E,t,w)}} is non empty set

(E,(E,s,t),w) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega
[(E,(E,s,t),w),(E,(E,s,t),(w + 1))] is Element of [#] ((),())
{(E,(E,s,t),w),(E,(E,s,t),(w + 1))} is non empty functional set
{(E,(E,s,t),w)} is non empty functional set
{{(E,(E,s,t),w),(E,(E,s,t),(w + 1))},{(E,(E,s,t),w)}} is non empty set

E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))
(E,S) is Relation-like Element of K6(([#] ((),())))

E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))
(E,S) is Relation-like Element of K6(([#] ((),())))
(E,S) ~ is Relation-like Element of K6(([#] ((),())))
s is set
t is set
w is set
[t,w] is set
{t,w} is non empty set
{t} is non empty set
{{t,w},{t}} is non empty set

[u,x] is Element of [#] ((),())
{u,x} is non empty functional set
{u} is non empty functional set
{{u,x},{u}} is non empty set
t is set
w is set
[t,w] is set
{t,w} is non empty set
{t} is non empty set
{{t,w},{t}} is non empty set

[u,x] is Element of [#] ((),())
{u,x} is non empty functional set
{u} is non empty functional set
{{u,x},{u}} is non empty set
E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))
(E,S) is Relation-like Element of K6(([#] ((),())))
s is Relation-like Element of K6(([#] ((),())))
(E,s) is Relation-like Element of K6(([#] ((),())))
t is set
w is set
x is set
[w,x] is set
{w,x} is non empty set
{w} is non empty set
{{w,x},{w}} is non empty set

E is set
E ^omega is non empty functional set
(()) is Relation-like E ^omega -defined E ^omega -valued Function-like one-to-one Element of K6(([#] ((),())))
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
(E,(())) is Relation-like Element of K6(([#] ((),())))
S is set
s is set
t is set
[s,t] is set
{s,t} is non empty set
{s} is non empty set
{{s,t},{s}} is non empty set

K237(E) is non empty functional M11(E)

[u,u] is Element of [#] ((),())
{u,u} is non empty functional set
{u} is non empty functional set
{{u,u},{u}} is non empty set
E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
(()) is Relation-like E ^omega -defined E ^omega -valued Function-like one-to-one Element of K6(([#] ((),())))
S is Relation-like Element of K6(([#] ((),())))
S \/ (()) is Relation-like Element of K6(([#] ((),())))
(E,(S \/ (()))) is Relation-like Element of K6(([#] ((),())))
(E,S) is Relation-like Element of K6(([#] ((),())))
(E,S) \/ (()) is Relation-like Element of K6(([#] ((),())))
s is set
t is set
w is set
[t,w] is set
{t,w} is non empty set
{t} is non empty set
{{t,w},{t}} is non empty set

K237(E) is non empty functional M11(E)

[u,w] is Element of [#] ((),())
{u,w} is non empty functional set
{u} is non empty functional set
{{u,w},{u}} is non empty set
s is set
(E,(())) is Relation-like Element of K6(([#] ((),())))
E is set
E ^omega is non empty functional set
{} ((),()) is Relation-like Element of K6(([#] ((),())))
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
(E,({} ((),()))) is Relation-like Element of K6(([#] ((),())))
S is set
s is set
t is set
[s,t] is set
{s,t} is non empty set
{s} is non empty set
{{s,t},{s}} is non empty set

E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))
(E,S) is Relation-like Element of K6(([#] ((),())))

K237(E) is non empty functional M11(E)

[u,t] is Element of [#] ((),())
{u,t} is non empty functional set
{u} is non empty functional set
{{u,t},{u}} is non empty set
E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))
(E,S) is Relation-like Element of K6(([#] ((),())))
(E,(E,S)) is Relation-like Element of K6(([#] ((),())))
s is set
t is set
w is set
[t,w] is set
{t,w} is non empty set
{t} is non empty set
{{t,w},{t}} is non empty set

E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))

(E,S) is Relation-like Element of K6(([#] ((),())))
E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))

[s,t] is Element of [#] ((),())
{s,t} is non empty functional set
{s} is non empty functional set
{{s,t},{s}} is non empty set
(E,S) is Relation-like Element of K6(([#] ((),())))
E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))

E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))

(E,S) is Relation-like Element of K6(([#] ((),())))
E is set
E ^omega is non empty functional set
[#] ((),()) is Relation-like set
K6(([#] ((),()))) is set
S is Relation-like Element of K6(([#] ((),())))

K237(E) is non empty functional M11(E)

(E,S) is Relation-like Element of K6(([#] ((),())))

x . 1 is set

x . (len x) is set

dom u is Element of K6(NAT)

(E,(E,w,u),1) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

(E,(E,w,u),(len (E,w,u))) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

(E,(E</