let S be non void Signature; for X being non-empty ManySortedSet of the carrier of S
for A being MSSubset of (FreeMSA X) holds
( A is opers_closed iff for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st rng p c= Union A holds
(Sym (o,X)) -tree p in A . (the_result_sort_of o) )
let X be non-empty ManySortedSet of the carrier of S; for A being MSSubset of (FreeMSA X) holds
( A is opers_closed iff for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st rng p c= Union A holds
(Sym (o,X)) -tree p in A . (the_result_sort_of o) )
set A = FreeMSA X;
let T be MSSubset of (FreeMSA X); ( T is opers_closed iff for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st rng p c= Union T holds
(Sym (o,X)) -tree p in T . (the_result_sort_of o) )
hereby ( ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st rng p c= Union T holds
(Sym (o,X)) -tree p in T . (the_result_sort_of o) ) implies T is opers_closed )
assume A1:
T is
opers_closed
;
for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st rng p c= Union T holds
(Sym (o,X)) -tree p in T . (the_result_sort_of o)let o be
OperSymbol of
S;
for p being ArgumentSeq of Sym (o,X) st rng p c= Union T holds
(Sym (o,X)) -tree p in T . (the_result_sort_of o)let p be
ArgumentSeq of
Sym (
o,
X);
( rng p c= Union T implies (Sym (o,X)) -tree p in T . (the_result_sort_of o) )
T is_closed_on o
by A1;
then A2:
rng ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) c= (T * the ResultSort of S) . o
;
A3:
p is
Element of
Args (
o,
(FreeMSA X))
by INSTALG1:1;
A4:
dom p = dom (the_arity_of o)
by MSATERM:22;
A5:
dom T = the
carrier of
S
by PARTFUN1:def 2;
assume A6:
rng p c= Union T
;
(Sym (o,X)) -tree p in T . (the_result_sort_of o)A7:
now for x being object st x in dom (the_arity_of o) holds
p . x in (T * (the_arity_of o)) . xlet x be
object ;
( x in dom (the_arity_of o) implies p . x in (T * (the_arity_of o)) . x )assume A8:
x in dom (the_arity_of o)
;
p . x in (T * (the_arity_of o)) . xthen reconsider i =
x as
Nat ;
reconsider t =
p . i as
Term of
S,
X by A4, A8, MSATERM:22;
A9:
(
the_sort_of t = (the_arity_of o) . x &
(T * (the_arity_of o)) . x = T . ((the_arity_of o) . x) )
by A4, A8, FUNCT_1:13, MSATERM:23;
p . x in rng p
by A4, A8, FUNCT_1:def 3;
then consider y being
object such that A10:
y in dom T
and A11:
p . x in T . y
by A6, CARD_5:2;
T c= the
Sorts of
(FreeMSA X)
by PBOOLE:def 18;
then
T . y c= the
Sorts of
(FreeMSA X) . y
by A10;
hence
p . x in (T * (the_arity_of o)) . x
by A10, A11, A9, Th7;
verum end;
rng (the_arity_of o) c= dom T
by A5;
then
dom (T * (the_arity_of o)) = dom (the_arity_of o)
by RELAT_1:27;
then A12:
p in product (T * (the_arity_of o))
by A4, A7, CARD_3:9;
A13:
((T #) * the Arity of S) . o =
(T #) . ( the Arity of S . o)
by FUNCT_2:15
.=
(T #) . (the_arity_of o)
by MSUALG_1:def 1
.=
product (T * (the_arity_of o))
by FINSEQ_2:def 5
;
then A14:
((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) . p = (Den (o,(FreeMSA X))) . p
by A12, FUNCT_1:49;
dom (Den (o,(FreeMSA X))) = Args (
o,
(FreeMSA X))
by FUNCT_2:def 1;
then
p in dom ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o))
by A13, A3, A12, RELAT_1:57;
then A15:
(Den (o,(FreeMSA X))) . p in rng ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o))
by A14, FUNCT_1:def 3;
(T * the ResultSort of S) . o =
T . ( the ResultSort of S . o)
by FUNCT_2:15
.=
T . (the_result_sort_of o)
by MSUALG_1:def 2
;
then
(
[o, the carrier of S] = Sym (
o,
X) &
(Den (o,(FreeMSA X))) . p in T . (the_result_sort_of o) )
by A2, A15, MSAFREE:def 9;
hence
(Sym (o,X)) -tree p in T . (the_result_sort_of o)
by A3, INSTALG1:3;
verum
end;
assume A16:
for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st rng p c= Union T holds
(Sym (o,X)) -tree p in T . (the_result_sort_of o)
; T is opers_closed
let o be OperSymbol of S; MSUALG_2:def 6 T is_closed_on o
let x be object ; TARSKI:def 3,MSUALG_2:def 5 ( not x in proj2 ((Den (o,(FreeMSA X))) | (( the Arity of S * (T #)) . o)) or x in ( the ResultSort of S * T) . o )
A17: (T * the ResultSort of S) . o =
T . ( the ResultSort of S . o)
by FUNCT_2:15
.=
T . (the_result_sort_of o)
by MSUALG_1:def 2
;
assume
x in rng ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o))
; x in ( the ResultSort of S * T) . o
then consider y being object such that
A18:
y in dom ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o))
and
A19:
x = ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) . y
by FUNCT_1:def 3;
y in dom (Den (o,(FreeMSA X)))
by A18, RELAT_1:57;
then reconsider y = y as Element of Args (o,(FreeMSA X)) ;
reconsider p = y as ArgumentSeq of Sym (o,X) by INSTALG1:1;
A20: ((T #) * the Arity of S) . o =
(T #) . ( the Arity of S . o)
by FUNCT_2:15
.=
(T #) . (the_arity_of o)
by MSUALG_1:def 1
.=
product (T * (the_arity_of o))
by FINSEQ_2:def 5
;
A21:
rng p c= Union T
proof
let z be
object ;
TARSKI:def 3 ( not z in rng p or z in Union T )
A22:
dom T = the
carrier of
S
by PARTFUN1:def 2;
assume
z in rng p
;
z in Union T
then consider a being
object such that A23:
a in dom p
and A24:
z = p . a
by FUNCT_1:def 3;
A25:
dom p = dom (T * (the_arity_of o))
by A18, A20, CARD_3:9;
then A26:
(
z in (T * (the_arity_of o)) . a &
(T * (the_arity_of o)) . a = T . ((the_arity_of o) . a) )
by A18, A20, A23, A24, CARD_3:9, FUNCT_1:12;
rng (the_arity_of o) c= the
carrier of
S
;
then
dom (T * (the_arity_of o)) = dom (the_arity_of o)
by A22, RELAT_1:27;
then
(the_arity_of o) . a in rng (the_arity_of o)
by A23, A25, FUNCT_1:def 3;
hence
z in Union T
by A22, A26, CARD_5:2;
verum
end;
x =
(Den (o,(FreeMSA X))) . y
by A18, A19, FUNCT_1:47
.=
[o, the carrier of S] -tree y
by INSTALG1:3
.=
(Sym (o,X)) -tree p
by MSAFREE:def 9
;
hence
x in ( the ResultSort of S * T) . o
by A16, A17, A21; verum