reconsider D = Union F3() as non empty set ;
A5:
DTConMSA F2() = DTConstrStr(# ([:the carrier' of F1(),{the carrier of F1()}:] \/ (Union (coprod F2()))),(REL F2()) #)
by MSAFREE:def 10;
A6:
Terminals (DTConMSA F2()) = Union (coprod F2())
by MSAFREE:6;
A7: TS (DTConMSA F2()) =
union (rng (FreeSort F2()))
by MSAFREE:12
.=
Union (FreeSort F2())
by CARD_3:def 4
;
A8:
dom F2() = the carrier of F1()
by PARTFUN1:def 4;
deffunc H1( Element of (DTConMSA F2())) -> Element of Union F3() = F4((root-tree $1));
consider G being Function of the carrier of (DTConMSA F2()),(Union F3()) such that
A9:
for t being Element of (DTConMSA F2()) holds G . t = H1(t)
from FUNCT_2:sch 4();
reconsider G = G as Function of the carrier of (DTConMSA F2()),D ;
A10:
now let f be
ManySortedFunction of
FreeSort F2(),
F3();
:: thesis: ( ( for s being SortSymbol of F1()
for y being set st y in FreeGen s,F2() holds
(f . s) . y = F4(y) ) implies for t being Element of (DTConMSA F2()) st t in Terminals (DTConMSA F2()) holds
(Flatten f) . (root-tree t) = G . t )assume A11:
for
s being
SortSymbol of
F1()
for
y being
set st
y in FreeGen s,
F2() holds
(f . s) . y = F4(
y)
;
:: thesis: for t being Element of (DTConMSA F2()) st t in Terminals (DTConMSA F2()) holds
(Flatten f) . (root-tree t) = G . tlet t be
Element of
(DTConMSA F2());
:: thesis: ( t in Terminals (DTConMSA F2()) implies (Flatten f) . (root-tree t) = G . t )assume A12:
t in Terminals (DTConMSA F2())
;
:: thesis: (Flatten f) . (root-tree t) = G . tthen A13:
(
t `2 in dom F2() &
t `1 in F2()
. (t `2 ) &
t = [(t `1 ),(t `2 )] )
by A6, CARD_3:33;
reconsider s =
t `2 as
SortSymbol of
F1()
by A6, A8, A12, CARD_3:33;
A14:
root-tree [(t `1 ),s] in FreeGen s,
F2()
by A13, MSAFREE:def 17;
hence (Flatten f) . (root-tree t) =
(f . s) . (root-tree [(t `1 ),s])
by A13, Def1
.=
F4(
(root-tree t))
by A11, A13, A14
.=
G . t
by A9
;
:: thesis: verum end;
deffunc H2( Element of (DTConMSA F2()), Element of (TS (DTConMSA F2())) * , Element of (Union F3()) * ) -> Element of Union F3() = F5(($1 `1 ),$2,$3);
consider H being Function of [:the carrier of (DTConMSA F2()),((TS (DTConMSA F2())) * ),((Union F3()) * ):],(Union F3()) such that
A15:
for nt being Element of (DTConMSA F2())
for ts being Element of (TS (DTConMSA F2())) *
for x being Element of (Union F3()) * holds H . nt,ts,x = H2(nt,ts,x)
from MULTOP_1:sch 4();
reconsider H = H as Function of [:the carrier of (DTConMSA F2()),((TS (DTConMSA F2())) * ),(D * ):],D ;
A16:
now let f be
ManySortedFunction of
FreeSort F2(),
F3();
:: thesis: ( ( for o being OperSymbol of F1()
for ts being Element of Args o,(FreeMSA F2())
for x being FinSequence of D st x = (Flatten f) * ts holds
(f . (the_result_sort_of o)) . ((Den o,(FreeMSA F2())) . ts) = F5(o,ts,x) ) implies for nt being Element of (DTConMSA F2())
for ts being FinSequence of TS (DTConMSA F2()) st nt ==> roots ts holds
for x being FinSequence of D st x = (Flatten f) * ts holds
(Flatten f) . (nt -tree ts) = H . nt,ts,x )assume A17:
for
o being
OperSymbol of
F1()
for
ts being
Element of
Args o,
(FreeMSA F2()) for
x being
FinSequence of
D st
x = (Flatten f) * ts holds
(f . (the_result_sort_of o)) . ((Den o,(FreeMSA F2())) . ts) = F5(
o,
ts,
x)
;
:: thesis: for nt being Element of (DTConMSA F2())
for ts being FinSequence of TS (DTConMSA F2()) st nt ==> roots ts holds
for x being FinSequence of D st x = (Flatten f) * ts holds
(Flatten f) . (nt -tree ts) = H . nt,ts,xA18:
FreeMSA F2()
= MSAlgebra(#
(FreeSort F2()),
(FreeOper F2()) #)
by MSAFREE:def 16;
let nt be
Element of
(DTConMSA F2());
:: thesis: for ts being FinSequence of TS (DTConMSA F2()) st nt ==> roots ts holds
for x being FinSequence of D st x = (Flatten f) * ts holds
(Flatten f) . (nt -tree ts) = H . nt,ts,xlet ts be
FinSequence of
TS (DTConMSA F2());
:: thesis: ( nt ==> roots ts implies for x being FinSequence of D st x = (Flatten f) * ts holds
(Flatten f) . (nt -tree ts) = H . nt,ts,x )assume A19:
nt ==> roots ts
;
:: thesis: for x being FinSequence of D st x = (Flatten f) * ts holds
(Flatten f) . (nt -tree ts) = H . nt,ts,xthen
[nt,(roots ts)] in REL F2()
by A5, LANG1:def 1;
then
nt in [:the carrier' of F1(),{the carrier of F1()}:]
by Th2;
then consider o being
OperSymbol of
F1(),
x2 being
Element of
{the carrier of F1()} such that A20:
nt = [o,x2]
by DOMAIN_1:9;
A21:
x2 = the
carrier of
F1()
by TARSKI:def 1;
then A22:
nt = Sym o,
F2()
by A20, MSAFREE:def 11;
then A23:
ts in (((FreeSort F2()) # ) * the Arity of F1()) . o
by A19, MSAFREE:10;
let x be
FinSequence of
D;
:: thesis: ( x = (Flatten f) * ts implies (Flatten f) . (nt -tree ts) = H . nt,ts,x )assume A24:
x = (Flatten f) * ts
;
:: thesis: (Flatten f) . (nt -tree ts) = H . nt,ts,x
((FreeSort F2()) * the ResultSort of F1()) . o = (FreeSort F2()) . (the_result_sort_of o)
by FUNCT_2:21;
then A25:
(DenOp o,F2()) . ts in (FreeSort F2()) . (the_result_sort_of o)
by A23, FUNCT_2:7;
(Flatten f) . ([o,the carrier of F1()] -tree ts) =
(Flatten f) . ((DenOp o,F2()) . ts)
by A19, A20, A21, A22, MSAFREE:def 14
.=
(f . (the_result_sort_of o)) . ((DenOp o,F2()) . ts)
by A25, Def1
.=
(f . (the_result_sort_of o)) . ((Den o,(FreeMSA F2())) . ts)
by A18, MSAFREE:def 15
.=
F5(
o,
ts,
x)
by A17, A18, A23, A24
.=
F5(
(nt `1 ),
ts,
x)
by A20, MCART_1:7
;
hence
(Flatten f) . (nt -tree ts) = H . nt,
ts,
x
by A15, A20, A21;
:: thesis: verum end;
reconsider f1 = Flatten F6(), f2 = Flatten F7() as Function of (TS (DTConMSA F2())),D by A7;
deffunc H3( Element of (DTConMSA F2())) -> Element of D = G . $1;
deffunc H4( Element of (DTConMSA F2()), FinSequence of TS (DTConMSA F2()), FinSequence of D) -> Element of D = H . $1,$2,$3;
A26:
for t being Element of (DTConMSA F2()) st t in Terminals (DTConMSA F2()) holds
f1 . (root-tree t) = H3(t)
by A2, A10;
A27:
for nt being Element of (DTConMSA F2())
for ts being FinSequence of TS (DTConMSA F2()) st nt ==> roots ts holds
for x being FinSequence of D st x = f1 * ts holds
f1 . (nt -tree ts) = H4(nt,ts,x)
by A1, A16;
A28:
for t being Symbol of (DTConMSA F2()) st t in Terminals (DTConMSA F2()) holds
f2 . (root-tree t) = H3(t)
by A4, A10;
A29:
for nt being Element of (DTConMSA F2())
for ts being FinSequence of TS (DTConMSA F2()) st nt ==> roots ts holds
for x being FinSequence of D st x = f2 * ts holds
f2 . (nt -tree ts) = H4(nt,ts,x)
by A3, A16;
f1 = f2
from MSAFREE1:sch 1(A26, A27, A28, A29);
hence
F6() = F7()
by Th4; :: thesis: verum