let IIG be non empty non void Circuit-like monotonic ManySortedSign ; for A being non-empty finite-yielding MSAlgebra over IIG
for v being Element of IIG holds
( size (v,A) = 1 iff v in (InputVertices IIG) \/ (SortsWithConstants IIG) )
let A be non-empty finite-yielding MSAlgebra over IIG; for v being Element of IIG holds
( size (v,A) = 1 iff v in (InputVertices IIG) \/ (SortsWithConstants IIG) )
let v be Element of IIG; ( size (v,A) = 1 iff v in (InputVertices IIG) \/ (SortsWithConstants IIG) )
consider s being non empty finite Subset of NAT such that
A1:
s = { (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum }
and
A2:
size (v,A) = max s
by Def4;
reconsider Y = s as non empty finite real-membered set ;
max Y in { (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum }
by A1, XXREAL_2:def 8;
then consider e being Element of the Sorts of (FreeEnv A) . v such that
A3:
card e = max Y
;
A4:
FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #)
by MSAFREE:def 14;
then
( e in the Sorts of (FreeEnv A) . v & the Sorts of (FreeEnv A) . v = FreeSort ( the Sorts of A,v) )
by MSAFREE:def 11;
then A5:
e in { a where a is Element of TS (DTConMSA the Sorts of A) : ( ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) ) }
by MSAFREE:def 10;
thus
( size (v,A) = 1 implies v in (InputVertices IIG) \/ (SortsWithConstants IIG) )
( v in (InputVertices IIG) \/ (SortsWithConstants IIG) implies size (v,A) = 1 )proof
assume A6:
size (
v,
A)
= 1
;
v in (InputVertices IIG) \/ (SortsWithConstants IIG)
now v in (InputVertices IIG) \/ (SortsWithConstants IIG)assume A7:
not
v in (InputVertices IIG) \/ (SortsWithConstants IIG)
;
contradictionthen
not
v in SortsWithConstants IIG
by XBOOLE_0:def 3;
then
not
v in { v9 where v9 is SortSymbol of IIG : v9 is with_const_op }
by MSAFREE2:def 1;
then A8:
not
v is
with_const_op
;
A9:
the
carrier of
IIG = (InputVertices IIG) \/ (InnerVertices IIG)
by XBOOLE_1:45;
not
v in InputVertices IIG
by A7, XBOOLE_0:def 3;
then
v in InnerVertices IIG
by A9, XBOOLE_0:def 3;
then consider x being
object such that A10:
x in dom the
ResultSort of
IIG
and A11:
v = the
ResultSort of
IIG . x
by FUNCT_1:def 3;
reconsider o =
x as
OperSymbol of
IIG by A10;
per cases
( not the Arity of IIG . o = {} or not the ResultSort of IIG . o = v )
by A8, MSUALG_2:def 1;
suppose
not the
Arity of
IIG . o = {}
;
contradictionthen A12:
the_arity_of o <> {}
by MSUALG_1:def 1;
reconsider O =
[: the carrier' of IIG,{ the carrier of IIG}:] \/ (Union (coprod the Sorts of A)) as non
empty set ;
reconsider R =
REL the
Sorts of
A as
Relation of
O,
(O *) ;
the
carrier of
IIG in { the carrier of IIG}
by TARSKI:def 1;
then A13:
[o, the carrier of IIG] in [: the carrier' of IIG,{ the carrier of IIG}:]
by ZFMISC_1:87;
DTConMSA the
Sorts of
A = DTConstrStr(#
O,
R #)
by MSAFREE:def 8;
then reconsider o9 =
[o, the carrier of IIG] as
Symbol of
(DTConMSA the Sorts of A) by A13, XBOOLE_0:def 3;
o9 in NonTerminals (DTConMSA the Sorts of A)
by A13, MSAFREE:6;
then consider p being
FinSequence of
TS (DTConMSA the Sorts of A) such that A14:
o9 ==> roots p
by DTCONSTR:def 5;
reconsider op =
o9 -tree p as
Element of
TS (DTConMSA the Sorts of A) by A14, DTCONSTR:def 1;
reconsider e1 =
op as
finite DecoratedTree ;
reconsider co =
card e1 as
Real ;
A15:
op . {} = o9
by TREES_4:def 4;
then
op in { a9 where a9 is Element of TS (DTConMSA the Sorts of A) : ( ex x9 being set st
( x9 in the Sorts of A . v & a9 = root-tree [x9,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a9 . {} & the_result_sort_of o = v ) ) }
;
then A16:
op in FreeSort ( the
Sorts of
A,
v)
by MSAFREE:def 10;
A17: the
Sorts of
(FreeEnv A) . (the_result_sort_of o) =
(FreeSort the Sorts of A) . v
by A4, A11, MSUALG_1:def 2
.=
FreeSort ( the
Sorts of
A,
v)
by MSAFREE:def 11
;
then reconsider e1 =
e1 as
Element of the
Sorts of
(FreeEnv A) . v by A11, A16, MSUALG_1:def 2;
len p = len (the_arity_of o)
by A16, A17, MSAFREE2:10;
then
p <> {}
by A12;
then
rng p <> {}
;
then A18:
1
in dom p
by FINSEQ_3:32;
( ex
q being
DTree-yielding FinSequence st
(
p = q &
dom op = tree (doms q) ) &
0 + 1
= 1 )
by TREES_4:def 4;
then A19:
<*0*> in dom op
by A18, PRE_CIRC:13;
then consider i being
Nat,
T being
DecoratedTree,
q being
Node of
T such that A20:
(
i < len p &
T = p . (i + 1) &
<*0*> = <*i*> ^ q )
by TREES_4:11;
op . <*0*> = T . q
by A20, TREES_4:12;
then A21:
[<*0*>,(T . q)] in op
by A19, FUNCT_1:1;
{} in dom op
by TREES_1:22;
then
[{},o9] in op
by A15, FUNCT_1:1;
then A22:
{[{},o9],[<*0*>,(T . q)]} c= op
by A21, ZFMISC_1:32;
e1 in the
Sorts of
(FreeEnv A) . v
;
then A23:
co in Y
by A1;
[{},o9] <> [<*0*>,(T . q)]
by XTUPLE_0:1;
then
card {[{},o9],[<*0*>,(T . q)]} = 2
by CARD_2:57;
then
2
<= co
by A22, NAT_1:43;
then
co > size (
v,
A)
by A6, XXREAL_0:2;
hence
contradiction
by A2, A23, XXREAL_2:def 8;
verum end; end;
hence
v in (InputVertices IIG) \/ (SortsWithConstants IIG)
;
verum
end;
consider a being Element of TS (DTConMSA the Sorts of A) such that
A24:
a = e
and
A25:
( ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) )
by A5;
assume A26:
v in (InputVertices IIG) \/ (SortsWithConstants IIG)
; size (v,A) = 1
per cases
( v in InputVertices IIG or v in SortsWithConstants IIG )
by A26, XBOOLE_0:def 3;
suppose
v in InputVertices IIG
;
size (v,A) = 1then consider x being
set such that
x in the
Sorts of
A . v
and A27:
a = root-tree [x,v]
by A25, MSAFREE2:2;
root-tree [x,v] =
{{}} --> [x,v]
by TREES_1:29, TREES_4:def 2
.=
[:{{}},{[x,v]}:]
by FUNCOP_1:def 2
.=
{[{},[x,v]]}
by ZFMISC_1:29
;
hence
size (
v,
A)
= 1
by A2, A3, A24, A27, CARD_1:30;
verum end; suppose
v in SortsWithConstants IIG
;
size (v,A) = 1then
v in { v9 where v9 is SortSymbol of IIG : v9 is with_const_op }
by MSAFREE2:def 1;
then consider v9 being
SortSymbol of
IIG such that A28:
v9 = v
and A29:
v9 is
with_const_op
;
consider o being
OperSymbol of
IIG such that A30:
the
Arity of
IIG . o = {}
and A31:
the
ResultSort of
IIG . o = v9
by A29, MSUALG_2:def 1;
now size (v,A) = 1per cases
( ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o9 being OperSymbol of IIG st
( [o9, the carrier of IIG] = a . {} & the_result_sort_of o9 = v ) )
by A25;
suppose
ex
o9 being
OperSymbol of
IIG st
(
[o9, the carrier of IIG] = a . {} &
the_result_sort_of o9 = v )
;
size (v,A) = 1then consider o9 being
OperSymbol of
IIG such that A33:
[o9, the carrier of IIG] = a . {}
and A34:
the_result_sort_of o9 = v
;
the_result_sort_of o9 = the_result_sort_of o
by A28, A31, A34, MSUALG_1:def 2;
then A35:
o9 = o
by MSAFREE2:def 6;
(
NonTerminals (DTConMSA the Sorts of A) = [: the carrier' of IIG,{ the carrier of IIG}:] & the
carrier of
IIG in { the carrier of IIG} )
by MSAFREE:6, TARSKI:def 1;
then reconsider nt =
[o9, the carrier of IIG] as
NonTerminal of
(DTConMSA the Sorts of A) by ZFMISC_1:87;
consider ts being
FinSequence of
TS (DTConMSA the Sorts of A) such that A36:
a = nt -tree ts
and
nt ==> roots ts
by A33, DTCONSTR:10;
reconsider ts =
ts as
DTree-yielding FinSequence ;
len ts =
len (the_arity_of o9)
by A24, A34, A36, MSAFREE2:10
.=
len {}
by A30, A35, MSUALG_1:def 1
.=
0
;
then
ts = {}
;
then a =
root-tree nt
by A36, TREES_4:20
.=
{[{},nt]}
by TREES_4:6
;
hence
size (
v,
A)
= 1
by A2, A3, A24, CARD_1:30;
verum end; hence
size (
v,
A)
= 1
;
verum end;