let S be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: 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; :: thesis: { 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 ;
:: according to TARSKI:def 3 :: thesis: ( 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 }
;
:: thesis: 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 &
depth t = 0 )
;
consider dt being
finite DecoratedTree,
ft being
finite Tree such that A3:
(
dt = t &
ft = dom dt &
depth t = height ft )
by MSAFREE2:def 14;
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 & ( 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 ) ) )
;
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 A4;
suppose
ex
o being
OperSymbol of
S st
(
[o,the carrier of S] = a . {} &
the_result_sort_of o = v )
;
:: thesis: x in (FreeGen v,X) \/ (Constants (FreeMSA X),v)then consider o being
OperSymbol of
S such that A6:
(
[o,the carrier of S] = a . {} &
the_result_sort_of o = v )
;
reconsider t' =
t as
Term of
S,
X by A4, MSATERM:def 1;
consider ars being
ArgumentSeq of
Sym o,
X such that A7:
t' = [o,the carrier of S] -tree ars
by A4, A6, MSATERM:10;
dt = root-tree (dt . {} )
by A2, A3, TREES_1:80, TREES_4:5;
then A8:
ars = {}
by A3, A7, TREES_4:17;
then 0 =
len ars
.=
len (the_arity_of o)
by MSATERM:22
;
then
the_arity_of o = {}
;
then A9:
the
Arity of
S . o = {}
by MSUALG_1:def 6;
A10:
the
ResultSort of
S . o = v
by A6, MSUALG_1:def 7;
A11:
Den o,
(FreeMSA X) =
(FreeOper X) . o
by MSUALG_1:def 11
.=
DenOp o,
X
by MSAFREE:def 15
;
A12:
Sym o,
X ==> roots ars
by MSATERM:21;
set ars' =
<*> (TS (DTConMSA X));
A13:
(DenOp o,X) . (<*> (TS (DTConMSA X))) = t
by A7, A8, A12, MSAFREE:def 14;
dom (Den o,(FreeMSA X)) = {{} }
by A9, Th25;
then
{} in dom (Den o,(FreeMSA X))
by TARSKI:def 1;
then A14:
t in rng (Den o,(FreeMSA X))
by A11, A13, FUNCT_1:def 5;
consider Av being non
empty set such that A15:
(
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;
t in Constants (FreeMSA X),
v
by A9, A10, A14, A15;
hence
x in (FreeGen v,X) \/ (Constants (FreeMSA X),v)
by A2, XBOOLE_0:def 3;
:: thesis: verum end;
end;
A16:
FreeGen v,X c= { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 }
Constants (FreeMSA X),v c= { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 }
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( 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 } )
assume A20:
x in Constants (FreeMSA X),
v
;
:: thesis: 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 A21:
(
Av = the
Sorts of
(FreeMSA X) . v &
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;
consider a being
Element of
Av such that A22:
(
x = a & 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 A20, A21;
consider o being
OperSymbol of
S such that A23:
( the
Arity of
S . o = {} & the
ResultSort of
S . o = v &
a in rng (Den o,(FreeMSA X)) )
by A22;
reconsider a =
a as
Element of the
Sorts of
(FreeMSA X) . v by A21;
consider dt being
finite DecoratedTree,
t being
finite Tree such that A24:
(
dt = a &
t = dom dt &
depth a = height t )
by MSAFREE2:def 14;
A25:
dom (Den o,(FreeMSA X)) = {{} }
by A23, Th25;
consider d being
set such that A26:
(
d in dom (Den o,(FreeMSA X)) &
a = (Den o,(FreeMSA X)) . d )
by A23, FUNCT_1:def 5;
A27:
d = {}
by A25, A26, TARSKI:def 1;
A28:
Den o,
(FreeMSA X) =
(FreeOper X) . o
by MSUALG_1:def 11
.=
DenOp o,
X
by MSAFREE:def 15
;
set p =
<*> (TS (DTConMSA X));
(((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 A25, TARSKI:def 1;
then
Sym o,
X ==> roots (<*> (TS (DTConMSA X)))
by MSAFREE:10;
then
(DenOp o,X) . (<*> (TS (DTConMSA X))) = (Sym o,X) -tree (<*> (TS (DTConMSA X)))
by MSAFREE:def 14;
then
a = root-tree (Sym o,X)
by A26, A27, A28, TREES_4:20;
then
height t = 0
by A24, 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 A22, A24;
:: thesis: verum
end;
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 A16, 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; :: thesis: verum