let S be non empty non void ManySortedSign ; for X0 being V5() countable ManySortedSet of S
for A0 being b1,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for w being ManySortedFunction of X0, the carrier of S --> NAT
for s being SortSymbol of S
for t being Element of (Free (S,X0)),s
for t1, t2 being Element of (TermAlg S),s st t1 = # (t,w) & t2 = # ((((canonical_homomorphism A0) . s) . t),w) holds
A0 |= t1 '=' t2
let X0 be V5() countable ManySortedSet of S; for A0 being X0,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for w being ManySortedFunction of X0, the carrier of S --> NAT
for s being SortSymbol of S
for t being Element of (Free (S,X0)),s
for t1, t2 being Element of (TermAlg S),s st t1 = # (t,w) & t2 = # ((((canonical_homomorphism A0) . s) . t),w) holds
A0 |= t1 '=' t2
let A0 be X0,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; for w being ManySortedFunction of X0, the carrier of S --> NAT
for s being SortSymbol of S
for t being Element of (Free (S,X0)),s
for t1, t2 being Element of (TermAlg S),s st t1 = # (t,w) & t2 = # ((((canonical_homomorphism A0) . s) . t),w) holds
A0 |= t1 '=' t2
set A = A0;
let w be ManySortedFunction of X0, the carrier of S --> NAT; for s being SortSymbol of S
for t being Element of (Free (S,X0)),s
for t1, t2 being Element of (TermAlg S),s st t1 = # (t,w) & t2 = # ((((canonical_homomorphism A0) . s) . t),w) holds
A0 |= t1 '=' t2
let s be SortSymbol of S; for t being Element of (Free (S,X0)),s
for t1, t2 being Element of (TermAlg S),s st t1 = # (t,w) & t2 = # ((((canonical_homomorphism A0) . s) . t),w) holds
A0 |= t1 '=' t2
set k = canonical_homomorphism A0;
set Y = the carrier of S --> NAT;
defpred S1[ DecoratedTree-like Function] means for s being SortSymbol of S
for t1, t2 being Element of (TermAlg S),s
for t3 being Term of S,X0 st t3 = ((canonical_homomorphism A0) . s) . $1 & t1 = # ($1,w) & t2 = # (t3,w) holds
A0 |= t1 '=' t2;
A1:
for s1 being SortSymbol of S
for v being Element of X0 . s1 holds S1[ root-tree [v,s1]]
proof
let s1 be
SortSymbol of
S;
for v being Element of X0 . s1 holds S1[ root-tree [v,s1]]let v be
Element of
X0 . s1;
S1[ root-tree [v,s1]]
set t =
root-tree [v,s1];
let s be
SortSymbol of
S;
for t1, t2 being Element of (TermAlg S),s
for t3 being Term of S,X0 st t3 = ((canonical_homomorphism A0) . s) . (root-tree [v,s1]) & t1 = # ((root-tree [v,s1]),w) & t2 = # (t3,w) holds
A0 |= t1 '=' t2let t1,
t2 be
Element of
(TermAlg S),
s;
for t3 being Term of S,X0 st t3 = ((canonical_homomorphism A0) . s) . (root-tree [v,s1]) & t1 = # ((root-tree [v,s1]),w) & t2 = # (t3,w) holds
A0 |= t1 '=' t2let t3 be
Term of
S,
X0;
( t3 = ((canonical_homomorphism A0) . s) . (root-tree [v,s1]) & t1 = # ((root-tree [v,s1]),w) & t2 = # (t3,w) implies A0 |= t1 '=' t2 )
assume A2:
t3 = ((canonical_homomorphism A0) . s) . (root-tree [v,s1])
;
( not t1 = # ((root-tree [v,s1]),w) or not t2 = # (t3,w) or A0 |= t1 '=' t2 )
assume A3:
t1 = # (
(root-tree [v,s1]),
w)
;
( not t2 = # (t3,w) or A0 |= t1 '=' t2 )
assume A4:
t2 = # (
t3,
w)
;
A0 |= t1 '=' t2
(
t1 = root-tree [((w . s1) . v),s1] &
FreeMSA ( the carrier of S --> NAT) = Free (
S,
( the carrier of S --> NAT)) )
by A3, Th57, MSAFREE3:31;
then
(
t1 in the
Sorts of
(Free (S,( the carrier of S --> NAT))) . s1 &
t1 in the
Sorts of
(Free (S,( the carrier of S --> NAT))) . s )
by MSAFREE3:4;
then
( the
Sorts of
(Free (S,( the carrier of S --> NAT))) . s1 meets the
Sorts of
(Free (S,( the carrier of S --> NAT))) . s & (
s <> s1 implies the
Sorts of
(Free (S,( the carrier of S --> NAT))) . s1 misses the
Sorts of
(Free (S,( the carrier of S --> NAT))) . s ) )
by XBOOLE_0:3, PROB_2:def 2;
then
root-tree [v,s1] is
Element of
A0,
s
by Th40;
then
t3 = root-tree [v,s1]
by A2, Th47;
hence
A0 |= t1 '=' t2
by A3, A4;
verum
end;
A5:
for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X0) st ( for t being Term of S,X0 st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S] -tree p]
proof
let o be
OperSymbol of
S;
for p being ArgumentSeq of Sym (o,X0) st ( for t being Term of S,X0 st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S] -tree p]let p be
ArgumentSeq of
Sym (
o,
X0);
( ( for t being Term of S,X0 st t in rng p holds
S1[t] ) implies S1[[o, the carrier of S] -tree p] )
assume
for
t being
Term of
S,
X0 st
t in rng p holds
S1[
t]
;
S1[[o, the carrier of S] -tree p]
set t =
[o, the carrier of S] -tree p;
let s be
SortSymbol of
S;
for t1, t2 being Element of (TermAlg S),s
for t3 being Term of S,X0 st t3 = ((canonical_homomorphism A0) . s) . ([o, the carrier of S] -tree p) & t1 = # (([o, the carrier of S] -tree p),w) & t2 = # (t3,w) holds
A0 |= t1 '=' t2let t1,
t2 be
Element of
(TermAlg S),
s;
for t3 being Term of S,X0 st t3 = ((canonical_homomorphism A0) . s) . ([o, the carrier of S] -tree p) & t1 = # (([o, the carrier of S] -tree p),w) & t2 = # (t3,w) holds
A0 |= t1 '=' t2let t3 be
Term of
S,
X0;
( t3 = ((canonical_homomorphism A0) . s) . ([o, the carrier of S] -tree p) & t1 = # (([o, the carrier of S] -tree p),w) & t2 = # (t3,w) implies A0 |= t1 '=' t2 )
assume A6:
t3 = ((canonical_homomorphism A0) . s) . ([o, the carrier of S] -tree p)
;
( not t1 = # (([o, the carrier of S] -tree p),w) or not t2 = # (t3,w) or A0 |= t1 '=' t2 )
assume A7:
t1 = # (
([o, the carrier of S] -tree p),
w)
;
( not t2 = # (t3,w) or A0 |= t1 '=' t2 )
assume A8:
t2 = # (
t3,
w)
;
A0 |= t1 '=' t2
A9:
FreeMSA X0 = Free (
S,
X0)
by MSAFREE3:31;
then reconsider a =
p as
Element of
Args (
o,
(Free (S,X0)))
by INSTALG1:1;
A10:
[o, the carrier of S] -tree p = (Den (o,(Free (S,X0)))) . a
by A9, INSTALG1:3;
t1 is
Element of the
Sorts of
(Free (S,( the carrier of S --> NAT))) . s
by MSAFREE3:31;
then reconsider tq =
t1 as
Term of
S,
( the carrier of S --> NAT) by Th42;
defpred S2[
Nat,
object ]
means for
t being
Element of
(Free (S,X0)) st
t = p . $1 holds
$2
= # (
t,
w);
A11:
dom p = Seg (len p)
by FINSEQ_1:def 3;
A12:
for
i being
Nat st
i in Seg (len p) holds
ex
x being
object st
S2[
i,
x]
consider q being
FinSequence such that A13:
(
dom q = Seg (len p) & ( for
i being
Nat st
i in Seg (len p) holds
S2[
i,
q . i] ) )
from FINSEQ_1:sch 1(A12);
(
dom q = dom p & ( for
i being
Nat for
t being
Element of
(Free (S,X0)) st
i in dom p &
t = p . i holds
q . i = # (
t,
w) ) )
by A11, A13;
then A14:
t1 = (Sym (o,( the carrier of S --> NAT))) -tree q
by A7, Th58;
then
q is
DTree-yielding
by TREES_3:24;
then
tq . {} = Sym (
o,
( the carrier of S --> NAT))
by A14, TREES_4:def 4;
then
the_sort_of tq = the_result_sort_of o
by MSATERM:17;
then
tq in FreeSort (
( the carrier of S --> NAT),
(the_result_sort_of o))
by MSATERM:def 5;
then
(
t1 in the
Sorts of
(TermAlg S) . s &
t1 in the
Sorts of
(TermAlg S) . (the_result_sort_of o) )
by MSAFREE:def 11;
then A16:
s = the_result_sort_of o
by PROB_2:def 2, XBOOLE_0:3;
reconsider tt =
[o, the carrier of S] -tree p as
Element of
(Free (S,X0)),
s by A16, A10, MSUALG_9:18;
A17:
the
Sorts of
A0 is
MSSubset of
(Free (S,X0))
by Def6;
(
((canonical_homomorphism A0) . s) . tt in the
Sorts of
A0 . s & the
Sorts of
A0 . s c= the
Sorts of
(Free (S,X0)) . s )
by A17, PBOOLE:def 2, PBOOLE:def 18;
then reconsider kt =
((canonical_homomorphism A0) . s) . tt as
Element of
(Free (S,X0)),
s ;
let h be
ManySortedFunction of
(TermAlg S),
A0;
EQUATION:def 5 ( not h is_homomorphism TermAlg S,A0 or (h . s) . ((t1 '=' t2) `1) = (h . s) . ((t1 '=' t2) `2) )
assume A18:
h is_homomorphism TermAlg S,
A0
;
(h . s) . ((t1 '=' t2) `1) = (h . s) . ((t1 '=' t2) `2)
consider hh being
ManySortedFunction of
(Free (S,X0)),
(TermAlg S) such that A19:
(
hh is_homomorphism Free (
S,
X0),
TermAlg S & ( for
s being
SortSymbol of
S for
t being
Element of
(Free (S,X0)),
s holds
# (
t,
w)
= (hh . s) . t ) )
by Th56;
A20:
(
((canonical_homomorphism A0) . s) . ((Den (o,(Free (S,X0)))) . a) in the
Sorts of
A0 . s & the
Sorts of
A0 . s c= the
Sorts of
(Free (S,X0)) . s )
by A17, PBOOLE:def 2, PBOOLE:def 18, FUNCT_2:5, A16, MSUALG_9:18;
thus (h . s) . ((t1 '=' t2) `1) =
(h . s) . ((hh . s) . tt)
by A7, A19
.=
(h . s) . ((hh . s) . ((Den (o,(Free (S,X0)))) . a))
by A9, INSTALG1:3
.=
((h . s) * (hh . s)) . ((Den (o,(Free (S,X0)))) . a)
by A16, MSUALG_9:18, FUNCT_2:15
.=
((h ** hh) . s) . ((Den (o,(Free (S,X0)))) . a)
by MSUALG_3:2
.=
((h ** hh) . s) . ((Den (o,(Free (S,X0)))) . ((canonical_homomorphism A0) # a))
by A16, Th69, A18, A19, MSUALG_3:10
.=
((h ** hh) . s) . ((Den (o,A0)) . ((canonical_homomorphism A0) # a))
by Th68, A18, A19, MSUALG_3:10, A16
.=
((h ** hh) . s) . (((canonical_homomorphism A0) . s) . ((Den (o,(Free (S,X0)))) . a))
by A16, Def10, MSUALG_3:def 7
.=
((h . s) * (hh . s)) . (((canonical_homomorphism A0) . s) . ((Den (o,(Free (S,X0)))) . a))
by MSUALG_3:2
.=
(h . s) . ((hh . s) . (((canonical_homomorphism A0) . s) . ((Den (o,(Free (S,X0)))) . a)))
by A20, FUNCT_2:15
.=
(h . s) . ((hh . s) . kt)
by A9, INSTALG1:3
.=
(h . s) . t2
by A6, A8, A19
.=
(h . s) . ((t1 '=' t2) `2)
;
verum
end;
A21:
for t being Term of S,X0 holds S1[t]
from MSATERM:sch 1(A1, A5);
let t be Element of the Sorts of (Free (S,X0)) . s; for t1, t2 being Element of (TermAlg S),s st t1 = # (t,w) & t2 = # ((((canonical_homomorphism A0) . s) . t),w) holds
A0 |= t1 '=' t2
A22:
t is Term of S,X0
by Th42;
let t1, t2 be Element of (TermAlg S),s; ( t1 = # (t,w) & t2 = # ((((canonical_homomorphism A0) . s) . t),w) implies A0 |= t1 '=' t2 )
assume A23:
t1 = # (t,w)
; ( not t2 = # ((((canonical_homomorphism A0) . s) . t),w) or A0 |= t1 '=' t2 )
assume A24:
t2 = # ((((canonical_homomorphism A0) . s) . t),w)
; A0 |= t1 '=' t2
((canonical_homomorphism A0) . s) . t is Element of the Sorts of A0 . s
;
then
((canonical_homomorphism A0) . s) . t is Term of S,X0
by Th42;
hence
A0 |= t1 '=' t2
by A22, A21, A23, A24; verum