deffunc H1( Element of S) -> Subset of ( the Sorts of (FreeOSA X) . $1) = OSFreeGen ($1,X);
set FM = FreeOSA X;
set D = DTConOSA X;
set PTA = ParsedTermsOSA X;
set SO = the Sorts of (FreeOSA X);
set NH = OSNat_Hom ((ParsedTermsOSA X),(LCongruence X));
reconsider NH1 = OSNat_Hom ((ParsedTermsOSA X),(LCongruence X)) as ManySortedFunction of (ParsedTermsOSA X),(FreeOSA X) ;
A1:
NH1 is order-sorted
by OSALG_4:15;
reconsider SOS = the Sorts of (FreeOSA X) as OrderSortedSet of S ;
consider f being Function such that
A2:
( dom f = the carrier of S & ( for s being Element of S holds f . s = H1(s) ) )
from FUNCT_1:sch 4();
reconsider f = f as ManySortedSet of the carrier of S by A2, PARTFUN1:def 2, RELAT_1:def 18;
A3:
f c= the Sorts of (FreeOSA X)
then reconsider f = f as MSSubset of (FreeOSA X) by PBOOLE:def 18;
OSCl f c= SOS
by A3, OSALG_2:8;
then
OSCl f is ManySortedSubset of the Sorts of (FreeOSA X)
by PBOOLE:def 18;
then reconsider O = OSCl f as OSSubset of FreeOSA X by OSALG_2:def 2;
O is OSSubset of GenOSAlg O
by OSALG_2:def 12;
then A4:
O c= the Sorts of (GenOSAlg O)
by PBOOLE:def 18;
f c= O
by OSALG_2:7;
then A5:
f c= the Sorts of (GenOSAlg O)
by A4, PBOOLE:13;
A6:
NH1 is_epimorphism ParsedTermsOSA X, FreeOSA X
by OSALG_4:15;
then A7:
NH1 is "onto"
;
A8:
NH1 is_homomorphism ParsedTermsOSA X, FreeOSA X
by A6;
A9:
the Sorts of (GenOSAlg O) = the Sorts of (FreeOSA X)
proof
defpred S1[
set ]
means for
s1 being
Element of
S st $1
in dom (NH1 . s1) holds
(NH1 . s1) . $1
in the
Sorts of
(GenOSAlg O) . s1;
reconsider O2 = the
Sorts of
(GenOSAlg O) as
OrderSortedSet of
S by OSALG_1:17;
the
Sorts of
(GenOSAlg O) is
MSSubset of
(FreeOSA X)
by MSUALG_2:def 9;
then A10:
the
Sorts of
(GenOSAlg O) c= the
Sorts of
(FreeOSA X)
by PBOOLE:def 18;
A11:
for
nt being
Symbol of
(DTConOSA X) for
ts being
FinSequence of
TS (DTConOSA X) st
nt ==> roots ts & ( for
t being
DecoratedTree of the
carrier of
(DTConOSA X) st
t in rng ts holds
S1[
t] ) holds
S1[
nt -tree ts]
proof
set G =
GenOSAlg O;
set OU =
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
let nt be
Symbol of
(DTConOSA X);
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConOSA X) st t in rng ts holds
S1[t] ) holds
S1[nt -tree ts]let ts be
FinSequence of
TS (DTConOSA X);
( nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConOSA X) st t in rng ts holds
S1[t] ) implies S1[nt -tree ts] )
assume that A12:
nt ==> roots ts
and A13:
for
t being
DecoratedTree of the
carrier of
(DTConOSA X) st
t in rng ts holds
S1[
t]
;
S1[nt -tree ts]
[nt,(roots ts)] in the
Rules of
(DTConOSA X)
by A12, LANG1:def 1;
then reconsider rt =
roots ts as
Element of
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by ZFMISC_1:87;
reconsider sy =
nt as
Element of
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) ;
[sy,rt] in OSREL X
by A12, LANG1:def 1;
then
sy in [: the carrier' of S,{ the carrier of S}:]
by Def4;
then consider o being
Element of the
carrier' of
S,
x2 being
Element of
{ the carrier of S} such that A14:
sy = [o,x2]
by DOMAIN_1:1;
let s1 be
Element of
S;
( nt -tree ts in dom (NH1 . s1) implies (NH1 . s1) . (nt -tree ts) in the Sorts of (GenOSAlg O) . s1 )
assume
nt -tree ts in dom (NH1 . s1)
;
(NH1 . s1) . (nt -tree ts) in the Sorts of (GenOSAlg O) . s1
then
nt -tree ts in the
Sorts of
(ParsedTermsOSA X) . s1
;
then
nt -tree ts in ParsedTerms (
X,
s1)
by Def8;
then consider a1 being
Element of
TS (DTConOSA X) such that A15:
nt -tree ts = a1
and A16:
( ex
s2 being
Element of
S ex
x being
object st
(
s2 <= s1 &
x in X . s2 &
a1 = root-tree [x,s2] ) or ex
o being
OperSymbol of
S st
(
[o, the carrier of S] = a1 . {} &
the_result_sort_of o <= s1 ) )
;
A17:
Seg (len rt) = dom rt
by FINSEQ_1:def 3;
A18:
x2 = the
carrier of
S
by TARSKI:def 1;
for
s2 being
Element of
S for
x being
set holds
( not
s2 <= s1 or not
x in X . s2 or not
a1 = root-tree [x,s2] )
then consider o1 being
OperSymbol of
S such that A20:
[o1, the carrier of S] = a1 . {}
and A21:
the_result_sort_of o1 <= s1
by A16;
set ar =
the_arity_of o;
set rs =
the_result_sort_of o;
A22:
dom (roots ts) = dom ts
by TREES_3:def 18;
[nt,(roots ts)] in OSREL X
by A12, LANG1:def 1;
then A23:
len rt = len (the_arity_of o)
by A14, A18, Th2;
A24:
Seg (len (the_arity_of o)) = dom (the_arity_of o)
by FINSEQ_1:def 3;
reconsider B = the
Sorts of
(GenOSAlg O) as
MSSubset of
(FreeOSA X) by MSUALG_2:def 9;
A25:
dom (B * (the_arity_of o)) = dom (the_arity_of o)
by PARTFUN1:def 2;
set AR = the
Arity of
S;
set RS = the
ResultSort of
S;
set BH =
(B #) * the
Arity of
S;
the
Arity of
S . o = the_arity_of o
by MSUALG_1:def 1;
then A26:
((B #) * the Arity of S) . o = product (B * (the_arity_of o))
by MSAFREE:1;
reconsider rs1 =
the_result_sort_of o,
s11 =
s1 as
Element of
S ;
reconsider B1 =
B as
OrderSortedSet of
S by OSALG_1:17;
A27:
the
ResultSort of
S . o = the_result_sort_of o
by MSUALG_1:def 2;
B is
opers_closed
by MSUALG_2:def 9;
then
B is_closed_on o
by MSUALG_2:def 6;
then A28:
rng ((Den (o,(FreeOSA X))) | (((B #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o
by MSUALG_2:def 5;
A29:
OSSym (
o,
X)
= [o, the carrier of S]
;
A30:
nt = [o, the carrier of S]
by A14, TARSKI:def 1;
then A31:
ts in (((ParsedTerms X) #) * the Arity of S) . o
by A12, A29, Th7;
then reconsider ts1 =
ts as
Element of
Args (
o,
(ParsedTermsOSA X))
by MSUALG_1:def 4;
Den (
o,
(ParsedTermsOSA X)) =
(PTOper X) . o
by MSUALG_1:def 6
.=
PTDenOp (
o,
X)
by Def10
;
then A32:
(Den (o,(ParsedTermsOSA X))) . ts = nt -tree ts
by A12, A29, A30, Def9;
A33:
dom ( the Sorts of (ParsedTermsOSA X) * (the_arity_of o)) = dom (the_arity_of o)
by PARTFUN1:def 2;
A34:
for
x being
object st
x in dom (B * (the_arity_of o)) holds
(NH1 # ts1) . x in (B * (the_arity_of o)) . x
proof
let x be
object ;
( x in dom (B * (the_arity_of o)) implies (NH1 # ts1) . x in (B * (the_arity_of o)) . x )
assume A35:
x in dom (B * (the_arity_of o))
;
(NH1 # ts1) . x in (B * (the_arity_of o)) . x
reconsider x1 =
x as
Nat by A35;
A36:
ts . x1 in rng ts
by A25, A22, A23, A17, A24, A35, FUNCT_1:def 3;
rng ts c= TS (DTConOSA X)
by FINSEQ_1:def 4;
then reconsider t =
ts . x as
Element of
TS (DTConOSA X) by A36;
ts1 . x in ( the Sorts of (ParsedTermsOSA X) * (the_arity_of o)) . x
by A25, A33, A35, MSUALG_3:6;
then
ts1 . x in the
Sorts of
(ParsedTermsOSA X) . ((the_arity_of o) . x)
by A25, A33, A35, FUNCT_1:12;
then
ts1 . x in the
Sorts of
(ParsedTermsOSA X) . ((the_arity_of o) /. x)
by A25, A35, PARTFUN1:def 6;
then
ts1 . x1 in dom (NH1 . ((the_arity_of o) /. x1))
by FUNCT_2:def 1;
then
(NH1 . ((the_arity_of o) /. x1)) . t in the
Sorts of
(GenOSAlg O) . ((the_arity_of o) /. x1)
by A13, A36;
then A37:
(NH1 . ((the_arity_of o) /. x1)) . (ts1 . x1) in B . ((the_arity_of o) . x)
by A25, A35, PARTFUN1:def 6;
(NH1 # ts1) . x1 = (NH1 . ((the_arity_of o) /. x1)) . (ts1 . x1)
by A25, A22, A23, A17, A24, A35, MSUALG_3:def 6;
hence
(NH1 # ts1) . x in (B * (the_arity_of o)) . x
by A35, A37, FUNCT_1:12;
verum
end;
NH1 # ts1 in Args (
o,
(FreeOSA X))
;
then A38:
NH1 # ts1 in dom (Den (o,(FreeOSA X)))
by FUNCT_2:def 1;
[o1, the carrier of S] = [o,x2]
by A14, A15, A20, TREES_4:def 4;
then A39:
o1 = o
by XTUPLE_0:1;
then A40:
B1 . rs1 c= B1 . s11
by A21, OSALG_1:def 16;
dom (NH1 # ts1) = dom (the_arity_of o)
by MSUALG_3:6;
then
NH1 # ts1 in ((B #) * the Arity of S) . o
by A26, A25, A34, CARD_3:9;
then
(Den (o,(FreeOSA X))) . (NH1 # ts1) in rng ((Den (o,(FreeOSA X))) | (((B #) * the Arity of S) . o))
by A38, FUNCT_1:50;
then A41:
(Den (o,(FreeOSA X))) . (NH1 # ts1) in (B * the ResultSort of S) . o
by A28;
ts in Args (
o,
(ParsedTermsOSA X))
by A31, MSUALG_1:def 4;
then
(Den (o,(ParsedTermsOSA X))) . ts in Result (
o,
(ParsedTermsOSA X))
by FUNCT_2:5;
then
(Den (o,(ParsedTermsOSA X))) . ts in ( the Sorts of (ParsedTermsOSA X) * the ResultSort of S) . o
by MSUALG_1:def 5;
then
(Den (o,(ParsedTermsOSA X))) . ts in the
Sorts of
(ParsedTermsOSA X) . (the_result_sort_of o)
by A27, FUNCT_2:15;
then
nt -tree ts in dom (NH1 . (the_result_sort_of o))
by A32, FUNCT_2:def 1;
then A42:
(NH1 . s11) . (nt -tree ts) = (NH1 . rs1) . (nt -tree ts)
by A1, A21, A39;
(NH1 . (the_result_sort_of o)) . ((Den (o,(ParsedTermsOSA X))) . ts1) = (Den (o,(FreeOSA X))) . (NH1 # ts1)
by A8;
then
(NH1 . (the_result_sort_of o)) . (nt -tree ts) in B . (the_result_sort_of o)
by A27, A32, A41, FUNCT_2:15;
hence
(NH1 . s1) . (nt -tree ts) in the
Sorts of
(GenOSAlg O) . s1
by A40, A42;
verum
end;
let x be
Element of
S;
PBOOLE:def 21 the Sorts of (GenOSAlg O) . x = the Sorts of (FreeOSA X) . x
set s =
x;
A43:
for
s being
Symbol of
(DTConOSA X) st
s in Terminals (DTConOSA X) holds
S1[
root-tree s]
proof
let t be
Symbol of
(DTConOSA X);
( t in Terminals (DTConOSA X) implies S1[ root-tree t] )
assume A44:
t in Terminals (DTConOSA X)
;
S1[ root-tree t]
let s1 be
Element of
S;
( root-tree t in dom (NH1 . s1) implies (NH1 . s1) . (root-tree t) in the Sorts of (GenOSAlg O) . s1 )
assume
root-tree t in dom (NH1 . s1)
;
(NH1 . s1) . (root-tree t) in the Sorts of (GenOSAlg O) . s1
then
root-tree t in the
Sorts of
(ParsedTermsOSA X) . s1
;
then
root-tree t in ParsedTerms (
X,
s1)
by Def8;
then consider a being
Element of
TS (DTConOSA X) such that A45:
root-tree t = a
and A46:
( ex
s2 being
Element of
S ex
x being
object st
(
s2 <= s1 &
x in X . s2 &
a = root-tree [x,s2] ) or ex
o being
OperSymbol of
S st
(
[o, the carrier of S] = a . {} &
the_result_sort_of o <= s1 ) )
;
for
o being
OperSymbol of
S holds
( not
[o, the carrier of S] = a . {} or not
the_result_sort_of o <= s1 )
then consider s2 being
Element of
S,
x being
set such that A49:
s2 <= s1
and A50:
x in X . s2
and A51:
a = root-tree [x,s2]
by A46;
reconsider s11 =
s1,
s21 =
s2 as
Element of
S ;
a in ParsedTerms (
X,
s2)
by A50, A51;
then
a in (ParsedTerms X) . s2
by Def8;
then
root-tree [x,s2] in dom (NH1 . s2)
by A51, FUNCT_2:def 1;
then A52:
(NH1 . s21) . (root-tree [x,s2]) = (NH1 . s11) . (root-tree [x,s2])
by A1, A49;
f . s2 c= the
Sorts of
(GenOSAlg O) . s2
by A5;
then A53:
OSFreeGen (
s2,
X)
c= the
Sorts of
(GenOSAlg O) . s2
by A2;
O2 . s21 c= O2 . s11
by A49, OSALG_1:def 16;
then A54:
OSFreeGen (
s2,
X)
c= the
Sorts of
(GenOSAlg O) . s1
by A53;
(NH1 . s2) . (root-tree [x,s2]) in OSFreeGen (
s2,
X)
by A50, Def25;
hence
(NH1 . s1) . (root-tree t) in the
Sorts of
(GenOSAlg O) . s1
by A45, A51, A52, A54;
verum
end;
A55:
for
t being
DecoratedTree of the
carrier of
(DTConOSA X) st
t in TS (DTConOSA X) holds
S1[
t]
from DTCONSTR:sch 7(A43, A11);
thus
the
Sorts of
(GenOSAlg O) . x c= the
Sorts of
(FreeOSA X) . x
by A10;
XBOOLE_0:def 10 the Sorts of (FreeOSA X) . x c= the Sorts of (GenOSAlg O) . x
let x1 be
object ;
TARSKI:def 3 ( not x1 in the Sorts of (FreeOSA X) . x or x1 in the Sorts of (GenOSAlg O) . x )
assume A56:
x1 in the
Sorts of
(FreeOSA X) . x
;
x1 in the Sorts of (GenOSAlg O) . x
A57: the
Sorts of
(ParsedTermsOSA X) . x =
ParsedTerms (
X,
x)
by Def8
.=
{ a where a is Element of TS (DTConOSA X) : ( ex s2 being Element of S ex x being object st
( s2 <= x & x in X . s2 & a = root-tree [x,s2] ) or ex o1 being OperSymbol of S st
( [o1, the carrier of S] = a . {} & the_result_sort_of o1 <= x ) ) }
;
rng (NH1 . x) = the
Sorts of
(FreeOSA X) . x
by A7;
then consider x2 being
object such that A58:
x2 in dom (NH1 . x)
and A59:
x1 = (NH1 . x) . x2
by A56, FUNCT_1:def 3;
x2 in the
Sorts of
(ParsedTermsOSA X) . x
by A58;
then
ex
a being
Element of
TS (DTConOSA X) st
(
a = x2 & ( ex
s2 being
Element of
S ex
x being
object st
(
s2 <= x &
x in X . s2 &
a = root-tree [x,s2] ) or ex
o1 being
OperSymbol of
S st
(
[o1, the carrier of S] = a . {} &
the_result_sort_of o1 <= x ) ) )
by A57;
hence
x1 in the
Sorts of
(GenOSAlg O) . x
by A55, A58, A59;
verum
end;
f is OSGeneratorSet of FreeOSA X
then reconsider f = f as OSGeneratorSet of FreeOSA X ;
take
f
; for s being Element of S holds f . s = OSFreeGen (s,X)
thus
for s being Element of S holds f . s = OSFreeGen (s,X)
by A2; verum