let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: for A being non-empty Circuit of IIG
for iv being InputValues of A
for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st v in SortsWithConstants IIG holds
((Fix_inp_ext iv) . v) . e = root-tree [(action_at v),the carrier of IIG]
let A be non-empty Circuit of IIG; :: thesis: for iv being InputValues of A
for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st v in SortsWithConstants IIG holds
((Fix_inp_ext iv) . v) . e = root-tree [(action_at v),the carrier of IIG]
let iv be InputValues of A; :: thesis: for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st v in SortsWithConstants IIG holds
((Fix_inp_ext iv) . v) . e = root-tree [(action_at v),the carrier of IIG]
let v be Vertex of IIG; :: thesis: for e being Element of the Sorts of (FreeEnv A) . v st v in SortsWithConstants IIG holds
((Fix_inp_ext iv) . v) . e = root-tree [(action_at v),the carrier of IIG]
let e be Element of the Sorts of (FreeEnv A) . v; :: thesis: ( v in SortsWithConstants IIG implies ((Fix_inp_ext iv) . v) . e = root-tree [(action_at v),the carrier of IIG] )
A1:
FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #)
by MSAFREE:def 16;
set X = the Sorts of A;
assume A2:
v in SortsWithConstants IIG
; :: thesis: ((Fix_inp_ext iv) . v) . e = root-tree [(action_at v),the carrier of IIG]
e in (FreeSort the Sorts of A) . v
by A1;
then
e in FreeSort the Sorts of A,v
by MSAFREE:def 13;
then
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 12;
then consider a being Element of TS (DTConMSA the Sorts of A) such that
A3:
( e = 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 ) ) )
;
per cases
( ex x being set st
( x in the Sorts of A . v & e = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o,the carrier of IIG] = e . {} & the_result_sort_of o = v ) )
by A3;
suppose
ex
o being
OperSymbol of
IIG st
(
[o,the carrier of IIG] = e . {} &
the_result_sort_of o = v )
;
:: thesis: ((Fix_inp_ext iv) . v) . e = root-tree [(action_at v),the carrier of IIG]then consider o' being
OperSymbol of
IIG such that A6:
[o',the carrier of IIG] = e . {}
and A7:
the_result_sort_of o' = v
;
A8:
SortsWithConstants IIG c= InnerVertices IIG
by MSAFREE2:5;
then A9:
the_result_sort_of (action_at v) = v
by A2, MSAFREE2:def 7;
v in { s where s is SortSymbol of IIG : s is with_const_op }
by A2, MSAFREE2:def 1;
then consider s being
SortSymbol of
IIG such that A10:
v = s
and A11:
s is
with_const_op
;
consider o being
OperSymbol of
IIG such that A12:
the
Arity of
IIG . o = {}
and A13:
the
ResultSort of
IIG . o = v
by A10, A11, MSUALG_2:def 2;
the_result_sort_of o = v
by A13, MSUALG_1:def 7;
then A14:
o = action_at v
by A2, A8, MSAFREE2:def 7;
A15:
o' = action_at v
by A2, A7, A8, MSAFREE2:def 7;
action_at v in the
carrier' of
IIG
;
then A16:
action_at v in dom the
Arity of
IIG
by FUNCT_2:def 1;
A17:
Args (action_at v),
(FreeEnv A) =
((the Sorts of (FreeEnv A) # ) * the Arity of IIG) . (action_at v)
by MSUALG_1:def 9
.=
(the Sorts of (FreeEnv A) # ) . (<*> the carrier of IIG)
by A12, A14, A16, FUNCT_1:23
.=
{{} }
by PRE_CIRC:5
;
then reconsider x =
{} as
Element of
Args (action_at v),
(FreeEnv A) by TARSKI:def 1;
A18:
x = (Fix_inp_ext iv) # x
by A17, TARSKI:def 1;
A19:
Fix_inp_ext iv is_homomorphism FreeEnv A,
FreeEnv A
by Def2;
consider q being
DTree-yielding FinSequence such that A20:
e = [(action_at v),the carrier of IIG] -tree q
by A6, A15, CIRCUIT1:10;
len q =
len (the_arity_of (action_at v))
by A9, A20, MSAFREE2:13
.=
len {}
by A12, A14, MSUALG_1:def 6
.=
0
;
then
q = {}
;
then A21:
e = root-tree [(action_at v),the carrier of IIG]
by A20, TREES_4:20;
A22:
Args (action_at v),
(FreeEnv A) = (((FreeSort the Sorts of A) # ) * the Arity of IIG) . o
by A1, A14, MSUALG_1:def 9;
then reconsider p =
x as
FinSequence of
TS (DTConMSA the Sorts of A) by MSAFREE:8;
A23:
Sym (action_at v),the
Sorts of
A ==> roots p
by A14, A22, MSAFREE:10;
(Den (action_at v),(FreeEnv A)) . x =
((FreeOper the Sorts of A) . (action_at v)) . x
by A1, MSUALG_1:def 11
.=
(DenOp (action_at v),the Sorts of A) . x
by MSAFREE:def 15
.=
(Sym (action_at v),the Sorts of A) -tree p
by A23, MSAFREE:def 14
.=
[(action_at v),the carrier of IIG] -tree p
by MSAFREE:def 11
.=
root-tree [(action_at v),the carrier of IIG]
by TREES_4:20
;
hence
((Fix_inp_ext iv) . v) . e = root-tree [(action_at v),the carrier of IIG]
by A9, A18, A19, A21, MSUALG_3:def 9;
:: thesis: verum end;