let S be non empty non void ManySortedSign ; for A being non-empty MSAlgebra over S
for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds
e1 = e2
let A be non-empty MSAlgebra over S; for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds
e1 = e2
let V be Variables of A; for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds
e1 = e2
let t be c-Term of A,V; for f being ManySortedFunction of V, the Sorts of A
for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds
e1 = e2
let f be ManySortedFunction of V, the Sorts of A; for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds
e1 = e2
defpred S1[ c-Term of A,V] means for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of $1,f & e2 is_an_evaluation_of $1,f holds
e1 = e2;
A1:
now for s being SortSymbol of S
for v being Element of V . s holds S1[v -term A]let s be
SortSymbol of
S;
for v being Element of V . s holds S1[v -term A]let v be
Element of
V . s;
S1[v -term A]thus
S1[
v -term A]
verumproof
let e1,
e2 be
finite DecoratedTree;
( e1 is_an_evaluation_of v -term A,f & e2 is_an_evaluation_of v -term A,f implies e1 = e2 )
set t =
v -term A;
assume that A2:
e1 is_an_evaluation_of v -term A,
f
and A3:
e2 is_an_evaluation_of v -term A,
f
;
e1 = e2
A4:
dom e1 = dom (v -term A)
by A2;
A5:
{} is
Node of
e1
by TREES_1:22;
A6:
(root-tree [v,s]) . {} = [v,s]
by TREES_4:3;
then
e1 . {} = (f . s) . v
by A2, A5;
then A7:
e1 = root-tree ((f . s) . v)
by A4, TREES_4:3, TREES_4:5;
A8:
dom e2 = dom (v -term A)
by A3;
e2 . {} = (f . s) . v
by A3, A4, A6, A5;
hence
e1 = e2
by A8, A7, TREES_4:3, TREES_4:5;
verum
end; end;
A9:
now for o being OperSymbol of S
for p being ArgumentSeq of o,A,V st ( for t being c-Term of A,V st t in rng p holds
S1[t] ) holds
S1[(Sym (o,( the Sorts of A (\/) V))) -tree p]let o be
OperSymbol of
S;
for p being ArgumentSeq of o,A,V st ( for t being c-Term of A,V st t in rng p holds
S1[t] ) holds
S1[(Sym (o,( the Sorts of A (\/) V))) -tree p]let p be
ArgumentSeq of
o,
A,
V;
( ( for t being c-Term of A,V st t in rng p holds
S1[t] ) implies S1[(Sym (o,( the Sorts of A (\/) V))) -tree p] )assume A10:
for
t being
c-Term of
A,
V st
t in rng p holds
S1[
t]
;
S1[(Sym (o,( the Sorts of A (\/) V))) -tree p]thus
S1[
(Sym (o,( the Sorts of A (\/) V))) -tree p]
verumproof
set t =
(Sym (o,( the Sorts of A (\/) V))) -tree p;
let e1,
e2 be
finite DecoratedTree;
( e1 is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f & e2 is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f implies e1 = e2 )
assume that A11:
e1 is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,
f
and A12:
e2 is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,
f
;
e1 = e2
consider q1 being
DTree-yielding FinSequence such that A13:
len q1 = len p
and A14:
e1 = ((Den (o,A)) . (roots q1)) -tree q1
and A15:
for
i being
Nat for
t being
c-Term of
A,
V st
i in dom p &
t = p . i holds
ex
vt being
finite DecoratedTree st
(
vt = q1 . i &
vt is_an_evaluation_of t,
f )
by A11, Th35;
consider q2 being
DTree-yielding FinSequence such that A16:
len q2 = len p
and A17:
e2 = ((Den (o,A)) . (roots q2)) -tree q2
and A18:
for
i being
Nat for
t being
c-Term of
A,
V st
i in dom p &
t = p . i holds
ex
vt being
finite DecoratedTree st
(
vt = q2 . i &
vt is_an_evaluation_of t,
f )
by A12, Th35;
A19:
now for i being Element of NAT st i < len p holds
q1 . (i + 1) = q2 . (i + 1)let i be
Element of
NAT ;
( i < len p implies q1 . (i + 1) = q2 . (i + 1) )assume A20:
i < len p
;
q1 . (i + 1) = q2 . (i + 1)then reconsider t =
p . (i + 1) as
c-Term of
A,
V by Lm2;
A21:
ex
vt2 being
finite DecoratedTree st
(
vt2 = q2 . (i + 1) &
vt2 is_an_evaluation_of t,
f )
by A18, A20, Lm9;
ex
vt1 being
finite DecoratedTree st
(
vt1 = q1 . (i + 1) &
vt1 is_an_evaluation_of t,
f )
by A15, A20, Lm9;
hence
q1 . (i + 1) = q2 . (i + 1)
by A10, A20, A21, Lm9;
verum end;
A23:
dom q2 = Seg (len q2)
by FINSEQ_1:def 3;
dom q1 = Seg (len q1)
by FINSEQ_1:def 3;
then
q1 = q2
by A13, A16, A23, A22, FINSEQ_1:13;
hence
e1 = e2
by A14, A17;
verum
end; end;
A24:
now for s being SortSymbol of S
for x being Element of the Sorts of A . s holds S1[x -term (A,V)]let s be
SortSymbol of
S;
for x being Element of the Sorts of A . s holds S1[x -term (A,V)]let x be
Element of the
Sorts of
A . s;
S1[x -term (A,V)]thus
S1[
x -term (
A,
V)]
verumproof
let e1,
e2 be
finite DecoratedTree;
( e1 is_an_evaluation_of x -term (A,V),f & e2 is_an_evaluation_of x -term (A,V),f implies e1 = e2 )
set t =
x -term (
A,
V);
assume that A25:
e1 is_an_evaluation_of x -term (
A,
V),
f
and A26:
e2 is_an_evaluation_of x -term (
A,
V),
f
;
e1 = e2
A27:
dom e1 = dom (x -term (A,V))
by A25;
A28:
{} is
Node of
e1
by TREES_1:22;
A29:
(root-tree [x,s]) . {} = [x,s]
by TREES_4:3;
then
e1 . {} = x
by A25, A28;
then A30:
e1 = root-tree x
by A27, TREES_4:3, TREES_4:5;
A31:
dom e2 = dom (x -term (A,V))
by A26;
e2 . {} = x
by A26, A27, A29, A28;
hence
e1 = e2
by A31, A30, TREES_4:3, TREES_4:5;
verum
end; end;
for t being c-Term of A,V holds S1[t]
from MSATERM:sch 3(A24, A1, A9);
hence
for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds
e1 = e2
; verum