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