{} in {{} } *
by FINSEQ_1:66;
then reconsider f = {[{} ,{{} }]} --> {} as Function of {[{} ,{{} }]},({{} } * ) by FUNCOP_1:58;
reconsider g = {[{} ,{{} }]} --> {} as Function of {[{} ,{{} }]},{{} } ;
take S = ManySortedSign(# {{} },{[{} ,{{} }]},f,g #); :: thesis: ( not S is void & S is finite & S is monotonic & S is Circuit-like )
thus
not S is void
; :: thesis: ( S is finite & S is monotonic & S is Circuit-like )
thus
S is finite
; :: thesis: ( S is monotonic & S is Circuit-like )
thus
S is monotonic
:: thesis: S is Circuit-like proof
let A be
non-empty finitely-generated MSAlgebra of
S;
:: according to MSAFREE2:def 13 :: thesis: A is finite-yielding
reconsider S' =
S as non
empty non
void ManySortedSign ;
reconsider A' =
A as
non-empty MSAlgebra of
S' ;
consider G being
GeneratorSet of
A' such that A1:
G is
finite-yielding
by Def10;
consider s being
SortSymbol of
S';
A2:
s = {}
by TARSKI:def 1;
consider o being
OperSymbol of
S';
A3:
o = [{} ,{{} }]
by TARSKI:def 1;
A4:
Args o,
A' =
(the Sorts of A' # ) . (the Arity of S . o)
by FUNCT_2:21
.=
(the Sorts of A' # ) . (<*> the carrier of S')
by FUNCOP_1:13
.=
{{} }
by PRE_CIRC:5
;
then A5:
dom (Den o,A') = {{} }
by FUNCT_2:def 1;
A6:
Result o,
A' =
the
Sorts of
A' . (the ResultSort of S . o)
by FUNCT_2:21
.=
the
Sorts of
A' . {}
by FUNCOP_1:13
;
set T =
s .--> ((G . s) \/ {((Den o,A') . {} )});
dom (s .--> ((G . s) \/ {((Den o,A') . {} )})) = the
carrier of
S
by A2, FUNCOP_1:19;
then reconsider T =
s .--> ((G . s) \/ {((Den o,A') . {} )}) as
V5()
ManySortedSet of
by PARTFUN1:def 4, RELAT_1:def 18;
set O =
o .--> (Den o,A');
dom (o .--> (Den o,A')) = the
carrier' of
S
by A3, FUNCOP_1:19;
then A7:
o .--> (Den o,A') is
ManySortedSet of
by PARTFUN1:def 4, RELAT_1:def 18;
now let i be
set ;
:: thesis: ( i in the carrier' of S implies (o .--> (Den o,A')) . i is Function of (((T # ) * the Arity of S) . i),((T * the ResultSort of S) . i) )assume A8:
i in the
carrier' of
S
;
:: thesis: (o .--> (Den o,A')) . i is Function of (((T # ) * the Arity of S) . i),((T * the ResultSort of S) . i)then
i = [{} ,{{} }]
by TARSKI:def 1;
then A9:
i = o
by TARSKI:def 1;
then A10:
(o .--> (Den o,A')) . i = Den o,
A'
by FUNCOP_1:87;
((T # ) * the Arity of S) . i =
(T # ) . (the Arity of S . i)
by A8, FUNCT_2:21
.=
(T # ) . (<*> the carrier of S)
by A8, FUNCOP_1:13
.=
{{} }
by PRE_CIRC:5
;
then reconsider Oi =
(o .--> (Den o,A')) . i as
Function of
(((T # ) * the Arity of S) . i),
(Result o,A') by A4, A9, FUNCOP_1:87;
A11:
rng Oi = {((Den o,A') . {} )}
by A5, A10, FUNCT_1:14;
(T * the ResultSort of S) . i =
T . (the ResultSort of S . i)
by A8, FUNCT_2:21
.=
T . s
by A2, A8, FUNCOP_1:13
.=
(G . s) \/ {((Den o,A') . {} )}
by FUNCOP_1:87
;
then
rng Oi c= (T * the ResultSort of S) . i
by A11, XBOOLE_1:7;
hence
(o .--> (Den o,A')) . i is
Function of
(((T # ) * the Arity of S) . i),
((T * the ResultSort of S) . i)
by FUNCT_2:8;
:: thesis: verum end;
then reconsider O =
o .--> (Den o,A') as
ManySortedFunction of
(T # ) * the
Arity of
S,
T * the
ResultSort of
S by A7, PBOOLE:def 18;
reconsider G' =
G as
MSSubset of
A' ;
reconsider T' =
T as
ManySortedSet of ;
T' c= the
Sorts of
A'
proof
let i be
set ;
:: according to PBOOLE:def 5 :: thesis: ( not i in the carrier of S' or T' . i c= the Sorts of A' . i )
assume
i in the
carrier of
S'
;
:: thesis: T' . i c= the Sorts of A' . i
then A12:
i = {}
by TARSKI:def 1;
then A13:
T' . i = (G . s) \/ {((Den o,A') . {} )}
by A2, FUNCOP_1:87;
G c= the
Sorts of
A'
by PBOOLE:def 23;
then A14:
G . s c= the
Sorts of
A' . i
by A2, A12, PBOOLE:def 5;
dom (Den o,A') = Args o,
A'
by FUNCT_2:def 1;
then
{} in dom (Den o,A')
by A4, TARSKI:def 1;
then
(Den o,A') . {} in rng (Den o,A')
by FUNCT_1:def 5;
then
{((Den o,A') . {} )} c= the
Sorts of
A' . i
by A6, A12, ZFMISC_1:37;
hence
T' . i c= the
Sorts of
A' . i
by A13, A14, XBOOLE_1:8;
:: thesis: verum
end;
then A15:
the
Sorts of
MSAlgebra(#
T,
O #) is
MSSubset of
A'
by PBOOLE:def 23;
reconsider A'' =
MSAlgebra(#
T,
O #) as
non-empty MSAlgebra of
S' by MSUALG_1:def 8;
now let B be
MSSubset of
A';
:: thesis: ( B = the Sorts of MSAlgebra(# T,O #) implies ( B is opers_closed & the Charact of MSAlgebra(# T,O #) = Opers A',B ) )assume A16:
B = the
Sorts of
MSAlgebra(#
T,
O #)
;
:: thesis: ( B is opers_closed & the Charact of MSAlgebra(# T,O #) = Opers A',B )thus A17:
B is
opers_closed
:: thesis: the Charact of MSAlgebra(# T,O #) = Opers A',Bproof
let o' be
OperSymbol of
S';
:: according to MSUALG_2:def 7 :: thesis: B is_closed_on o'let x be
set ;
:: according to TARSKI:def 3,
MSUALG_2:def 6 :: thesis: ( not x in rng ((Den o',A') | ((the Arity of S' * (B # )) . o')) or x in (the ResultSort of S' * B) . o' )
A18:
o' = o
by A3, TARSKI:def 1;
A19:
((B # ) * the Arity of S) . o =
(B # ) . (the Arity of S . o)
by FUNCT_2:21
.=
(T # ) . (<*> the carrier of S)
by A16, FUNCOP_1:13
.=
{{} }
by PRE_CIRC:5
;
A20:
(Den o,A') | {{} } = Den o,
A'
by A5, RELAT_1:97;
assume
x in rng ((Den o',A') | (((B # ) * the Arity of S') . o'))
;
:: thesis: x in (the ResultSort of S' * B) . o'
then consider y being
set such that A21:
y in dom (Den o,A')
and A22:
x = (Den o,A') . y
by A18, A19, A20, FUNCT_1:def 5;
A23:
x = (Den o,A') . {}
by A4, A21, A22, TARSKI:def 1;
A24:
B . s = (G . s) \/ {((Den o,A') . {} )}
by A16, FUNCOP_1:87;
x in {((Den o,A') . {} )}
by A23, TARSKI:def 1;
then A25:
x in B . s
by A24, XBOOLE_0:def 3;
A26:
dom the
ResultSort of
S' = {[{} ,{{} }]}
by FUNCOP_1:19;
the
ResultSort of
S' . o = s
by A2, FUNCOP_1:13;
hence
x in (the ResultSort of S' * B) . o'
by A18, A25, A26, FUNCT_1:23;
:: thesis: verum
end; now let o' be
OperSymbol of
S';
:: thesis: the Charact of MSAlgebra(# T,O #) . o' = o' /. BA27:
o' = o
by A3, TARSKI:def 1;
A28:
B is_closed_on o
by A17, MSUALG_2:def 7;
((B # ) * the Arity of S') . o =
(B # ) . (the Arity of S' . o)
by FUNCT_2:21
.=
(T # ) . (<*> the carrier of S')
by A16, FUNCOP_1:13
.=
{{} }
by PRE_CIRC:5
;
then
(Den o,A') | (((B # ) * the Arity of S') . o) = Den o,
A'
by A5, RELAT_1:97;
then
the
Charact of
MSAlgebra(#
T,
O #)
. o = (Den o,A') | (((B # ) * the Arity of S') . o)
by FUNCOP_1:87;
hence
the
Charact of
MSAlgebra(#
T,
O #)
. o' = o' /. B
by A27, A28, MSUALG_2:def 8;
:: thesis: verum end; hence
the
Charact of
MSAlgebra(#
T,
O #)
= Opers A',
B
by A16, MSUALG_2:def 9;
:: thesis: verum end;
then reconsider A'' =
A'' as
strict MSSubAlgebra of
A' by A15, MSUALG_2:def 10;
then
G' c= the
Sorts of
A''
by PBOOLE:def 5;
then A30:
G' is
MSSubset of
A''
by PBOOLE:def 23;
now let U1 be
MSSubAlgebra of
A';
:: thesis: ( G' is MSSubset of U1 implies A'' is MSSubAlgebra of U1 )assume A31:
G' is
MSSubset of
U1
;
:: thesis: A'' is MSSubAlgebra of U1now let i be
set ;
:: thesis: ( i in the carrier of S' implies the Sorts of A'' . i c= the Sorts of U1 . i )assume
i in the
carrier of
S'
;
:: thesis: the Sorts of A'' . i c= the Sorts of U1 . ithen A32:
i = s
by A2, TARSKI:def 1;
A33:
the
Sorts of
A'' . s = (G . s) \/ {((Den o,A') . {} )}
by FUNCOP_1:87;
G c= the
Sorts of
U1
by A31, PBOOLE:def 23;
then A34:
G . s c= the
Sorts of
U1 . s
by PBOOLE:def 5;
Constants A' is
MSSubset of
U1
by MSUALG_2:11;
then
Constants A' c= the
Sorts of
U1
by PBOOLE:def 23;
then
(Constants A') . s c= the
Sorts of
U1 . s
by PBOOLE:def 5;
then A35:
Constants A',
s c= the
Sorts of
U1 . s
by MSUALG_2:def 5;
A36:
{} in dom (Den o,A')
by A5, TARSKI:def 1;
then
(Den o,A') . {} in rng (Den o,A')
by FUNCT_1:def 5;
then reconsider b =
(Den o,A') . {} as
Element of the
Sorts of
A' . s by A6, TARSKI:def 1;
A37:
the
Arity of
S' . o = {}
by FUNCOP_1:13;
consider X being non
empty set such that A38:
(
X = the
Sorts of
A' . s &
Constants A',
s = { a where a is Element of X : ex o being OperSymbol of S' st
( the Arity of S' . o = {} & the ResultSort of S' . o = s & a in rng (Den o,A') ) } )
by MSUALG_2:def 4;
b in rng (Den o,A')
by A36, FUNCT_1:def 5;
then
(Den o,A') . {} in Constants A',
s
by A2, A37, A38;
then
{((Den o,A') . {} )} c= the
Sorts of
U1 . s
by A35, ZFMISC_1:37;
hence
the
Sorts of
A'' . i c= the
Sorts of
U1 . i
by A32, A33, A34, XBOOLE_1:8;
:: thesis: verum end; then
the
Sorts of
A'' c= the
Sorts of
U1
by PBOOLE:def 5;
hence
A'' is
MSSubAlgebra of
U1
by MSUALG_2:9;
:: thesis: verum end;
then A39:
s .--> ((G . s) \/ {((Den o,A') . {} )}) =
the
Sorts of
(GenMSAlg G)
by A30, MSUALG_2:def 18
.=
the
Sorts of
A'
by MSAFREE:def 4
;
reconsider Gs =
G . s as
finite set by A1, FINSET_1:def 4;
let i be
set ;
:: according to FINSET_1:def 4,
MSAFREE2:def 11 :: thesis: ( not i in the carrier of S or the Sorts of A . i is finite )
assume
i in the
carrier of
S
;
:: thesis: the Sorts of A . i is finite
then
i = s
by A2, TARSKI:def 1;
then
the
Sorts of
A . i = Gs \/ {((Den o,A') . {} )}
by A39, FUNCOP_1:87;
hence
the
Sorts of
A . i is
finite
;
:: thesis: verum
end;
thus
S is Circuit-like
:: thesis: verum