let S be non empty non void ManySortedSign ; for X being V5() ManySortedSet of the carrier of S
for t, t1 being Element of (Free (S,X)) st t c= t1 holds
t = t1
let X be V5() ManySortedSet of the carrier of S; for t, t1 being Element of (Free (S,X)) st t c= t1 holds
t = t1
let t, t1 be Element of (Free (S,X)); ( t c= t1 implies t = t1 )
assume A1:
t c= t1
; t = t1
defpred S1[ Element of (Free (S,X))] means for t1 being Element of (Free (S,X)) st $1 c= t1 holds
$1 = t1;
A2:
for s being SortSymbol of S
for x being Element of X . s holds S1[x -term ]
A7:
for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X))) st ( for t being Element of (Free (S,X)) st t in rng p holds
S1[t] ) holds
S1[o -term p]
proof
let o be
OperSymbol of
S;
for p being Element of Args (o,(Free (S,X))) st ( for t being Element of (Free (S,X)) st t in rng p holds
S1[t] ) holds
S1[o -term p]let p be
Element of
Args (
o,
(Free (S,X)));
( ( for t being Element of (Free (S,X)) st t in rng p holds
S1[t] ) implies S1[o -term p] )
assume Z0:
for
t being
Element of
(Free (S,X)) st
t in rng p holds
S1[
t]
;
S1[o -term p]
let t1 be
Element of
(Free (S,X));
( o -term p c= t1 implies o -term p = t1 )
assume Z1:
o -term p c= t1
;
o -term p = t1
{} in dom (o -term p)
by TREES_1:22;
then A8:
(
t1 . {} = (o -term p) . {} &
(o -term p) . {} = [o, the carrier of S] )
by Z1, GRFUNC_1:2, TREES_4:def 4;
per cases
( ex s being SortSymbol of S ex x being Element of X . s st t1 = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t1 = o -term p )
by Th16;
suppose
ex
o being
OperSymbol of
S ex
p being
Element of
Args (
o,
(Free (S,X))) st
t1 = o -term p
;
o -term p = t1then consider o1 being
OperSymbol of
S,
p1 being
Element of
Args (
o1,
(Free (S,X)))
such that A6:
t1 = o1 -term p1
;
t1 . {} = [o1, the carrier of S]
by A6, TREES_4:def 4;
then A7:
o = o1
by A8, XTUPLE_0:1;
p = p1
proof
A8:
(
dom p = dom (the_arity_of o) &
dom (the_arity_of o) = dom p1 )
by A7, MSUALG_6:2;
hence B3:
len p = len p1
by FINSEQ_3:29;
FINSEQ_1:def 17 for b1 being set holds
( not 1 <= b1 or not b1 <= len p or p . b1 = p1 . b1 )
let i be
Nat;
( not 1 <= i or not i <= len p or p . i = p1 . i )
assume A9:
( 1
<= i &
i <= len p )
;
p . i = p1 . i
then B8:
i in dom p
by FINSEQ_3:25;
reconsider t =
p . i,
t1 =
p1 . i as
Element of
(Free (S,X)) by A8, A9, FUNCT_1:102, FINSEQ_3:25;
consider j being
Nat such that B2:
i = 1
+ j
by A9, NAT_1:10;
B7:
j < len p
by A9, B2, NAT_1:13;
then B4:
(
t = (o -term p) | <*j*> &
t1 = (o1 -term p1) | <*j*> )
by B2, B3, TREES_4:def 4;
then B5:
(
dom t = (dom (o -term p)) | <*j*> &
dom t1 = (dom (o1 -term p1)) | <*j*> )
by TREES_2:def 10;
(doms p) . (j + 1) = dom t
by B2, B8, FUNCT_6:def 2;
then
(
{} in (doms p) . (j + 1) &
dom (o -term p) = tree (doms p) &
len (doms p) = len p )
by TREES_3:38, TREES_4:10, TREES_1:22;
then B6:
<*j*> ^ {} in dom (o -term p)
by B7, TREES_3:48;
(doms p1) . (j + 1) = dom t1
by B2, A9, A8, FINSEQ_3:25, FUNCT_6:def 2;
then
(
{} in (doms p1) . (j + 1) &
dom (o1 -term p1) = tree (doms p1) &
len (doms p1) = len p1 )
by TREES_3:38, TREES_4:10, TREES_1:22;
then BB:
<*j*> ^ {} in dom (o1 -term p1)
by B3, B7, TREES_3:48;
BE:
t c= t1
proof
let a be
object ;
RELAT_1:def 3 for b1 being object holds
( not [a,b1] in t or [a,b1] in t1 )let b be
object ;
( not [a,b] in t or [a,b] in t1 )
assume B1:
[a,b] in t
;
[a,b] in t1
then reconsider a =
a as
Node of
t by XTUPLE_0:def 12;
t . a = b
by B1, FUNCT_1:1;
then BA:
(
(o -term p) . (<*j*> ^ a) = b &
<*j*> ^ a in dom (o -term p) )
by B4, B5, B6, TREES_1:def 6, TREES_2:def 10;
then BC:
(
(o1 -term p1) . (<*j*> ^ a) = b &
dom (o -term p) c= dom (o1 -term p1) )
by Z1, A6, GRFUNC_1:2;
then BD:
a in dom t1
by BA, BB, B5, TREES_1:def 6;
then
t1 . a = b
by BC, B4, B5, TREES_2:def 10;
hence
[a,b] in t1
by BD, FUNCT_1:1;
verum
end;
t in rng p
by B8, FUNCT_1:def 3;
hence
p . i = p1 . i
by BE, Z0;
verum
end; hence
o -term p = t1
by A6, A8, TREES_4:def 4;
verum end; end;
end;
S1[t]
from MSAFREE5:sch 2(A2, A7);
hence
t = t1
by A1; verum