:: REWRITE2 semantic presentation

begin

theorem :: REWRITE2:1
for k being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Nat)
for p being ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) st not k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Nat) in dom p : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) & k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Nat) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative V81() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative V81() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) in dom p : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Nat) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional finite FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V60() V81() irreflexive ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: REWRITE2:2
for k being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Nat)
for p, q being ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) st k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Nat) > len p : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Nat) <= len (p : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) ^ q : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) ) : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) set ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
ex l being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Nat) st
( k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Nat) = (len p : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) + l : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Nat) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & l : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Nat) >= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative V81() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & l : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Nat) <= len q : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: REWRITE2:3
for k being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Nat)
for R being ( ( Relation-like ) ( Relation-like ) Relation)
for p being ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) RedSequence of R : ( ( Relation-like ) ( Relation-like ) Relation) ) st k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Nat) >= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative V81() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
p : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) RedSequence of b2 : ( ( Relation-like ) ( Relation-like ) Relation) ) | k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Nat) : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) set ) is ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) RedSequence of R : ( ( Relation-like ) ( Relation-like ) Relation) ) ;

theorem :: REWRITE2:4
for k being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Nat)
for R being ( ( Relation-like ) ( Relation-like ) Relation)
for p being ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) RedSequence of R : ( ( Relation-like ) ( Relation-like ) Relation) ) st k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Nat) in dom p : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) RedSequence of b2 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( non empty ) Element of K6(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
ex q being ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) RedSequence of R : ( ( Relation-like ) ( Relation-like ) Relation) ) st
( len q : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) RedSequence of b2 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) = k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Nat) & q : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) RedSequence of b2 : ( ( Relation-like ) ( Relation-like ) Relation) ) . 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative V81() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = p : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) RedSequence of b2 : ( ( Relation-like ) ( Relation-like ) Relation) ) . 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative V81() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) & q : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) RedSequence of b2 : ( ( Relation-like ) ( Relation-like ) Relation) ) . (len q : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) RedSequence of b2 : ( ( Relation-like ) ( Relation-like ) Relation) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = p : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) RedSequence of b2 : ( ( Relation-like ) ( Relation-like ) Relation) ) . k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Nat) : ( ( ) ( ) set ) ) ;

begin

definition
let f be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
attr f is XFinSequence-yielding means :: REWRITE2:def 1
 for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom f : ( ( ) ( ) GrammarStr ) : ( ( ) ( ) set ) holds
f : ( ( ) ( ) GrammarStr ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) is ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) ;
end;

registration
cluster empty Relation-like Function-like -> Relation-like Function-like XFinSequence-yielding for ( ( ) ( ) set ) ;
end;

registration
let f be ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) ;
cluster <*f : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) set ) *> : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V39(1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative V81() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) set ) -> XFinSequence-yielding ;
end;

registration
let p be ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like Function-like XFinSequence-yielding ) Function) ;
let x be ( ( ) ( ) set ) ;
cluster p : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like Function-like XFinSequence-yielding ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) -> Relation-like Function-like finite ;
end;

registration
let p be ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like Function-like XFinSequence-yielding ) Function) ;
let x be ( ( ) ( ) set ) ;
cluster p : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like Function-like XFinSequence-yielding ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( Relation-like Function-like finite ) set ) -> T-Sequence-like ;
end;

registration
cluster Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding for ( ( ) ( ) set ) ;
end;

registration
let E be ( ( ) ( ) set ) ;
cluster -> XFinSequence-yielding for ( ( ) ( ) FinSequence of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;
end;

registration
let p, q be ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) ;
cluster p : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) set ) ^ q : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) set ) : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) set ) -> Relation-like Function-like FinSequence-like XFinSequence-yielding ;
end;

begin

definition
let s be ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) ;
let p be ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like Function-like XFinSequence-yielding ) Function) ;
func s ^+ p -> ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like Function-like XFinSequence-yielding ) Function) means :: REWRITE2:def 2
( dom it : ( ( ) ( Relation-like ) Element of K6(([#] (s : ( ( ) ( ) set ) ,K250(s : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M12(s : ( ( ) ( ) set ) )) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = dom p : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) & ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom p : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) holds
it : ( ( ) ( Relation-like ) Element of K6(([#] (s : ( ( ) ( ) set ) ,K250(s : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M12(s : ( ( ) ( ) set ) )) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = s : ( ( ) ( ) set ) ^ (p : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) . x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( T-Sequence-like Relation-like Function-like ) ( T-Sequence-like Relation-like Function-like ) set ) ) );
func p +^ s -> ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like Function-like XFinSequence-yielding ) Function) means :: REWRITE2:def 3
( dom it : ( ( ) ( Relation-like ) Element of K6(([#] (s : ( ( ) ( ) set ) ,K250(s : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M12(s : ( ( ) ( ) set ) )) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = dom p : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) & ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom p : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) holds
it : ( ( ) ( Relation-like ) Element of K6(([#] (s : ( ( ) ( ) set ) ,K250(s : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M12(s : ( ( ) ( ) set ) )) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (p : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) . x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ^ s : ( ( ) ( ) set ) : ( ( T-Sequence-like Relation-like Function-like ) ( T-Sequence-like Relation-like Function-like ) set ) ) );
end;

registration
let s be ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) ;
let p be ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) ;
cluster s : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) set ) ^+ p : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) set ) : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like Function-like XFinSequence-yielding ) Function) -> Relation-like Function-like FinSequence-like XFinSequence-yielding ;
cluster p : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) set ) +^ s : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) set ) : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like Function-like XFinSequence-yielding ) Function) -> Relation-like Function-like FinSequence-like XFinSequence-yielding ;
end;

theorem :: REWRITE2:5
for s being ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence)
for p being ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) holds
( len (s : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) ^+ p : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) ) : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) Function) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) = len p : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & len (p : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) +^ s : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) ) : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) Function) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) = len p : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: REWRITE2:6
for E being ( ( ) ( ) set )
for p being ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) holds
( (<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( ) ( ) set ) -valued Function-like one-to-one constant functional finite FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V60() V81() irreflexive XFinSequence-yielding ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ^+ p : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) Function) = p : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) & p : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) +^ (<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( ) ( ) set ) -valued Function-like one-to-one constant functional finite FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V60() V81() irreflexive XFinSequence-yielding ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) Function) = p : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) ) ;

theorem :: REWRITE2:7
for s, t being ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence)
for p being ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) holds
( s : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) ^+ (t : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) ^+ p : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) ) : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) Function) : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) Function) = (s : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) ^ t : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) ) : ( ( T-Sequence-like Relation-like Function-like ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) set ) ^+ p : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) Function) & (p : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) +^ t : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) ) : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) Function) +^ s : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) Function) = p : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) +^ (t : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) ^ s : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) ) : ( ( T-Sequence-like Relation-like Function-like ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) set ) : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) Function) ) ;

theorem :: REWRITE2:8
for s, t being ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence)
for p being ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) holds s : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) ^+ (p : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) +^ t : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) ) : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) Function) : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) Function) = (s : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) ^+ p : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) ) : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) Function) +^ t : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) Function) ;

theorem :: REWRITE2:9
for s being ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence)
for p, q being ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) holds
( s : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) ^+ (p : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) ^ q : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) ) : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) set ) : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) Function) = (s : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) ^+ p : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) ) : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) Function) ^ (s : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) ^+ q : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) ) : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) Function) : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) set ) & (p : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) ^ q : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) ) : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) set ) +^ s : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) Function) = (p : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) +^ s : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) ) : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) Function) ^ (q : ( ( Relation-like Function-like FinSequence-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence) +^ s : ( ( T-Sequence-like Relation-like Function-like finite ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) XFinSequence) ) : ( ( Relation-like Function-like XFinSequence-yielding ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) Function) : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) set ) ) ;

begin

definition
let E be ( ( ) ( ) set ) ;
let p be ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;
let k be ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() ) Nat) ;
:: original: .
redefine func p . k -> ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;
end;

definition
let E be ( ( ) ( ) set ) ;
let s be ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;
let p be ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;
:: original: ^+
redefine func s ^+ p -> ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;
:: original: +^
redefine func p +^ s -> ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;
end;

definition
let E be ( ( ) ( ) set ) ;
mode semi-Thue-system of E is ( ( ) ( Relation-like ) Relation of ) ;
end;

registration
let S be ( ( Relation-like ) ( Relation-like ) Relation) ;
cluster S : ( ( Relation-like ) ( Relation-like ) set ) \/ (S : ( ( Relation-like ) ( Relation-like ) set ) ~) : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( Relation-like ) set ) -> symmetric ;
end;

registration
let E be ( ( ) ( ) set ) ;
cluster Relation-like symmetric for ( ( ) ( ) Element of K6(([#] ((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ;
end;

definition
let E be ( ( ) ( ) set ) ;
mode Thue-system of E is ( ( symmetric ) ( Relation-like symmetric ) semi-Thue-system of E : ( ( ) ( ) set ) ) ;
end;

begin

definition
let E be ( ( ) ( ) set ) ;
let S be ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) ) ;
let s, t be ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;
pred s -->. t,S means :: REWRITE2:def 4
[s : ( ( ) ( Relation-like ) Element of K6(([#] (E : ( ( ) ( ) set ) ,K250(E : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M12(E : ( ( ) ( ) set ) )) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ,t : ( ( Function-like V29(E : ( ( ) ( ) set ) ,S : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) ) ( Relation-like Function-like V29(E : ( ( ) ( ) set ) ,S : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) ) Element of K6(([#] (E : ( ( ) ( ) set ) ,S : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ] : ( ( ) ( ) Element of [#] ((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( Relation-like ) set ) ) in S : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ;
end;

definition
let E be ( ( ) ( ) set ) ;
let S be ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) ) ;
let s, t be ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;
pred s ==>. t,S means :: REWRITE2:def 5
 ex v, w, s1, t1 being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st
( s : ( ( ) ( Relation-like ) Element of K6(([#] (E : ( ( ) ( ) set ) ,K250(E : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M12(E : ( ( ) ( ) set ) )) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) = (v : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ s1 : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(E : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(E : ( ( ) ( ) set ) )) ) ^ w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(E : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(E : ( ( ) ( ) set ) )) ) & t : ( ( Function-like V29(E : ( ( ) ( ) set ) ,S : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) ) ( Relation-like Function-like V29(E : ( ( ) ( ) set ) ,S : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) ) Element of K6(([#] (E : ( ( ) ( ) set ) ,S : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) = (v : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ t1 : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(E : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(E : ( ( ) ( ) set ) )) ) ^ w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(E : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(E : ( ( ) ( ) set ) )) ) & s1 : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) -->. t1 : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) );
end;

theorem :: REWRITE2:10
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) -->. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:11
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>. s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
ex v, w, s1 being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st
( s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) = (v : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ s1 : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ^ w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) & s1 : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) -->. s1 : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: REWRITE2:12
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t, u being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
( u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ==>. u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) & s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ==>. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: REWRITE2:13
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t, u, v being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
(u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ^ v : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ==>. (u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ^ v : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:14
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t, u being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) -->. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
( u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ==>. u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) & s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ==>. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: REWRITE2:15
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t, u, v being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) -->. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
(u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ^ v : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ==>. (u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ^ v : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:16
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) is ( ( symmetric ) ( Relation-like symmetric ) Thue-system of E : ( ( ) ( ) set ) ) & s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) -->. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) -->. s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:17
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) is ( ( symmetric ) ( Relation-like symmetric ) Thue-system of E : ( ( ) ( ) set ) ) & s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>. s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:18
for E being ( ( ) ( ) set )
for S, T being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) c= T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) & s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) -->. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) -->. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:19
for E being ( ( ) ( ) set )
for S, T being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) c= T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) & s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:20
for E being ( ( ) ( ) set )
for s, t being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) holds not s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) , {} ((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( Relation-like ) Element of K6(([#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:21
for E being ( ( ) ( ) set )
for S, T being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) holds
( not s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) \/ T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Element of K6(([#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) or s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) or s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ) ;

begin

definition
let E be ( ( ) ( ) set ) ;
:: original: id
redefine func id E -> ( ( ) ( Relation-like ) Relation of ) ;
end;

definition
let E be ( ( ) ( ) set ) ;
let S be ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) ) ;
func ==>.-relation S -> ( ( ) ( Relation-like ) Relation of ) means :: REWRITE2:def 6
 for s, t being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) holds
( [s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ] : ( ( ) ( ) Element of [#] ((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( Relation-like ) set ) ) in it : ( ( ) ( Relation-like ) Element of K6(([#] (E : ( ( ) ( ) set ) ,K250(E : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M12(E : ( ( ) ( ) set ) )) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) iff s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) );
end;

theorem :: REWRITE2:22
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) ) holds S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) c= ==>.-relation S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Relation of ) ;

theorem :: REWRITE2:23
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for u being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) )
for p being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st p : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) is ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) RedSequence of ==>.-relation S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Relation of ) ) holds
( p : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) +^ u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) is ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) RedSequence of ==>.-relation S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Relation of ) ) & u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^+ p : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) is ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) RedSequence of ==>.-relation S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Relation of ) ) ) ;

theorem :: REWRITE2:24
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for t, u being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) )
for p being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st p : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) is ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) RedSequence of ==>.-relation S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Relation of ) ) holds
(t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^+ p : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) +^ u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding ) FinSequence of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) is ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) RedSequence of ==>.-relation S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Relation of ) ) ;

theorem :: REWRITE2:25
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) ) st S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) is ( ( symmetric ) ( Relation-like symmetric ) Thue-system of E : ( ( ) ( ) set ) ) holds
==>.-relation S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Relation of ) = (==>.-relation S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like ) Relation of ) ~ : ( ( ) ( Relation-like ) Element of K6(([#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:26
for E being ( ( ) ( ) set )
for S, T being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) ) st S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) c= T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
==>.-relation S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Relation of ) c= ==>.-relation T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Relation of ) ;

theorem :: REWRITE2:27
for E being ( ( ) ( ) set ) holds ==>.-relation (id (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -defined b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like one-to-one ) Relation of ) : ( ( ) ( Relation-like ) Relation of ) = id (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -defined b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like one-to-one ) Relation of ) ;

theorem :: REWRITE2:28
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) ) holds ==>.-relation (S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) \/ (id (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -defined b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like one-to-one ) Relation of ) ) : ( ( ) ( Relation-like ) Element of K6(([#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Relation of ) = (==>.-relation S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like ) Relation of ) \/ (id (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -defined b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like one-to-one ) Relation of ) : ( ( ) ( Relation-like ) Element of K6(([#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:29
for E being ( ( ) ( ) set ) holds ==>.-relation ({} ((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) Element of K6(([#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Relation of ) = {} ((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( Relation-like ) Element of K6(([#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:30
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) , ==>.-relation S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Relation of ) holds
s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:31
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) ) holds ==>.-relation (==>.-relation S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like ) Relation of ) : ( ( ) ( Relation-like ) Relation of ) = ==>.-relation S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Relation of ) ;

begin

definition
let E be ( ( ) ( ) set ) ;
let S be ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) ) ;
let s, t be ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;
pred s ==>* t,S means :: REWRITE2:def 7
 ==>.-relation S : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( Relation-like ) Relation of ) reduces s : ( ( ) ( Relation-like ) Element of K6(([#] (E : ( ( ) ( ) set ) ,K250(E : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M12(E : ( ( ) ( ) set ) )) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ,t : ( ( Function-like V29(E : ( ( ) ( ) set ) ,S : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) ) ( Relation-like Function-like V29(E : ( ( ) ( ) set ) ,S : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) ) Element of K6(([#] (E : ( ( ) ( ) set ) ,S : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ;
end;

theorem :: REWRITE2:32
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) holds s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:33
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:34
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) -->. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:35
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t, u being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) & t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:36
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t, u being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
( s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ==>* t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) & u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ==>* u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: REWRITE2:37
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t, u, v being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
(u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ^ v : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ==>* (u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ^ v : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:38
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t, u, v being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) & u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* v : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
( s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ==>* t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ v : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) & u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ==>* v : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ^ t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: REWRITE2:39
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) is ( ( symmetric ) ( Relation-like symmetric ) Thue-system of E : ( ( ) ( ) set ) ) & s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:40
for E being ( ( ) ( ) set )
for S, T being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) c= T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) & s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:41
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) holds
( s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) iff s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) \/ (id (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -defined b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like one-to-one ) Relation of ) : ( ( ) ( Relation-like ) Element of K6(([#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: REWRITE2:42
for E being ( ( ) ( ) set )
for s, t being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) , {} ((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( Relation-like ) Element of K6(([#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) holds
s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) = t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;

theorem :: REWRITE2:43
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) , ==>.-relation S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Relation of ) holds
s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:44
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t, u, v being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) & u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>. v : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,{[s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ] : ( ( ) ( ) Element of [#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( Relation-like ) set ) ) } : ( ( ) ( non empty Relation-like Function-like ) Element of K6(([#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) holds
u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* v : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:45
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t, u, v being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) & u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* v : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) \/ {[s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ] : ( ( ) ( ) Element of [#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( Relation-like ) set ) ) } : ( ( ) ( non empty Relation-like Function-like ) Element of K6(([#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty Relation-like ) Element of K6(([#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) holds
u : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* v : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ;

begin

definition
let E be ( ( ) ( ) set ) ;
let S be ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) ) ;
let w be ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;
func Lang (w,S) -> ( ( ) ( functional ) Subset of ( ( ) ( ) set ) ) equals :: REWRITE2:def 8
 { s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) where s is ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) : w : ( ( ) ( Relation-like ) Element of K6(([#] (E : ( ( ) ( ) set ) ,K250(E : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M12(E : ( ( ) ( ) set ) )) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ==>* s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) } ;
end;

theorem :: REWRITE2:46
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, w being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) holds
( s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) in Lang (w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( ) set ) ) iff w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: REWRITE2:47
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for w being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) holds w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) in Lang (w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( ) set ) ) ;

registration
let E be ( ( non empty ) ( non empty ) set ) ;
let S be ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( non empty ) ( non empty ) set ) ) ;
let w be ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( non empty ) ( non empty ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;
cluster Lang (w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( non empty ) ( non empty ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) Element of K6(([#] ((E : ( ( non empty ) ( non empty ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(E : ( ( non empty ) ( non empty ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( ) set ) ) -> non empty ;
end;

theorem :: REWRITE2:48
for E being ( ( ) ( ) set )
for S, T being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for w being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) c= T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
Lang (w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( ) set ) ) c= Lang (w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:49
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for w being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) holds Lang (w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( ) set ) ) = Lang (w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,(S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) \/ (id (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -defined b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like one-to-one ) Relation of ) ) : ( ( ) ( Relation-like ) Element of K6(([#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:50
for E being ( ( ) ( ) set )
for w being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) holds Lang (w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,({} ((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) Element of K6(([#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( ) set ) ) = {w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) } : ( ( ) ( non empty functional ) Element of K6(K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:51
for E being ( ( ) ( ) set )
for w being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) holds Lang (w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,(id (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -defined b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like one-to-one ) Relation of ) ) : ( ( ) ( functional ) Subset of ( ( ) ( ) set ) ) = {w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) } : ( ( ) ( non empty functional ) Element of K6(K237(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty functional ) M11(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( ) set ) ) ;

begin

definition
let E be ( ( ) ( ) set ) ;
let S, T be ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) ) ;
let w be ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;
pred S,T are_equivalent_wrt w means :: REWRITE2:def 9
 Lang (w : ( ( Function-like V29(E : ( ( ) ( ) set ) ,S : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) ) ( Relation-like Function-like V29(E : ( ( ) ( ) set ) ,S : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) ) Element of K6(([#] (E : ( ( ) ( ) set ) ,S : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ,S : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( ) set ) ) = Lang (w : ( ( Function-like V29(E : ( ( ) ( ) set ) ,S : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) ) ( Relation-like Function-like V29(E : ( ( ) ( ) set ) ,S : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) ) Element of K6(([#] (E : ( ( ) ( ) set ) ,S : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ,T : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( ) set ) ) ;
end;

theorem :: REWRITE2:52
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for w being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) holds S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) are_equivalent_wrt w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;

theorem :: REWRITE2:53
for E being ( ( ) ( ) set )
for S, T being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for w being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ,T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) are_equivalent_wrt w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) holds
T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) are_equivalent_wrt w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;

theorem :: REWRITE2:54
for E being ( ( ) ( ) set )
for S, T, U being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for w being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ,T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) are_equivalent_wrt w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) & T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ,U : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) are_equivalent_wrt w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) holds
S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ,U : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) are_equivalent_wrt w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;

theorem :: REWRITE2:55
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for w being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) holds S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) \/ (id (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -defined b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) -valued Function-like one-to-one ) Relation of ) : ( ( ) ( Relation-like ) Element of K6(([#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) are_equivalent_wrt w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;

theorem :: REWRITE2:56
for E being ( ( ) ( ) set )
for S, T, U being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for w being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ,T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) are_equivalent_wrt w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) & S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) c= U : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) & U : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) c= T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
( S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ,U : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) are_equivalent_wrt w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) & U : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ,T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) are_equivalent_wrt w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ) ;

theorem :: REWRITE2:57
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for w being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) holds S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) , ==>.-relation S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Relation of ) are_equivalent_wrt w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;

theorem :: REWRITE2:58
for E being ( ( ) ( ) set )
for S, T being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for w, s being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ,T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) are_equivalent_wrt w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) & ==>.-relation (S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) \/ T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like ) Element of K6(([#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Relation of ) reduces w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) holds
==>.-relation S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Relation of ) reduces w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;

theorem :: REWRITE2:59
for E being ( ( ) ( ) set )
for S, T being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for w, s being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ,T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) are_equivalent_wrt w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) & w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) \/ T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Element of K6(([#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) holds
w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ;

theorem :: REWRITE2:60
for E being ( ( ) ( ) set )
for S, T being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for w being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ,T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) are_equivalent_wrt w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) holds
S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) \/ T : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Element of K6(([#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) are_equivalent_wrt w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;

theorem :: REWRITE2:61
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t, w being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>. t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) \/ {[s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ] : ( ( ) ( ) Element of [#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( Relation-like ) set ) ) } : ( ( ) ( non empty Relation-like Function-like ) Element of K6(([#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty Relation-like ) Element of K6(([#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) are_equivalent_wrt w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;

theorem :: REWRITE2:62
for E being ( ( ) ( ) set )
for S being ( ( ) ( Relation-like ) semi-Thue-system of E : ( ( ) ( ) set ) )
for s, t, w being ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) st s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ==>* t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) holds
S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) ,S : ( ( ) ( Relation-like ) semi-Thue-system of b1 : ( ( ) ( ) set ) ) \/ {[s : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ,t : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ] : ( ( ) ( ) Element of [#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( Relation-like ) set ) ) } : ( ( ) ( non empty Relation-like Function-like ) Element of K6(([#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty Relation-like ) Element of K6(([#] ((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) ,(b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) set ) )) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) are_equivalent_wrt w : ( ( ) ( T-Sequence-like Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite V60() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) set ) ) ;