let S be non empty non void ManySortedSign ; for V being V2() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for x being set holds
( x in InputVertices (X -CircuitStr) iff ( x in Subtrees X & ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] ) )
let V be V2() ManySortedSet of the carrier of S; for X being non empty Subset of (S -Terms V)
for x being set holds
( x in InputVertices (X -CircuitStr) iff ( x in Subtrees X & ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] ) )
let X be non empty Subset of (S -Terms V); for x being set holds
( x in InputVertices (X -CircuitStr) iff ( x in Subtrees X & ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] ) )
set G = X -CircuitStr ;
let x be set ; ( x in InputVertices (X -CircuitStr) iff ( x in Subtrees X & ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] ) )
hereby ( x in Subtrees X & ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] implies x in InputVertices (X -CircuitStr) )
assume A1:
x in InputVertices (X -CircuitStr)
;
( x in Subtrees X & ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] )then A2:
not
x in the
carrier' of
(X -CircuitStr)
by XBOOLE_0:def 5;
thus
x in Subtrees X
by A1;
ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s]reconsider t =
x as
Term of
S,
V by A1, Th4;
( ex
s being
SortSymbol of
S ex
v being
Element of
V . s st
t . {} = [v,s] or
t . {} in [: the carrier' of S,{ the carrier of S}:] )
by MSATERM:2;
then
( ex
s being
SortSymbol of
S ex
v being
Element of
V . s st
t . {} = [v,s] or
t is
CompoundTerm of
S,
V )
by MSATERM:def 6;
then consider s being
SortSymbol of
S,
v being
Element of
V . s such that A3:
t . {} = [v,s]
by A1, A2, Th5;
take s =
s;
ex v being Element of V . s st x = root-tree [v,s]reconsider v =
v as
Element of
V . s ;
take v =
v;
x = root-tree [v,s]thus
x = root-tree [v,s]
by A3, MSATERM:5;
verum
end;
assume A4:
x in Subtrees X
; ( for s being SortSymbol of S
for v being Element of V . s holds not x = root-tree [v,s] or x in InputVertices (X -CircuitStr) )
given s being SortSymbol of S, v being Element of V . s such that A5:
x = root-tree [v,s]
; x in InputVertices (X -CircuitStr)
assume
not x in InputVertices (X -CircuitStr)
; contradiction
then
x in the carrier' of (X -CircuitStr)
by A4, XBOOLE_0:def 5;
then reconsider t = x as CompoundTerm of S,V by Th4;
t . {} = [v,s]
by A5, TREES_4:3;
then
[v,s] in [: the carrier' of S,{ the carrier of S}:]
by MSATERM:def 6;
then
s = the carrier of S
by ZFMISC_1:106;
then
s in s
;
hence
contradiction
; verum