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, e1 being Element of the Sorts of () . v
for t, t1 being DecoratedTree st t = e & t1 = e1 & e1 = (() . v) . e holds
dom t = dom t1

let A be non-empty Circuit of IIG; :: thesis: for iv being InputValues of A
for v being Vertex of IIG
for e, e1 being Element of the Sorts of () . v
for t, t1 being DecoratedTree st t = e & t1 = e1 & e1 = (() . v) . e holds
dom t = dom t1

let iv be InputValues of A; :: thesis: for v being Vertex of IIG
for e, e1 being Element of the Sorts of () . v
for t, t1 being DecoratedTree st t = e & t1 = e1 & e1 = (() . v) . e holds
dom t = dom t1

let v be Vertex of IIG; :: thesis: for e, e1 being Element of the Sorts of () . v
for t, t1 being DecoratedTree st t = e & t1 = e1 & e1 = (() . v) . e holds
dom t = dom t1

let e, e1 be Element of the Sorts of () . v; :: thesis: for t, t1 being DecoratedTree st t = e & t1 = e1 & e1 = (() . v) . e holds
dom t = dom t1

let t, t1 be DecoratedTree; :: thesis: ( t = e & t1 = e1 & e1 = (() . v) . e implies dom t = dom t1 )
set X = the Sorts of A;
set FX = the Sorts of ();
defpred S1[ Nat] means for v being Vertex of IIG
for e, e1 being Element of the Sorts of () . v
for t, t1 being DecoratedTree st t = e & t1 = e1 & depth (v,A) <= \$1 & e1 = (() . v) . e holds
dom t = dom t1;
reconsider k = depth (v,A) as Element of NAT by ORDINAL1:def 12;
A1: depth (v,A) <= k ;
A2: FreeMSA the Sorts of A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) by MSAFREE:def 14;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
A4: ((InnerVertices IIG) \ ()) \/ () = InnerVertices IIG by ;
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; :: thesis: S1[k + 1]
let v be Vertex of IIG; :: thesis: for e, e1 being Element of the Sorts of () . v
for t, t1 being DecoratedTree st t = e & t1 = e1 & depth (v,A) <= k + 1 & e1 = (() . v) . e holds
dom t = dom t1

let e, e1 be Element of the Sorts of () . v; :: thesis: for t, t1 being DecoratedTree st t = e & t1 = e1 & depth (v,A) <= k + 1 & e1 = (() . v) . e holds
dom t = dom t1

let t, t1 be DecoratedTree; :: thesis: ( t = e & t1 = e1 & depth (v,A) <= k + 1 & e1 = (() . v) . e implies dom t = dom t1 )
assume that
A6: t = e and
A7: t1 = e1 and
A8: depth (v,A) <= k + 1 and
A9: e1 = (() . v) . e ; :: thesis: dom t = dom t1
A10: FreeSort ( the Sorts of A,v) = { 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;
(InputVertices IIG) \/ () = the carrier of IIG by XBOOLE_1:45;
then A11: ( v in InputVertices IIG or v in InnerVertices IIG ) by XBOOLE_0:def 3;
( e in the Sorts of () . v & (FreeSort the Sorts of A) . v = FreeSort ( the Sorts of A,v) ) by MSAFREE:def 11;
then consider a being Element of TS (DTConMSA the Sorts of A) such that
A12: a = e and
A13: ( 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 ;
per cases ( v in InputVertices IIG or ( v in () \ () & ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) ) or ( v in SortsWithConstants IIG & ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) ) or ( v in InnerVertices IIG & ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) ) )
by ;
suppose A14: v in InputVertices IIG ; :: thesis: dom t = dom t1
then A15: ((Fix_inp_ext iv) . v) . a = root-tree [(iv . v),v] by ;
thus dom t = by
.= dom t1 by ; :: thesis: verum
end;
suppose ( v in () \ () & ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) ) ; :: thesis: dom t = dom t1
hence dom t = dom t1 by A6, A7, A9, A12, Th2; :: thesis: verum
end;
suppose that A16: v in SortsWithConstants IIG and
A17: ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) ; :: thesis: dom t = dom t1
A18: ((Fix_inp_ext iv) . v) . a = root-tree [(), the carrier of IIG] by ;
thus dom t = by
.= dom t1 by ; :: thesis: verum
end;
suppose that A19: v in InnerVertices IIG and
A20: ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) ; :: thesis: dom t = dom t1
consider o being OperSymbol of IIG such that
A21: [o, the carrier of IIG] = a . {} and
A22: the_result_sort_of o = v by A20;
A23: o = action_at v by ;
then consider p being DTree-yielding FinSequence such that
A24: e = [(), the carrier of IIG] -tree p by ;
deffunc H1( Nat) -> set = (() . (() /. \$1)) . (p . \$1);
consider q being FinSequence such that
A25: len q = len p and
A26: for k being Nat st k in dom q holds
q . k = H1(k) from A27: dom p = dom q by ;
len p = len () by ;
then A28: dom p = dom () by FINSEQ_3:29;
A29: now :: thesis: for x being object st x in dom q holds
q . x is DecoratedTree
let x be object ; :: thesis: ( x in dom q implies q . x is DecoratedTree )
assume A30: x in dom q ; :: thesis: q . x is DecoratedTree
then reconsider i = x as Element of NAT ;
set v1 = () /. i;
(the_arity_of ()) /. i = () . i by ;
then reconsider ee = p . i as Element of the Sorts of () . (() /. i) by ;
reconsider fv1 = () . (() /. i) as Function of ( the Sorts of () . (() /. i)),( the Sorts of () . (() /. i)) ;
q . i = fv1 . ee by ;
hence q . x is DecoratedTree ; :: thesis: verum
end;
A31: for k being Element of NAT st k in dom q holds
q . k = H1(k) by A26;
reconsider q = q as DTree-yielding FinSequence by ;
A32: ((Fix_inp_ext iv) . v) . e = [(), the carrier of IIG] -tree q by A19, A24, A31, A27, Th4;
A33: dom (doms p) = dom p by TREES_3:37;
A34: now :: thesis: for i being Nat st i in dom (doms p) holds
(doms p) . i = (doms q) . i
let i be Nat; :: thesis: ( i in dom (doms p) implies (doms p) . i = (doms q) . i )
set v1 = () /. i;
reconsider fv1 = () . (() /. i) as Function of ( the Sorts of () . (() /. i)),( the Sorts of () . (() /. i)) ;
assume A35: i in dom (doms p) ; :: thesis: (doms p) . i = (doms q) . i
then (the_arity_of ()) /. i = () . i by ;
then reconsider ee = p . i as Element of the Sorts of () . (() /. i) by ;
q . i = fv1 . ee by A26, A33, A27, A35;
then reconsider ee1 = q . i as Element of the Sorts of () . (() /. i) ;
(the_arity_of ()) /. i in rng () by ;
then depth ((() /. i),A) < k + 1 by ;
then A36: depth ((() /. i),A) <= k by NAT_1:13;
q . i = (() . (() /. i)) . (p . i) by A26, A33, A27, A35;
then dom ee = dom ee1 by ;
hence (doms p) . i = dom ee1 by
.= (doms q) . i by ;
:: thesis: verum
end;
dom q = dom (doms q) by TREES_3:37;
then doms p = doms q by ;
hence dom t = tree (doms q) by
.= dom t1 by ;
:: thesis: verum
end;
end;
end;
A37: S1[ 0 ]
proof
let v be Vertex of IIG; :: thesis: for e, e1 being Element of the Sorts of () . v
for t, t1 being DecoratedTree st t = e & t1 = e1 & depth (v,A) <= 0 & e1 = (() . v) . e holds
dom t = dom t1

let e, e1 be Element of the Sorts of () . v; :: thesis: for t, t1 being DecoratedTree st t = e & t1 = e1 & depth (v,A) <= 0 & e1 = (() . v) . e holds
dom t = dom t1

let t, t1 be DecoratedTree; :: thesis: ( t = e & t1 = e1 & depth (v,A) <= 0 & e1 = (() . v) . e implies dom t = dom t1 )
assume that
A38: t = e and
A39: t1 = e1 and
A40: depth (v,A) <= 0 and
A41: e1 = (() . v) . e ; :: thesis: dom t = dom t1
A42: depth (v,A) = 0 by ;
A43: FreeSort ( the Sorts of A,v) = { 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;
( e in the Sorts of () . v & (FreeSort the Sorts of A) . v = FreeSort ( the Sorts of A,v) ) by MSAFREE:def 11;
then consider a being Element of TS (DTConMSA the Sorts of A) such that
A44: a = e and
A45: ( 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 ;
per cases ( v in InputVertices IIG or ( v in SortsWithConstants IIG & ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) ) or ( v in SortsWithConstants IIG & ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) ) )
by ;
suppose A46: v in InputVertices IIG ; :: thesis: dom t = dom t1
then A47: ((Fix_inp_ext iv) . v) . a = root-tree [(iv . v),v] by ;
thus dom t = by
.= dom t1 by ; :: thesis: verum
end;
suppose that A48: v in SortsWithConstants IIG and
A49: ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) ; :: thesis: dom t = dom t1
A50: ((Fix_inp_ext iv) . v) . a = root-tree [(), the carrier of IIG] by ;
thus dom t = by
.= dom t1 by ; :: thesis: verum
end;
suppose that A51: v in SortsWithConstants IIG and
A52: ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) ; :: thesis: dom t = dom t1
A53: ((Fix_inp_ext iv) . v) . a = root-tree [(), the carrier of IIG] by ;
consider o being OperSymbol of IIG such that
A54: [o, the carrier of IIG] = a . {} and
A55: the_result_sort_of o = v by A52;
A56: SortsWithConstants IIG c= InnerVertices IIG by MSAFREE2:3;
then o = action_at v by ;
then consider p being DTree-yielding FinSequence such that
A57: a = [(), the carrier of IIG] -tree p by ;
v in { s where s is SortSymbol of IIG : s is with_const_op } by ;
then ex s being SortSymbol of IIG st
( v = s & s is with_const_op ) ;
then consider o9 being OperSymbol of IIG such that
A58: the Arity of IIG . o9 = {} and
A59: the ResultSort of IIG . o9 = v by MSUALG_2:def 1;
A60: the_result_sort_of o9 = v by ;
then A61: o9 = action_at v by ;
then len p = len () by
.= len {} by
.= 0 ;
then p = {} ;
then a = root-tree [o9, the carrier of IIG] by ;
hence dom t = by
.= dom t1 by ;
:: thesis: verum
end;
end;
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A37, A3);
hence ( t = e & t1 = e1 & e1 = (() . v) . e implies dom t = dom t1 ) by A1; :: thesis: verum