:: COMPOS_1 semantic presentation

REAL is non empty non trivial V5() non finite V71() V72() V73() V77() set

NAT is non empty non trivial V5() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal limit_cardinal countable denumerable V71() V72() V73() V74() V75() V76() V77() Element of bool REAL

bool REAL is non empty non trivial V5() non finite set

omega is non empty non trivial V5() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal limit_cardinal countable denumerable V71() V72() V73() V74() V75() V76() V77() set

bool omega is non empty non trivial V5() non finite set

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

COMPLEX is non empty non trivial V5() non finite V71() V77() set

RAT is non empty non trivial V5() non finite V71() V72() V73() V74() V77() set

INT is non empty non trivial V5() non finite V71() V72() V73() V74() V75() V77() set

{} is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V47() Cardinal-yielding countable V57() V58() integer complex-valued ext-real-valued real-valued natural-valued V65() decreasing non-decreasing non-increasing V71() V72() V73() V74() V75() V76() V77() V92() V93() V96() initial set

the empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V47() Cardinal-yielding countable V57() V58() integer complex-valued ext-real-valued real-valued natural-valued V65() decreasing non-decreasing non-increasing V71() V72() V73() V74() V75() V76() V77() V92() V93() V96() initial set is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V47() Cardinal-yielding countable V57() V58() integer complex-valued ext-real-valued real-valued natural-valued V65() decreasing non-decreasing non-increasing V71() V72() V73() V74() V75() V76() V77() V92() V93() V96() initial set

2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

proj1 {} is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V47() Cardinal-yielding countable V57() V58() integer complex-valued ext-real-valued real-valued natural-valued V65() decreasing non-decreasing non-increasing V71() V72() V73() V74() V75() V76() V77() V92() V93() V96() initial set

proj2 {} is empty trivial V4() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V47() Cardinal-yielding countable V57() V58() integer complex-valued ext-real-valued real-valued natural-valued V65() decreasing non-decreasing non-increasing V71() V72() V73() V74() V75() V76() V77() V92() V93() V96() initial set

card {} is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V47() Cardinal-yielding countable V57() V58() integer complex-valued ext-real-valued real-valued natural-valued V65() decreasing non-decreasing non-increasing V71() V72() V73() V74() V75() V76() V77() V92() V93() V96() initial set

{{}} is non empty trivial functional finite V40() 1 -element with_common_domain countable V71() V72() V73() V74() V75() V76() set

0 is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V47() Cardinal-yielding countable V57() V58() integer V60() complex-valued ext-real-valued real-valued natural-valued V65() decreasing non-decreasing non-increasing V71() V72() V73() V74() V75() V76() V77() V92() V93() V96() initial Element of NAT

[0,{},{}] is V7() V8() set

[0,{}] is non empty V7() set

{0,{}} is non empty functional finite V40() countable V71() V72() V73() V74() V75() V76() set

{0} is non empty trivial functional finite V40() 1 -element with_common_domain countable V71() V72() V73() V74() V75() V76() set

{{0,{}},{0}} is non empty V4() V5() finite V40() countable set

[[0,{}],{}] is non empty V7() set

{[0,{}],{}} is non empty finite countable set

{[0,{}]} is non empty trivial V4() V5() Relation-like Function-like constant finite 1 -element countable V93() set

{{[0,{}],{}},{[0,{}]}} is non empty V4() V5() finite V40() countable set

{[0,{},{}]} is non empty trivial Relation-like finite 1 -element countable standard-ins homogeneous J/A-independent V121() set

({[0,{},{}]}) is () ()

S is () ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

S is () ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

I is () ()

the of I is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

() is () ()

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

halt the of S is ins-loc-free Element of the of S

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

I is non empty Relation-like NAT -defined the of S -valued Function-like total set

J is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer set

I . J is set

proj1 I is non empty V71() V72() V73() V74() V75() V76() set

proj2 I is non empty set

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

I is non empty Relation-like NAT -defined the of S -valued Function-like total set

J is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer set

(S,I,J) is Element of the of S

(S) is Element of the of S

halt the of S is ins-loc-free Element of the of S

proj1 I is non empty V71() V72() V73() V74() V75() V76() set

I . J is set

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

the Element of the of S is Element of the of S

<% the Element of the of S%> is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial set

0 .--> the Element of the of S is non empty trivial Relation-like NAT -defined {0} -defined the of S -valued Function-like one-to-one constant finite 1 -element countable V93() set

{0} --> the Element of the of S is non empty Relation-like {0} -defined the of S -valued { the Element of the of S} -valued Function-like constant total V21({0},{ the Element of the of S}) finite countable V93() Element of bool [:{0},{ the Element of the of S}:]

{ the Element of the of S} is non empty trivial finite 1 -element countable set

[:{0},{ the Element of the of S}:] is non empty Relation-like finite countable set

bool [:{0},{ the Element of the of S}:] is non empty finite V40() countable set

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

(S) is Element of the of S

halt the of S is ins-loc-free Element of the of S

<%(S)%> is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial set

0 .--> (S) is non empty trivial Relation-like NAT -defined {0} -defined the of S -valued Function-like one-to-one constant finite 1 -element countable V93() set

{0} --> (S) is non empty Relation-like {0} -defined the of S -valued {(S)} -valued Function-like constant total V21({0},{(S)}) finite countable V93() Element of bool [:{0},{(S)}:]

{(S)} is non empty trivial finite 1 -element countable set

[:{0},{(S)}:] is non empty Relation-like finite countable set

bool [:{0},{(S)}:] is non empty finite V40() countable set

I is non empty Relation-like NAT -defined the of S -valued Function-like T-Sequence-like finite countable V93() initial set

the of () is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

S is Element of the of ()

InsCode S is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer Element of InsCodes the of ()

InsCodes the of () is non empty set

K51( the of ()) is set

proj1 the of () is non empty set

proj1 (proj1 the of ()) is set

K41(S) is set

K41(K41(S)) is set

S is ()

(S) is Element of the of S

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

halt the of S is ins-loc-free Element of the of S

<%(S)%> is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial set

0 .--> (S) is non empty trivial Relation-like NAT -defined {0} -defined the of S -valued Function-like one-to-one constant finite 1 -element countable V93() set

{0} --> (S) is non empty Relation-like {0} -defined the of S -valued {(S)} -valued Function-like constant total V21({0},{(S)}) finite countable V93() Element of bool [:{0},{(S)}:]

{(S)} is non empty trivial finite 1 -element countable set

[:{0},{(S)}:] is non empty Relation-like finite countable set

bool [:{0},{(S)}:] is non empty finite V40() countable set

S is ()

(S) is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

(S) is Element of the of S

halt the of S is ins-loc-free Element of the of S

<%(S)%> is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial set

0 .--> (S) is non empty trivial Relation-like NAT -defined {0} -defined the of S -valued Function-like one-to-one constant finite 1 -element countable V93() set

{0} --> (S) is non empty Relation-like {0} -defined the of S -valued {(S)} -valued Function-like constant total V21({0},{(S)}) finite countable V93() Element of bool [:{0},{(S)}:]

{(S)} is non empty trivial finite 1 -element countable set

[:{0},{(S)}:] is non empty Relation-like finite countable set

bool [:{0},{(S)}:] is non empty finite V40() countable set

S is ()

(S) is non empty Relation-like NAT -defined the of S -valued Function-like T-Sequence-like finite countable V93() initial set

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

(S) is Element of the of S

halt the of S is ins-loc-free Element of the of S

<%(S)%> is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial set

0 .--> (S) is non empty trivial Relation-like NAT -defined {0} -defined the of S -valued Function-like one-to-one constant finite 1 -element countable V93() set

{0} --> (S) is non empty Relation-like {0} -defined the of S -valued {(S)} -valued Function-like constant total V21({0},{(S)}) finite countable V93() Element of bool [:{0},{(S)}:]

{(S)} is non empty trivial finite 1 -element countable set

[:{0},{(S)}:] is non empty Relation-like finite countable set

bool [:{0},{(S)}:] is non empty finite V40() countable set

S is ()

(S) is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial set

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

(S) is Element of the of S

halt the of S is ins-loc-free Element of the of S

<%(S)%> is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial set

0 .--> (S) is non empty trivial Relation-like NAT -defined {0} -defined the of S -valued Function-like one-to-one constant finite 1 -element countable V93() set

{0} --> (S) is non empty Relation-like {0} -defined the of S -valued {(S)} -valued Function-like constant total V21({0},{(S)}) finite countable V93() Element of bool [:{0},{(S)}:]

{(S)} is non empty trivial finite 1 -element countable set

[:{0},{(S)}:] is non empty Relation-like finite countable set

bool [:{0},{(S)}:] is non empty finite V40() countable set

dom (S) is non empty trivial ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal 1 -element countable V57() V58() integer V71() V72() V73() V74() V75() V76() Element of bool NAT

{0} is non empty trivial functional finite V40() 1 -element with_common_domain countable V71() V72() V73() V74() V75() V76() Element of bool NAT

S is ()

(S) is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial set

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

(S) is Element of the of S

halt the of S is ins-loc-free Element of the of S

<%(S)%> is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial set

0 .--> (S) is non empty trivial Relation-like NAT -defined {0} -defined the of S -valued Function-like one-to-one constant finite 1 -element countable V93() set

{0} --> (S) is non empty Relation-like {0} -defined the of S -valued {(S)} -valued Function-like constant total V21({0},{(S)}) finite countable V93() Element of bool [:{0},{(S)}:]

{(S)} is non empty trivial finite 1 -element countable set

[:{0},{(S)}:] is non empty Relation-like finite countable set

bool [:{0},{(S)}:] is non empty finite V40() countable set

card (S) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of omega

proj1 (S) is non empty trivial ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal 1 -element countable V57() V58() integer V71() V72() V73() V74() V75() V76() set

(card (S)) -' 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

(card (S)) - 1 is ext-real V57() V58() integer set

1 - 1 is ext-real V57() V58() integer set

S is ()

(S) is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial set

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

(S) is Element of the of S

halt the of S is ins-loc-free Element of the of S

<%(S)%> is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial set

0 .--> (S) is non empty trivial Relation-like NAT -defined {0} -defined the of S -valued Function-like one-to-one constant finite 1 -element countable V93() set

{0} --> (S) is non empty Relation-like {0} -defined the of S -valued {(S)} -valued Function-like constant total V21({0},{(S)}) finite countable V93() Element of bool [:{0},{(S)}:]

{(S)} is non empty trivial finite 1 -element countable set

[:{0},{(S)}:] is non empty Relation-like finite countable set

bool [:{0},{(S)}:] is non empty finite V40() countable set

LastLoc (S) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

card (S) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of omega

proj1 (S) is non empty trivial ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal 1 -element countable V57() V58() integer V71() V72() V73() V74() V75() V76() set

(card (S)) -' 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

S is ()

(S) is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial set

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

(S) is Element of the of S

halt the of S is ins-loc-free Element of the of S

<%(S)%> is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial set

0 .--> (S) is non empty trivial Relation-like NAT -defined {0} -defined the of S -valued Function-like one-to-one constant finite 1 -element countable V93() set

{0} --> (S) is non empty Relation-like {0} -defined the of S -valued {(S)} -valued Function-like constant total V21({0},{(S)}) finite countable V93() Element of bool [:{0},{(S)}:]

{(S)} is non empty trivial finite 1 -element countable set

[:{0},{(S)}:] is non empty Relation-like finite countable set

bool [:{0},{(S)}:] is non empty finite V40() countable set

LastLoc (S) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

(S) . (LastLoc (S)) is set

(0 .--> (S)) . 0 is set

I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer set

(S) . I is set

proj1 (S) is non empty trivial ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal 1 -element countable V57() V58() integer V71() V72() V73() V74() V75() V76() set

dom (S) is non empty trivial ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal 1 -element countable V57() V58() integer V71() V72() V73() V74() V75() V76() Element of bool NAT

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

(S) is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial (S) (S) set

(S) is Element of the of S

halt the of S is ins-loc-free Element of the of S

<%(S)%> is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial set

0 .--> (S) is non empty trivial Relation-like NAT -defined {0} -defined the of S -valued Function-like one-to-one constant finite 1 -element countable V93() set

{0} --> (S) is non empty Relation-like {0} -defined the of S -valued {(S)} -valued Function-like constant total V21({0},{(S)}) finite countable V93() Element of bool [:{0},{(S)}:]

{(S)} is non empty trivial finite 1 -element countable set

[:{0},{(S)}:] is non empty Relation-like finite countable set

bool [:{0},{(S)}:] is non empty finite V40() countable set

I is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial (S) (S) set

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

(S) is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial (S) (S) set

(S) is Element of the of S

halt the of S is ins-loc-free Element of the of S

<%(S)%> is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial set

0 .--> (S) is non empty trivial Relation-like NAT -defined {0} -defined the of S -valued Function-like one-to-one constant finite 1 -element countable V93() set

{0} --> (S) is non empty Relation-like {0} -defined the of S -valued {(S)} -valued Function-like constant total V21({0},{(S)}) finite countable V93() Element of bool [:{0},{(S)}:]

{(S)} is non empty trivial finite 1 -element countable set

[:{0},{(S)}:] is non empty Relation-like finite countable set

bool [:{0},{(S)}:] is non empty finite V40() countable set

S is ()

(S) is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial (S) (S) set

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

(S) is Element of the of S

halt the of S is ins-loc-free Element of the of S

<%(S)%> is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial set

0 .--> (S) is non empty trivial Relation-like NAT -defined {0} -defined the of S -valued Function-like one-to-one constant finite 1 -element countable V93() set

{0} --> (S) is non empty Relation-like {0} -defined the of S -valued {(S)} -valued Function-like constant total V21({0},{(S)}) finite countable V93() Element of bool [:{0},{(S)}:]

{(S)} is non empty trivial finite 1 -element countable set

[:{0},{(S)}:] is non empty Relation-like finite countable set

bool [:{0},{(S)}:] is non empty finite V40() countable set

dom (S) is non empty trivial ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal 1 -element countable V57() V58() integer V71() V72() V73() V74() V75() V76() Element of bool NAT

S is ()

(S) is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial (S) (S) set

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

(S) is Element of the of S

halt the of S is ins-loc-free Element of the of S

<%(S)%> is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial set

0 .--> (S) is non empty trivial Relation-like NAT -defined {0} -defined the of S -valued Function-like one-to-one constant finite 1 -element countable V93() set

{0} --> (S) is non empty Relation-like {0} -defined the of S -valued {(S)} -valued Function-like constant total V21({0},{(S)}) finite countable V93() Element of bool [:{0},{(S)}:]

{(S)} is non empty trivial finite 1 -element countable set

[:{0},{(S)}:] is non empty Relation-like finite countable set

bool [:{0},{(S)}:] is non empty finite V40() countable set

card (S) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of omega

proj1 (S) is non empty trivial ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal 1 -element countable V57() V58() integer V71() V72() V73() V74() V75() V76() set

- 1 is non empty ext-real non positive negative V57() V58() integer set

S is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer set

S is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer set

I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

J is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

I - 1 is ext-real V57() V58() integer set

I + J is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

(I + J) - 3 is ext-real V57() V58() integer set

(I + J) - 2 is ext-real V57() V58() integer set

(I - 1) + 1 is ext-real V57() V58() integer set

1 + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

((I + J) - 3) + 1 is ext-real V57() V58() integer set

S is Element of the of ()

S `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like finite FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set

K41(S) is set

K41(S) `3_3 is set

[:NAT,NAT,NAT:] is non empty set

[:NAT,NAT:] is non empty non trivial V5() Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set

[:[:NAT,NAT:],NAT:] is non empty non trivial V5() Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set

[0,0,0] is V7() V8() Element of [:NAT,NAT,NAT:]

[0,0] is non empty V7() set

{0,0} is non empty functional finite V40() countable V71() V72() V73() V74() V75() V76() set

{{0,0},{0}} is non empty V4() V5() finite V40() countable set

[[0,0],0] is non empty V7() set

{[0,0],0} is non empty finite countable set

{[0,0]} is non empty trivial V4() V5() Relation-like Function-like constant finite 1 -element countable V93() set

{{[0,0],0},{[0,0]}} is non empty V4() V5() finite V40() countable set

{[0,0,0]} is non empty trivial Relation-like finite 1 -element countable standard-ins homogeneous J/A-independent V121() Element of bool [:NAT,NAT,NAT:]

bool [:NAT,NAT,NAT:] is non empty set

InsCodes the of () is non empty set

K51( the of ()) is set

proj1 the of () is non empty set

proj1 (proj1 the of ()) is set

S is Element of InsCodes the of ()

JumpParts S is non empty functional with_common_domain product-like set

{ (b

J is set

[:NAT,NAT,NAT:] is non empty set

[:NAT,NAT:] is non empty non trivial V5() Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set

[:[:NAT,NAT:],NAT:] is non empty non trivial V5() Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set

[0,0,0] is V7() V8() Element of [:NAT,NAT,NAT:]

[0,0] is non empty V7() set

{0,0} is non empty functional finite V40() countable V71() V72() V73() V74() V75() V76() set

{{0,0},{0}} is non empty V4() V5() finite V40() countable set

[[0,0],0] is non empty V7() set

{[0,0],0} is non empty finite countable set

{[0,0]} is non empty trivial V4() V5() Relation-like Function-like constant finite 1 -element countable V93() set

{{[0,0],0},{[0,0]}} is non empty V4() V5() finite V40() countable set

{[0,0,0]} is non empty trivial Relation-like finite 1 -element countable standard-ins homogeneous J/A-independent V121() Element of bool [:NAT,NAT,NAT:]

bool [:NAT,NAT,NAT:] is non empty set

(()) is Element of the of ()

halt the of () is ins-loc-free Element of the of ()

n is Element of the of ()

n `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like finite FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set

K41(n) is set

K41(n) `3_3 is set

InsCode n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer Element of InsCodes the of ()

K41(K41(n)) is set

J is set

n is Element of the of ()

n `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like finite FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set

K41(n) is set

K41(n) `3_3 is set

InsCode n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer Element of InsCodes the of ()

K41(K41(n)) is set

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

I is non empty Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

J is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer set

I . J is set

(S) is Element of the of S

halt the of S is ins-loc-free Element of the of S

proj1 I is non empty finite countable V71() V72() V73() V74() V75() V76() set

LastLoc I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

n is set

{n} is non empty trivial finite 1 -element countable set

l is set

l is set

[l,l] is non empty V7() set

{l,l} is non empty finite countable set

{l} is non empty trivial finite 1 -element countable set

{{l,l},{l}} is non empty V4() V5() finite V40() countable set

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

(S) is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial (S) (S) set

(S) is Element of the of S

halt the of S is ins-loc-free Element of the of S

<%(S)%> is non empty trivial Relation-like NAT -defined the of S -valued the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial (S) set

0 .--> (S) is non empty trivial Relation-like NAT -defined {0} -defined the of S -valued the of S -valued Function-like one-to-one constant finite 1 -element countable V93() (S) set

{0} --> (S) is non empty Relation-like {0} -defined the of S -valued {(S)} -valued Function-like constant total V21({0},{(S)}) finite countable V93() Element of bool [:{0},{(S)}:]

{(S)} is non empty trivial finite 1 -element countable set

[:{0},{(S)}:] is non empty Relation-like finite countable set

bool [:{0},{(S)}:] is non empty finite V40() countable set

I is non empty Relation-like NAT -defined the of S -valued Function-like T-Sequence-like finite countable V93() initial (S) (S) set

card I is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of omega

proj1 I is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V71() V72() V73() V74() V75() V76() set

J is set

{J} is non empty trivial finite 1 -element countable set

n is set

l is set

[n,l] is non empty V7() set

{n,l} is non empty finite countable set

{n} is non empty trivial finite 1 -element countable set

{{n,l},{n}} is non empty V4() V5() finite V40() countable set

dom I is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V71() V72() V73() V74() V75() V76() Element of bool NAT

(card I) -' 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

(card I) - 1 is ext-real V57() V58() integer set

LastLoc I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

I . 0 is set

proj2 I is non empty finite countable set

{l} is non empty trivial finite 1 -element countable set

[:NAT, the of S:] is non empty non trivial V5() Relation-like non finite set

[0,(S)] is non empty V7() Element of [:NAT, the of S:]

{0,(S)} is non empty finite countable set

{{0,(S)},{0}} is non empty V4() V5() finite V40() countable set

{[0,(S)]} is non empty trivial V4() V5() Relation-like NAT -defined the of S -valued the of S -valued Function-like constant finite 1 -element countable V93() (S) Element of bool [:NAT, the of S:]

bool [:NAT, the of S:] is non empty non trivial V5() non finite set

S is ()

(S) is non empty trivial Relation-like NAT -defined the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial (S) (S) set

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

(S) is Element of the of S

halt the of S is ins-loc-free Element of the of S

<%(S)%> is non empty trivial Relation-like NAT -defined the of S -valued the of S -valued Function-like constant T-Sequence-like finite 1 -element countable V93() initial (S) set

0 .--> (S) is non empty trivial Relation-like NAT -defined {0} -defined the of S -valued the of S -valued Function-like one-to-one constant finite 1 -element countable V93() (S) set

{0} --> (S) is non empty Relation-like {0} -defined the of S -valued {(S)} -valued Function-like constant total V21({0},{(S)}) finite countable V93() Element of bool [:{0},{(S)}:]

{(S)} is non empty trivial finite 1 -element countable set

[:{0},{(S)}:] is non empty Relation-like finite countable set

bool [:{0},{(S)}:] is non empty finite V40() countable set

LastLoc (S) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

I is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

proj1 I is finite countable V71() V72() V73() V74() V75() V76() set

J is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer set

n is set

l is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

l is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer set

I /. l is Element of the of S

IncAddr ((I /. l),J) is Element of the of S

n is Relation-like Function-like set

proj1 n is set

proj2 n is set

l is set

l is set

n . l is set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

I /. n is Element of the of S

IncAddr ((I /. n),J) is Element of the of S

l is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

proj1 l is finite countable V71() V72() V73() V74() V75() V76() set

l is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer set

l . l is set

I /. l is Element of the of S

IncAddr ((I /. l),J) is Element of the of S

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

I /. n is Element of the of S

IncAddr ((I /. n),J) is Element of the of S

n is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

proj1 n is finite countable V71() V72() V73() V74() V75() V76() set

l is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

proj1 l is finite countable V71() V72() V73() V74() V75() V76() set

l is set

n . l is set

l . l is set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer set

e is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

I /. e is Element of the of S

IncAddr ((I /. e),J) is Element of the of S

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

I is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

J is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer set

(S,I,J) is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

I is empty trivial Relation-like non-empty empty-yielding NAT -defined the of S -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V47() Cardinal-yielding countable V57() V58() integer complex-valued ext-real-valued real-valued natural-valued V65() decreasing non-decreasing non-increasing V71() V72() V73() V74() V75() V76() V77() V92() V93() V96() initial set

J is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer set

(S,I,J) is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

n is non empty Relation-like Function-like set

proj1 n is non empty set

proj1 (S,I,J) is finite countable V71() V72() V73() V74() V75() V76() set

dom I is empty trivial proper Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V47() Cardinal-yielding countable V57() V58() integer complex-valued ext-real-valued real-valued natural-valued V65() decreasing non-decreasing non-increasing V71() V72() V73() V74() V75() V76() V77() V92() V93() V96() initial Element of bool NAT

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

I is non empty Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

J is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer set

(S,I,J) is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

proj1 (S,I,J) is finite countable V71() V72() V73() V74() V75() V76() set

proj1 I is non empty finite countable V71() V72() V73() V74() V75() V76() set

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

I is Relation-like NAT -defined the of S -valued Function-like T-Sequence-like finite countable V93() initial set

J is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer set

(S,I,J) is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

proj1 (S,I,J) is finite countable V71() V72() V73() V74() V75() V76() set

dom I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V71() V72() V73() V74() V75() V76() Element of bool NAT

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

I is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

(S,I,0) is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

proj1 I is finite countable V71() V72() V73() V74() V75() V76() set

J is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer set

I . J is set

I /. J is Element of the of S

IncAddr ((I /. J),0) is Element of the of S

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

I is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

(S,I,0) is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

S is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer set

I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer set

S + I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer set

J is ()

the of J is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

n is Relation-like NAT -defined the of J -valued Function-like finite countable V93() set

(J,n,S) is Relation-like NAT -defined the of J -valued Function-like finite countable V93() set

(J,(J,n,S),I) is Relation-like NAT -defined the of J -valued Function-like finite countable V93() set

(J,n,(S + I)) is Relation-like NAT -defined the of J -valued Function-like finite countable V93() set

proj1 (J,(J,n,S),I) is finite countable V71() V72() V73() V74() V75() V76() set

proj1 (J,n,S) is finite countable V71() V72() V73() V74() V75() V76() set

proj1 n is finite countable V71() V72() V73() V74() V75() V76() set

proj1 (J,n,(S + I)) is finite countable V71() V72() V73() V74() V75() V76() set

l is set

(J,(J,n,S),I) . l is set

(J,n,(S + I)) . l is set

l is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

n /. l is Element of the of J

IncAddr ((n /. l),S) is Element of the of J

(J,n,S) . l is set

(J,n,S) /. l is Element of the of J

(J,(J,n,S),I) . l is set

IncAddr (((J,n,S) /. l),I) is Element of the of J

IncAddr ((n /. l),(S + I)) is Element of the of J

(J,n,(S + I)) . l is set

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

I is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

J is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer set

(S,I,J) is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

Shift ((S,I,J),J) is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

I is non empty Relation-like NAT -defined the of S -valued Function-like T-Sequence-like finite countable V93() initial set

CutLastLoc I is Relation-like NAT -defined the of S -valued Function-like T-Sequence-like finite countable V93() initial set

LastLoc I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

I . (LastLoc I) is set

(LastLoc I) .--> (I . (LastLoc I)) is non empty trivial Relation-like NAT -defined {(LastLoc I)} -defined Function-like one-to-one constant finite 1 -element countable V93() set

{(LastLoc I)} is non empty trivial finite V40() 1 -element countable V71() V72() V73() V74() V75() V76() set

{(LastLoc I)} --> (I . (LastLoc I)) is non empty Relation-like {(LastLoc I)} -defined {(I . (LastLoc I))} -valued Function-like constant total V21({(LastLoc I)},{(I . (LastLoc I))}) finite countable V93() Element of bool [:{(LastLoc I)},{(I . (LastLoc I))}:]

{(I . (LastLoc I))} is non empty trivial finite 1 -element countable set

[:{(LastLoc I)},{(I . (LastLoc I))}:] is non empty Relation-like finite countable set

bool [:{(LastLoc I)},{(I . (LastLoc I))}:] is non empty finite V40() countable set

I \ ((LastLoc I) .--> (I . (LastLoc I))) is Relation-like NAT -defined the of S -valued Function-like finite countable V93() Element of bool I

bool I is non empty finite V40() countable set

dom (CutLastLoc I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V71() V72() V73() V74() V75() V76() Element of bool NAT

card I is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of omega

proj1 I is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V71() V72() V73() V74() V75() V76() set

(card I) -' 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

J is non empty Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

(S,J,((card I) -' 1)) is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

(S,J,((card I) -' 1)) is non empty Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

Shift ((S,J,((card I) -' 1)),((card I) -' 1)) is non empty Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

proj1 (S,J,((card I) -' 1)) is finite countable V71() V72() V73() V74() V75() V76() set

(dom (CutLastLoc I)) /\ (proj1 (S,J,((card I) -' 1))) is finite countable V71() V72() V73() V74() V75() V76() Element of bool NAT

l is set

proj1 (S,J,((card I) -' 1)) is non empty finite countable V71() V72() V73() V74() V75() V76() set

{ (b

l is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

l + ((card I) -' 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

n is non empty Relation-like NAT -defined Function-like finite countable V93() set

LastLoc n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

card n is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of omega

(card n) -' 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

(card I) - 1 is ext-real V57() V58() integer set

((card I) -' 1) - 1 is ext-real V57() V58() integer set

(l + ((card I) -' 1)) - ((card I) -' 1) is ext-real V57() V58() integer set

(((card I) -' 1) - 1) - ((card I) -' 1) is ext-real V57() V58() integer set

((card I) -' 1) - 1 is ext-real V57() V58() integer set

((card I) -' 1) - 1 is ext-real V57() V58() integer set

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

(S) is Element of the of S

halt the of S is ins-loc-free Element of the of S

I is non empty Relation-like NAT -defined the of S -valued Function-like T-Sequence-like finite countable V93() initial (S) set

CutLastLoc I is Relation-like NAT -defined the of S -valued Function-like T-Sequence-like finite countable V93() initial set

LastLoc I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

I . (LastLoc I) is set

(LastLoc I) .--> (I . (LastLoc I)) is non empty trivial Relation-like NAT -defined {(LastLoc I)} -defined Function-like one-to-one constant finite 1 -element countable V93() set

{(LastLoc I)} is non empty trivial finite V40() 1 -element countable V71() V72() V73() V74() V75() V76() set

{(LastLoc I)} --> (I . (LastLoc I)) is non empty Relation-like {(LastLoc I)} -defined {(I . (LastLoc I))} -valued Function-like constant total V21({(LastLoc I)},{(I . (LastLoc I))}) finite countable V93() Element of bool [:{(LastLoc I)},{(I . (LastLoc I))}:]

{(I . (LastLoc I))} is non empty trivial finite 1 -element countable set

[:{(LastLoc I)},{(I . (LastLoc I))}:] is non empty Relation-like finite countable set

bool [:{(LastLoc I)},{(I . (LastLoc I))}:] is non empty finite V40() countable set

I \ ((LastLoc I) .--> (I . (LastLoc I))) is Relation-like NAT -defined the of S -valued Function-like finite countable V93() Element of bool I

bool I is non empty finite V40() countable set

dom (CutLastLoc I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V71() V72() V73() V74() V75() V76() Element of bool NAT

J is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer set

(CutLastLoc I) . J is set

dom I is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V71() V72() V73() V74() V75() V76() Element of bool NAT

I . J is set

{(LastLoc I)} is non empty trivial finite V40() 1 -element countable V71() V72() V73() V74() V75() V76() Element of bool NAT

(dom I) \ {(LastLoc I)} is finite countable V71() V72() V73() V74() V75() V76() Element of bool NAT

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

I is non empty Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

CutLastLoc I is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

LastLoc I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

I . (LastLoc I) is set

(LastLoc I) .--> (I . (LastLoc I)) is non empty trivial Relation-like NAT -defined {(LastLoc I)} -defined Function-like one-to-one constant finite 1 -element countable V93() set

{(LastLoc I)} is non empty trivial finite V40() 1 -element countable V71() V72() V73() V74() V75() V76() set

{(LastLoc I)} --> (I . (LastLoc I)) is non empty Relation-like {(LastLoc I)} -defined {(I . (LastLoc I))} -valued Function-like constant total V21({(LastLoc I)},{(I . (LastLoc I))}) finite countable V93() Element of bool [:{(LastLoc I)},{(I . (LastLoc I))}:]

{(I . (LastLoc I))} is non empty trivial finite 1 -element countable set

[:{(LastLoc I)},{(I . (LastLoc I))}:] is non empty Relation-like finite countable set

bool [:{(LastLoc I)},{(I . (LastLoc I))}:] is non empty finite V40() countable set

I \ ((LastLoc I) .--> (I . (LastLoc I))) is Relation-like NAT -defined the of S -valued Function-like finite countable V93() Element of bool I

bool I is non empty finite V40() countable set

J is non empty Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

card I is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of omega

(card I) -' 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

(S,J,((card I) -' 1)) is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

(S,J,((card I) -' 1)) is non empty Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

Shift ((S,J,((card I) -' 1)),((card I) -' 1)) is non empty Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

(CutLastLoc I) +* (S,J,((card I) -' 1)) is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

I is non empty Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

J is non empty Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

(S,I,J) is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

CutLastLoc I is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

LastLoc I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

I . (LastLoc I) is set

(LastLoc I) .--> (I . (LastLoc I)) is non empty trivial Relation-like NAT -defined {(LastLoc I)} -defined Function-like one-to-one constant finite 1 -element countable V93() set

{(LastLoc I)} is non empty trivial finite V40() 1 -element countable V71() V72() V73() V74() V75() V76() set

{(LastLoc I)} --> (I . (LastLoc I)) is non empty Relation-like {(LastLoc I)} -defined {(I . (LastLoc I))} -valued Function-like constant total V21({(LastLoc I)},{(I . (LastLoc I))}) finite countable V93() Element of bool [:{(LastLoc I)},{(I . (LastLoc I))}:]

{(I . (LastLoc I))} is non empty trivial finite 1 -element countable set

[:{(LastLoc I)},{(I . (LastLoc I))}:] is non empty Relation-like finite countable set

bool [:{(LastLoc I)},{(I . (LastLoc I))}:] is non empty finite V40() countable set

I \ ((LastLoc I) .--> (I . (LastLoc I))) is Relation-like NAT -defined the of S -valued Function-like finite countable V93() Element of bool I

bool I is non empty finite V40() countable set

card I is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of omega

(card I) -' 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

(S,J,((card I) -' 1)) is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

(S,J,((card I) -' 1)) is non empty Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

Shift ((S,J,((card I) -' 1)),((card I) -' 1)) is non empty Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

(CutLastLoc I) +* (S,J,((card I) -' 1)) is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

I is non empty Relation-like NAT -defined the of S -valued Function-like T-Sequence-like finite countable V93() initial set

card I is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of omega

proj1 I is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V71() V72() V73() V74() V75() V76() set

J is non empty Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

(S,I,J) is non empty Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

CutLastLoc I is Relation-like NAT -defined the of S -valued Function-like T-Sequence-like finite countable V93() initial set

LastLoc I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

I . (LastLoc I) is set

(LastLoc I) .--> (I . (LastLoc I)) is non empty trivial Relation-like NAT -defined {(LastLoc I)} -defined Function-like one-to-one constant finite 1 -element countable V93() set

{(LastLoc I)} is non empty trivial finite V40() 1 -element countable V71() V72() V73() V74() V75() V76() set

{(LastLoc I)} --> (I . (LastLoc I)) is non empty Relation-like {(LastLoc I)} -defined {(I . (LastLoc I))} -valued Function-like constant total V21({(LastLoc I)},{(I . (LastLoc I))}) finite countable V93() Element of bool [:{(LastLoc I)},{(I . (LastLoc I))}:]

{(I . (LastLoc I))} is non empty trivial finite 1 -element countable set

[:{(LastLoc I)},{(I . (LastLoc I))}:] is non empty Relation-like finite countable set

bool [:{(LastLoc I)},{(I . (LastLoc I))}:] is non empty finite V40() countable set

I \ ((LastLoc I) .--> (I . (LastLoc I))) is Relation-like NAT -defined the of S -valued Function-like finite countable V93() Element of bool I

bool I is non empty finite V40() countable set

(card I) -' 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

(S,J,((card I) -' 1)) is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

(S,J,((card I) -' 1)) is non empty Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

Shift ((S,J,((card I) -' 1)),((card I) -' 1)) is non empty Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

(CutLastLoc I) +* (S,J,((card I) -' 1)) is Relation-like NAT -defined the of S -valued Function-like finite countable V93() set

card (S,I,J) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of omega

card J is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of omega

(card I) + (card J) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

((card I) + (card J)) - 1 is ext-real V57() V58() integer set

((card I) + (card J)) -' 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

proj1 (S,J,((card I) -' 1)) is non empty finite countable V71() V72() V73() V74() V75() V76() set

proj1 (S,J,((card I) -' 1)) is finite countable V71() V72() V73() V74() V75() V76() set

dom (CutLastLoc I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V71() V72() V73() V74() V75() V76() Element of bool NAT

card (CutLastLoc I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of omega

proj1 (CutLastLoc I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V71() V72() V73() V74() V75() V76() set

card (S,J,((card I) -' 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of omega

(card (CutLastLoc I)) + (card (S,J,((card I) -' 1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

card (S,J,((card I) -' 1)) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of omega

(card (CutLastLoc I)) + (card (S,J,((card I) -' 1))) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

card (proj1 (S,J,((card I) -' 1))) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of omega

(card (CutLastLoc I)) + (card (proj1 (S,J,((card I) -' 1)))) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

proj1 J is non empty finite countable V71() V72() V73() V74() V75() V76() set

card (proj1 J) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of omega

(card (CutLastLoc I)) + (card (proj1 J)) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

(card (CutLastLoc I)) + (card J) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT

(card I) - 1 is ext-real V57() V58() integer set

((card I) - 1) + (card J) is ext-real V57() V58() integer set

S is ()

the of S is non empty Relation-like standard-ins homogeneous J/A-independent V121() set

I is non empty Relation-like NAT -defined the of S -valued Function-like T-Sequence-like finite countable V93() initial set

J is non empty Relation-like NAT -defined the of S -valued Function-like T-Sequence-like finite countable V93() initial set

(S,I,J) is non empty