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
for p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ) holds
((Fix_inp_ext iv) . v) . e = [(action_at v), the carrier of IIG] -tree q
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
for p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ) holds
((Fix_inp_ext iv) . v) . e = [(action_at v), the carrier of IIG] -tree q
let iv be InputValues of A; :: thesis: for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v
for p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ) holds
((Fix_inp_ext iv) . v) . e = [(action_at v), the carrier of IIG] -tree q
let v be Vertex of IIG; :: thesis: for e being Element of the Sorts of (FreeEnv A) . v
for p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ) holds
((Fix_inp_ext iv) . v) . e = [(action_at v), the carrier of IIG] -tree q
let e be Element of the Sorts of (FreeEnv A) . v; :: thesis: for p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ) holds
((Fix_inp_ext iv) . v) . e = [(action_at v), the carrier of IIG] -tree q
let p, q be DTree-yielding FinSequence; :: thesis: ( v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ) implies ((Fix_inp_ext iv) . v) . e = [(action_at v), the carrier of IIG] -tree q )
assume that
A1: v in InnerVertices IIG and
A2: e = [(action_at v), the carrier of IIG] -tree p and
A3: dom p = dom q and
A4: for k being Element of NAT st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ; :: thesis: ((Fix_inp_ext iv) . v) . e = [(action_at v), the carrier of IIG] -tree q
set o = action_at v;
A5: the_result_sort_of (action_at v) = v by A1, MSAFREE2:def 7;
then A6: len p = len (the_arity_of (action_at v)) by A2, MSAFREE2:10;
then reconsider x = p as Element of Args ((action_at v),(FreeEnv A)) by A6, MSAFREE2:5;
A13: FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) by MSAFREE:def 14;
then A14: Args ((action_at v),(FreeEnv A)) = (((FreeSort the Sorts of A) #) * the Arity of IIG) . (action_at v) by MSUALG_1:def 4;
then reconsider pp = p as FinSequence of TS (DTConMSA the Sorts of A) by A6, A11, MSAFREE:8, MSAFREE2:5;
p in Args ((action_at v),(FreeEnv A)) by A6, A11, MSAFREE2:5;
then A15: Sym ((action_at v), the Sorts of A) ==> roots pp by A14, MSAFREE:10;
A16: len q = len (the_arity_of (action_at v)) by A3, A6, FINSEQ_3:29;
then reconsider y = q as Element of Args ((action_at v),(FreeEnv A)) by A7, MSAFREE2:5;
A17: Fix_inp_ext iv is_homomorphism FreeEnv A, FreeEnv A by Def2;
reconsider qq = q as FinSequence of TS (DTConMSA the Sorts of A) by A14, A16, A7, MSAFREE:8, MSAFREE2:5;
q in Args ((action_at v),(FreeEnv A)) by A16, A7, MSAFREE2:5;
then A18: Sym ((action_at v), the Sorts of A) ==> roots qq by A14, MSAFREE:10;
for k being Nat st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) by A4;
then A19: y = (Fix_inp_ext iv) # x by MSUALG_3:def 6;
e = (Sym ((action_at v), the Sorts of A)) -tree pp by A2, MSAFREE:def 9
.= (DenOp ((action_at v), the Sorts of A)) . x by A15, MSAFREE:def 12
.= ( the Charact of (FreeEnv A) . (action_at v)) . x by A13, MSAFREE:def 13
.= (Den ((action_at v),(FreeEnv A))) . x by MSUALG_1:def 6 ;
hence ((Fix_inp_ext iv) . v) . e = (Den ((action_at v),(FreeEnv A))) . q by A5, A19, A17, MSUALG_3:def 7
.= ((FreeOper the Sorts of A) . (action_at v)) . q by A13, MSUALG_1:def 6
.= (DenOp ((action_at v), the Sorts of A)) . q by MSAFREE:def 13
.= (Sym ((action_at v), the Sorts of A)) -tree qq by A18, MSAFREE:def 12
.= [(action_at v), the carrier of IIG] -tree q by MSAFREE:def 9 ;
:: thesis: verum