let IIG be non empty non void Circuit-like monotonic ManySortedSign ; for SCS being non-empty Circuit of IIG
for v being Vertex of IIG
for iv being InputValues of SCS st v in SortsWithConstants IIG holds
IGValue (v,iv) = (Set-Constants SCS) . v
reconsider p = {} as DTree-yielding FinSequence ;
let SCS be non-empty Circuit of IIG; for v being Vertex of IIG
for iv being InputValues of SCS st v in SortsWithConstants IIG holds
IGValue (v,iv) = (Set-Constants SCS) . v
let v be Vertex of IIG; for iv being InputValues of SCS st v in SortsWithConstants IIG holds
IGValue (v,iv) = (Set-Constants SCS) . v
let iv be InputValues of SCS; ( v in SortsWithConstants IIG implies IGValue (v,iv) = (Set-Constants SCS) . v )
assume A1:
v in SortsWithConstants IIG
; IGValue (v,iv) = (Set-Constants SCS) . v
set e = ((Eval SCS) . v) . (root-tree [(action_at v), the carrier of IIG]);
A2:
{} = <*> the carrier of IIG
;
set X = the Sorts of SCS;
set F = Eval SCS;
A3:
dom the Arity of IIG = the carrier' of IIG
by FUNCT_2:def 1;
A4:
dom the ResultSort of IIG = the carrier' of IIG
by FUNCT_2:def 1;
set o = action_at v;
A5:
SortsWithConstants IIG c= InnerVertices IIG
by MSAFREE2:3;
then A6:
v = the_result_sort_of (action_at v)
by A1, MSAFREE2:def 7;
SortsWithConstants IIG = { v1 where v1 is SortSymbol of IIG : v1 is with_const_op }
by MSAFREE2:def 1;
then consider x9 being SortSymbol of IIG such that
A7:
x9 = v
and
A8:
x9 is with_const_op
by A1;
consider o1 being OperSymbol of IIG such that
A9:
the Arity of IIG . o1 = {}
and
A10:
the ResultSort of IIG . o1 = x9
by A8, MSUALG_2:def 1;
the ResultSort of IIG . o1 = the_result_sort_of o1
by MSUALG_1:def 2;
then A11:
action_at v = o1
by A1, A5, A7, A10, MSAFREE2:def 7;
A12: Args ((action_at v),(FreeEnv SCS)) =
(( the Sorts of (FreeEnv SCS) #) * the Arity of IIG) . (action_at v)
by MSUALG_1:def 4
.=
( the Sorts of (FreeEnv SCS) #) . ( the Arity of IIG . (action_at v))
by A3, FUNCT_1:13
.=
{{}}
by A9, A11, A2, PRE_CIRC:2
;
then reconsider x = {} as Element of Args ((action_at v),(FreeEnv SCS)) by TARSKI:def 1;
reconsider Fx = (Eval SCS) # x as Element of Args ((action_at v),SCS) ;
Eval SCS is_homomorphism FreeEnv SCS,SCS
by MSAFREE2:def 9;
then A13:
((Eval SCS) . (the_result_sort_of (action_at v))) . ((Den ((action_at v),(FreeEnv SCS))) . x) = (Den ((action_at v),SCS)) . Fx
by MSUALG_3:def 7;
A14:
FreeMSA the Sorts of SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #)
by MSAFREE:def 14;
then A15: Den ((action_at v),(FreeEnv SCS)) =
(FreeOper the Sorts of SCS) . (action_at v)
by MSUALG_1:def 6
.=
DenOp ((action_at v), the Sorts of SCS)
by MSAFREE:def 13
;
{} in Args ((action_at v),(FreeEnv SCS))
by A12, TARSKI:def 1;
then A16:
p in (((FreeSort the Sorts of SCS) #) * the Arity of IIG) . (action_at v)
by A14, MSUALG_1:def 4;
then reconsider p9 = {} as FinSequence of TS (DTConMSA the Sorts of SCS) by MSAFREE:8;
Sym ((action_at v), the Sorts of SCS) ==> roots p9
by A16, MSAFREE:10;
then A17: (Den ((action_at v),(FreeEnv SCS))) . {} =
(Sym ((action_at v), the Sorts of SCS)) -tree p
by A15, MSAFREE:def 12
.=
[(action_at v), the carrier of IIG] -tree {}
by MSAFREE:def 9
.=
root-tree [(action_at v), the carrier of IIG]
by TREES_4:20
;
dom (Den ((action_at v),SCS)) = Args ((action_at v),SCS)
by FUNCT_2:def 1;
then A18:
((Eval SCS) . v) . (root-tree [(action_at v), the carrier of IIG]) in rng (Den ((action_at v),SCS))
by A6, A17, A13, FUNCT_1:def 3;
Result ((action_at v),SCS) =
( the Sorts of SCS * the ResultSort of IIG) . (action_at v)
by MSUALG_1:def 5
.=
the Sorts of SCS . ( the ResultSort of IIG . (action_at v))
by A4, FUNCT_1:13
;
then reconsider e = ((Eval SCS) . v) . (root-tree [(action_at v), the carrier of IIG]) as Element of the Sorts of SCS . v by A6, A17, A13, MSUALG_1:def 2;
ex A being non empty set st
( A = the Sorts of SCS . v & Constants (SCS,v) = { a where a is Element of A : ex o being OperSymbol of IIG st
( the Arity of IIG . o = {} & the ResultSort of IIG . o = v & a in rng (Den (o,SCS)) ) } )
by MSUALG_2:def 3;
then A19:
e in Constants (SCS,v)
by A7, A9, A10, A11, A18;
ex e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size (v,SCS) & IGTree (v,iv) = ((Fix_inp_ext iv) . v) . e )
by Def3;
hence IGValue (v,iv) =
e
by A1, Th5
.=
(Set-Constants SCS) . v
by A1, A19, CIRCUIT1:1
;
verum