let S be non empty non void ManySortedSign ; for X being V2() ManySortedSet of the carrier of S
for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } = (FreeGen v,X) \/ (Constants (FreeMSA X),v)
let X be V2() ManySortedSet of the carrier of S; for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } = (FreeGen v,X) \/ (Constants (FreeMSA X),v)
let v be SortSymbol of S; { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } = (FreeGen v,X) \/ (Constants (FreeMSA X),v)
set SF = the Sorts of (FreeMSA X);
set d0 = { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } ;
A1:
{ t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } c= (FreeGen v,X) \/ (Constants (FreeMSA X),v)
proof
let x be
set ;
TARSKI:def 3 ( not x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } or x in (FreeGen v,X) \/ (Constants (FreeMSA X),v) )
assume
x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 }
;
x in (FreeGen v,X) \/ (Constants (FreeMSA X),v)
then consider t being
Element of the
Sorts of
(FreeMSA X) . v such that A2:
x = t
and A3:
depth t = 0
;
t in the
Sorts of
(FreeMSA X) . v
;
then
t in FreeSort X,
v
by MSAFREE:def 13;
then consider a being
Element of
TS (DTConMSA X) such that A4:
t = a
and A5:
( ex
x being
set st
(
x in X . v &
a = root-tree [x,v] ) or ex
o being
OperSymbol of
S st
(
[o,the carrier of S] = a . {} &
the_result_sort_of o = v ) )
;
consider dt being
finite DecoratedTree,
ft being
finite Tree such that A6:
dt = t
and A7:
(
ft = dom dt &
depth t = height ft )
by MSAFREE2:def 14;
per cases
( ex x being set st
( x in X . v & a = root-tree [x,v] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a . {} & the_result_sort_of o = v ) )
by A5;
suppose
ex
o being
OperSymbol of
S st
(
[o,the carrier of S] = a . {} &
the_result_sort_of o = v )
;
x in (FreeGen v,X) \/ (Constants (FreeMSA X),v)then consider o being
OperSymbol of
S such that A8:
[o,the carrier of S] = a . {}
and A9:
the_result_sort_of o = v
;
A10:
the
ResultSort of
S . o = v
by A9, MSUALG_1:def 7;
set ars9 =
<*> (TS (DTConMSA X));
reconsider t9 =
t as
Term of
S,
X by A4, MSATERM:def 1;
A11:
ex
Av being non
empty set st
(
Av = the
Sorts of
(FreeMSA X) . v &
Constants (FreeMSA X),
v = { a1 where a1 is Element of Av : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = v & a1 in rng (Den o,(FreeMSA X)) ) } )
by MSUALG_2:def 4;
consider ars being
ArgumentSeq of
Sym o,
X such that A12:
t9 = [o,the carrier of S] -tree ars
by A4, A8, MSATERM:10;
dt = root-tree (dt . {} )
by A3, A7, TREES_1:80, TREES_4:5;
then A13:
ars = {}
by A6, A12, TREES_4:17;
then 0 =
len ars
.=
len (the_arity_of o)
by MSATERM:22
;
then
the_arity_of o = {}
;
then A14:
the
Arity of
S . o = {}
by MSUALG_1:def 6;
then
dom (Den o,(FreeMSA X)) = {{} }
by Th25;
then A15:
{} in dom (Den o,(FreeMSA X))
by TARSKI:def 1;
Sym o,
X ==> roots ars
by MSATERM:21;
then A16:
(DenOp o,X) . (<*> (TS (DTConMSA X))) = t
by A12, A13, MSAFREE:def 14;
Den o,
(FreeMSA X) =
(FreeOper X) . o
by MSUALG_1:def 11
.=
DenOp o,
X
by MSAFREE:def 15
;
then
t in rng (Den o,(FreeMSA X))
by A16, A15, FUNCT_1:def 5;
then
t in Constants (FreeMSA X),
v
by A14, A10, A11;
hence
x in (FreeGen v,X) \/ (Constants (FreeMSA X),v)
by A2, XBOOLE_0:def 3;
verum end;
end;
A17:
Constants (FreeMSA X),v c= { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 }
proof
set p =
<*> (TS (DTConMSA X));
let x be
set ;
TARSKI:def 3 ( not x in Constants (FreeMSA X),v or x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } )
consider Av being non
empty set such that A18:
Av = the
Sorts of
(FreeMSA X) . v
and A19:
Constants (FreeMSA X),
v = { a where a is Element of Av : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = v & a in rng (Den o,(FreeMSA X)) ) }
by MSUALG_2:def 4;
assume
x in Constants (FreeMSA X),
v
;
x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 }
then consider a being
Element of
Av such that A20:
x = a
and A21:
ex
o being
OperSymbol of
S st
( the
Arity of
S . o = {} & the
ResultSort of
S . o = v &
a in rng (Den o,(FreeMSA X)) )
by A19;
consider o being
OperSymbol of
S such that A22:
the
Arity of
S . o = {}
and
the
ResultSort of
S . o = v
and A23:
a in rng (Den o,(FreeMSA X))
by A21;
A24:
dom (Den o,(FreeMSA X)) = {{} }
by A22, Th25;
(((FreeSort X) # ) * the Arity of S) . o =
Args o,
(FreeMSA X)
by MSUALG_1:def 9
.=
dom (Den o,(FreeMSA X))
by FUNCT_2:def 1
;
then
<*> (TS (DTConMSA X)) in (((FreeSort X) # ) * the Arity of S) . o
by A24, TARSKI:def 1;
then
Sym o,
X ==> roots (<*> (TS (DTConMSA X)))
by MSAFREE:10;
then A25:
(DenOp o,X) . (<*> (TS (DTConMSA X))) = (Sym o,X) -tree (<*> (TS (DTConMSA X)))
by MSAFREE:def 14;
reconsider a =
a as
Element of the
Sorts of
(FreeMSA X) . v by A18;
consider d being
set such that A26:
d in dom (Den o,(FreeMSA X))
and A27:
a = (Den o,(FreeMSA X)) . d
by A23, FUNCT_1:def 5;
consider dt being
finite DecoratedTree,
t being
finite Tree such that A28:
(
dt = a &
t = dom dt )
and A29:
depth a = height t
by MSAFREE2:def 14;
A30:
Den o,
(FreeMSA X) =
(FreeOper X) . o
by MSUALG_1:def 11
.=
DenOp o,
X
by MSAFREE:def 15
;
d = {}
by A24, A26, TARSKI:def 1;
then
a = root-tree (Sym o,X)
by A27, A30, A25, TREES_4:20;
then
height t = 0
by A28, TREES_1:79, TREES_4:3;
hence
x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 }
by A20, A29;
verum
end;
FreeGen v,X c= { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 }
then
(FreeGen v,X) \/ (Constants (FreeMSA X),v) c= { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 }
by A17, XBOOLE_1:8;
hence
{ t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } = (FreeGen v,X) \/ (Constants (FreeMSA X),v)
by A1, XBOOLE_0:def 10; verum