let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S
for t being Element of (Free (S,X))
for xi1, xi2 being FinSequence st xi1 <> xi2 & xi1 in dom t & xi2 in dom t holds
for s1, s2 being SortSymbol of S
for x1 being Element of X . s1
for x2 being Element of X . s2 st t . xi1 = [x1,s1] holds
not xi1 is_a_prefix_of xi2
let X be V5() ManySortedSet of the carrier of S; :: thesis: for t being Element of (Free (S,X))
for xi1, xi2 being FinSequence st xi1 <> xi2 & xi1 in dom t & xi2 in dom t holds
for s1, s2 being SortSymbol of S
for x1 being Element of X . s1
for x2 being Element of X . s2 st t . xi1 = [x1,s1] holds
not xi1 is_a_prefix_of xi2
let t be Element of (Free (S,X)); :: thesis: for xi1, xi2 being FinSequence st xi1 <> xi2 & xi1 in dom t & xi2 in dom t holds
for s1, s2 being SortSymbol of S
for x1 being Element of X . s1
for x2 being Element of X . s2 st t . xi1 = [x1,s1] holds
not xi1 is_a_prefix_of xi2
let xi1, xi2 be FinSequence; :: thesis: ( xi1 <> xi2 & xi1 in dom t & xi2 in dom t implies for s1, s2 being SortSymbol of S
for x1 being Element of X . s1
for x2 being Element of X . s2 st t . xi1 = [x1,s1] holds
not xi1 is_a_prefix_of xi2 )
assume Z0: xi1 <> xi2 ; :: thesis: ( not xi1 in dom t or not xi2 in dom t or for s1, s2 being SortSymbol of S
for x1 being Element of X . s1
for x2 being Element of X . s2 st t . xi1 = [x1,s1] holds
not xi1 is_a_prefix_of xi2 )
assume xi1 in dom t ; :: thesis: ( not xi2 in dom t or for s1, s2 being SortSymbol of S
for x1 being Element of X . s1
for x2 being Element of X . s2 st t . xi1 = [x1,s1] holds
not xi1 is_a_prefix_of xi2 )
then reconsider nu1 = xi1 as Element of dom t ;
assume Z2: xi2 in dom t ; :: thesis: for s1, s2 being SortSymbol of S
for x1 being Element of X . s1
for x2 being Element of X . s2 st t . xi1 = [x1,s1] holds
not xi1 is_a_prefix_of xi2
let s1, s2 be SortSymbol of S; :: thesis: for x1 being Element of X . s1
for x2 being Element of X . s2 st t . xi1 = [x1,s1] holds
not xi1 is_a_prefix_of xi2
let x1 be Element of X . s1; :: thesis: for x2 being Element of X . s2 st t . xi1 = [x1,s1] holds
not xi1 is_a_prefix_of xi2
let x2 be Element of X . s2; :: thesis: ( t . xi1 = [x1,s1] implies not xi1 is_a_prefix_of xi2 )
assume Z3: t . xi1 = [x1,s1] ; :: thesis: not xi1 is_a_prefix_of xi2
assume xi1 is_a_prefix_of xi2 ; :: thesis: contradiction
then consider r being FinSequence such that
A1: xi2 = xi1 ^ r by TREES_1:1;
reconsider t1 = t | nu1 as Element of (Free (S,X)) by MSAFREE4:44;
<*> NAT in (dom t) | nu1 by TREES_1:22;
then A2: t1 . {} = t . (nu1 ^ {}) by TREES_2:def 10;
xi2 is Element of dom t by Z2;
then reconsider r = r as FinSequence of NAT by A1, FINSEQ_1:36;