let S be non empty non void ManySortedSign ; for X being non-empty 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 non-empty 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
object ;
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 11;
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 2;
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 3;
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:43, 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 1;
then
dom (Den (o,(FreeMSA X))) = {{}}
by Th23;
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 12;
Den (
o,
(FreeMSA X)) =
(FreeOper X) . o
by MSUALG_1:def 6
.=
DenOp (
o,
X)
by MSAFREE:def 13
;
then
t in rng (Den (o,(FreeMSA X)))
by A16, A15, FUNCT_1:def 3;
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
object ;
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 3;
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, Th23;
(((FreeSort X) #) * the Arity of S) . o =
Args (
o,
(FreeMSA X))
by MSUALG_1:def 4
.=
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 12;
reconsider a =
a as
Element of the
Sorts of
(FreeMSA X) . v by A18;
consider d being
object such that A26:
d in dom (Den (o,(FreeMSA X)))
and A27:
a = (Den (o,(FreeMSA X))) . d
by A23, FUNCT_1:def 3;
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 6
.=
DenOp (
o,
X)
by MSAFREE:def 13
;
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:42, 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