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 (FreeEnv A) . v

for t, t1 being DecoratedTree st t = e & t1 = e1 & e1 = ((Fix_inp_ext iv) . 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 (FreeEnv A) . v

for t, t1 being DecoratedTree st t = e & t1 = e1 & e1 = ((Fix_inp_ext iv) . 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 (FreeEnv A) . v

for t, t1 being DecoratedTree st t = e & t1 = e1 & e1 = ((Fix_inp_ext iv) . v) . e holds

dom t = dom t1

let v be Vertex of IIG; :: thesis: for e, e1 being Element of the Sorts of (FreeEnv A) . v

for t, t1 being DecoratedTree st t = e & t1 = e1 & e1 = ((Fix_inp_ext iv) . v) . e holds

dom t = dom t1

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

dom t = dom t1

let t, t1 be DecoratedTree; :: thesis: ( t = e & t1 = e1 & e1 = ((Fix_inp_ext iv) . v) . e implies dom t = dom t1 )

set X = the Sorts of A;

set FX = the Sorts of (FreeEnv A);

defpred S_{1}[ Nat] means for v being Vertex of IIG

for e, e1 being Element of the Sorts of (FreeEnv A) . v

for t, t1 being DecoratedTree st t = e & t1 = e1 & depth (v,A) <= $1 & e1 = ((Fix_inp_ext iv) . 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 S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(A37, A3);

hence ( t = e & t1 = e1 & e1 = ((Fix_inp_ext iv) . v) . e implies dom t = dom t1 ) by A1; :: thesis: verum

for iv being InputValues of A

for v being Vertex of IIG

for e, e1 being Element of the Sorts of (FreeEnv A) . v

for t, t1 being DecoratedTree st t = e & t1 = e1 & e1 = ((Fix_inp_ext iv) . 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 (FreeEnv A) . v

for t, t1 being DecoratedTree st t = e & t1 = e1 & e1 = ((Fix_inp_ext iv) . 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 (FreeEnv A) . v

for t, t1 being DecoratedTree st t = e & t1 = e1 & e1 = ((Fix_inp_ext iv) . v) . e holds

dom t = dom t1

let v be Vertex of IIG; :: thesis: for e, e1 being Element of the Sorts of (FreeEnv A) . v

for t, t1 being DecoratedTree st t = e & t1 = e1 & e1 = ((Fix_inp_ext iv) . v) . e holds

dom t = dom t1

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

dom t = dom t1

let t, t1 be DecoratedTree; :: thesis: ( t = e & t1 = e1 & e1 = ((Fix_inp_ext iv) . v) . e implies dom t = dom t1 )

set X = the Sorts of A;

set FX = the Sorts of (FreeEnv A);

defpred S

for e, e1 being Element of the Sorts of (FreeEnv A) . v

for t, t1 being DecoratedTree st t = e & t1 = e1 & depth (v,A) <= $1 & e1 = ((Fix_inp_ext iv) . 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 S

S

proof

A37:
S
A4:
((InnerVertices IIG) \ (SortsWithConstants IIG)) \/ (SortsWithConstants IIG) = InnerVertices IIG
by MSAFREE2:3, XBOOLE_1:45;

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A5: S_{1}[k]
; :: thesis: S_{1}[k + 1]

let v be Vertex of IIG; :: thesis: for e, e1 being Element of the Sorts of (FreeEnv A) . v

for t, t1 being DecoratedTree st t = e & t1 = e1 & depth (v,A) <= k + 1 & e1 = ((Fix_inp_ext iv) . v) . e holds

dom t = dom t1

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

dom t = dom t1

let t, t1 be DecoratedTree; :: thesis: ( t = e & t1 = e1 & depth (v,A) <= k + 1 & e1 = ((Fix_inp_ext iv) . 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 = ((Fix_inp_ext iv) . 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) \/ (InnerVertices 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 (FreeEnv A) . 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 A2, A10;

end;let k be Nat; :: thesis: ( S

assume A5: S

let v be Vertex of IIG; :: thesis: for e, e1 being Element of the Sorts of (FreeEnv A) . v

for t, t1 being DecoratedTree st t = e & t1 = e1 & depth (v,A) <= k + 1 & e1 = ((Fix_inp_ext iv) . v) . e holds

dom t = dom t1

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

dom t = dom t1

let t, t1 be DecoratedTree; :: thesis: ( t = e & t1 = e1 & depth (v,A) <= k + 1 & e1 = ((Fix_inp_ext iv) . 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 = ((Fix_inp_ext iv) . 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) \/ (InnerVertices 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 (FreeEnv A) . 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 A2, A10;

per cases
( v in InputVertices IIG or ( v in (InnerVertices IIG) \ (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 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 A13, A11, A4, XBOOLE_0:def 3;

end;

( 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 A13, A11, A4, XBOOLE_0:def 3;

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 A13, Th3, MSAFREE2:2;

thus dom t = {{}} by A6, A12, A13, A14, MSAFREE2:2, TREES_1:29, TREES_4:3

.= dom t1 by A7, A9, A12, A15, TREES_1:29, TREES_4:3 ; :: thesis: verum

end;thus dom t = {{}} by A6, A12, A13, A14, MSAFREE2:2, TREES_1:29, TREES_4:3

.= dom t1 by A7, A9, A12, A15, TREES_1:29, TREES_4:3 ; :: thesis: verum

suppose
( v in (InnerVertices IIG) \ (SortsWithConstants IIG) & ex x being set st

( x in the Sorts of A . v & a = root-tree [x,v] ) ) ; :: thesis: dom t = dom t1

end;

( x in the Sorts of A . v & a = root-tree [x,v] ) ) ; :: thesis: dom t = dom t1

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

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 [(action_at v), the carrier of IIG]
by A12, A16, Th5;

thus dom t = {{}} by A6, A12, A17, TREES_1:29, TREES_4:3

.= dom t1 by A7, A9, A12, A18, TREES_1:29, TREES_4:3 ; :: thesis: verum

end;thus dom t = {{}} by A6, A12, A17, TREES_1:29, TREES_4:3

.= dom t1 by A7, A9, A12, A18, TREES_1:29, TREES_4:3 ; :: thesis: verum

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

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 A19, A22, MSAFREE2:def 7;

then consider p being DTree-yielding FinSequence such that

A24: e = [(action_at v), the carrier of IIG] -tree p by A12, A21, CIRCUIT1:9;

deffunc H_{1}( Nat) -> set = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. $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 = H_{1}(k)
from FINSEQ_1:sch 2();

A27: dom p = dom q by A25, FINSEQ_3:29;

len p = len (the_arity_of (action_at v)) by A22, A23, A24, MSAFREE2:10;

then A28: dom p = dom (the_arity_of (action_at v)) by FINSEQ_3:29;

q . k = H_{1}(k)
by A26;

reconsider q = q as DTree-yielding FinSequence by A29, TREES_3:24;

A32: ((Fix_inp_ext iv) . v) . e = [(action_at v), the carrier of IIG] -tree q by A19, A24, A31, A27, Th4;

A33: dom (doms p) = dom p by TREES_3:37;

then doms p = doms q by A27, A34, FINSEQ_1:13, TREES_3:37;

hence dom t = tree (doms q) by A6, A24, TREES_4:10

.= dom t1 by A7, A9, A32, TREES_4:10 ;

:: thesis: verum

end;A21: [o, the carrier of IIG] = a . {} and

A22: the_result_sort_of o = v by A20;

A23: o = action_at v by A19, A22, MSAFREE2:def 7;

then consider p being DTree-yielding FinSequence such that

A24: e = [(action_at v), the carrier of IIG] -tree p by A12, A21, CIRCUIT1:9;

deffunc H

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 = H

A27: dom p = dom q by A25, FINSEQ_3:29;

len p = len (the_arity_of (action_at v)) by A22, A23, A24, MSAFREE2:10;

then A28: dom p = dom (the_arity_of (action_at v)) by FINSEQ_3:29;

A29: now :: thesis: for x being object st x in dom q holds

q . x is DecoratedTree

A31:
for k being Element of NAT st k 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 = (the_arity_of (action_at v)) /. i;

(the_arity_of (action_at v)) /. i = (the_arity_of o) . i by A23, A28, A27, A30, PARTFUN1:def 6;

then reconsider ee = p . i as Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. i) by A22, A23, A24, A28, A27, A30, MSAFREE2:11;

reconsider fv1 = (Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. i) as Function of ( the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. i)),( the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. i)) ;

q . i = fv1 . ee by A26, A30;

hence q . x is DecoratedTree ; :: thesis: verum

end;assume A30: x in dom q ; :: thesis: q . x is DecoratedTree

then reconsider i = x as Element of NAT ;

set v1 = (the_arity_of (action_at v)) /. i;

(the_arity_of (action_at v)) /. i = (the_arity_of o) . i by A23, A28, A27, A30, PARTFUN1:def 6;

then reconsider ee = p . i as Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. i) by A22, A23, A24, A28, A27, A30, MSAFREE2:11;

reconsider fv1 = (Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. i) as Function of ( the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. i)),( the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. i)) ;

q . i = fv1 . ee by A26, A30;

hence q . x is DecoratedTree ; :: thesis: verum

q . k = H

reconsider q = q as DTree-yielding FinSequence by A29, TREES_3:24;

A32: ((Fix_inp_ext iv) . v) . e = [(action_at v), 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

dom q = dom (doms q)
by TREES_3:37;(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 = (the_arity_of (action_at v)) /. i;

reconsider fv1 = (Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. i) as Function of ( the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. i)),( the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. i)) ;

assume A35: i in dom (doms p) ; :: thesis: (doms p) . i = (doms q) . i

then (the_arity_of (action_at v)) /. i = (the_arity_of o) . i by A23, A28, A33, PARTFUN1:def 6;

then reconsider ee = p . i as Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. i) by A22, A23, A24, A28, A33, A35, MSAFREE2:11;

q . i = fv1 . ee by A26, A33, A27, A35;

then reconsider ee1 = q . i as Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. i) ;

(the_arity_of (action_at v)) /. i in rng (the_arity_of (action_at v)) by A28, A33, A35, PARTFUN2:2;

then depth (((the_arity_of (action_at v)) /. i),A) < k + 1 by A8, A19, CIRCUIT1:19, XXREAL_0:2;

then A36: depth (((the_arity_of (action_at v)) /. i),A) <= k by NAT_1:13;

q . i = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. i)) . (p . i) by A26, A33, A27, A35;

then dom ee = dom ee1 by A5, A36;

hence (doms p) . i = dom ee1 by A33, A35, FUNCT_6:22

.= (doms q) . i by A33, A27, A35, FUNCT_6:22 ;

:: thesis: verum

end;set v1 = (the_arity_of (action_at v)) /. i;

reconsider fv1 = (Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. i) as Function of ( the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. i)),( the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. i)) ;

assume A35: i in dom (doms p) ; :: thesis: (doms p) . i = (doms q) . i

then (the_arity_of (action_at v)) /. i = (the_arity_of o) . i by A23, A28, A33, PARTFUN1:def 6;

then reconsider ee = p . i as Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. i) by A22, A23, A24, A28, A33, A35, MSAFREE2:11;

q . i = fv1 . ee by A26, A33, A27, A35;

then reconsider ee1 = q . i as Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. i) ;

(the_arity_of (action_at v)) /. i in rng (the_arity_of (action_at v)) by A28, A33, A35, PARTFUN2:2;

then depth (((the_arity_of (action_at v)) /. i),A) < k + 1 by A8, A19, CIRCUIT1:19, XXREAL_0:2;

then A36: depth (((the_arity_of (action_at v)) /. i),A) <= k by NAT_1:13;

q . i = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. i)) . (p . i) by A26, A33, A27, A35;

then dom ee = dom ee1 by A5, A36;

hence (doms p) . i = dom ee1 by A33, A35, FUNCT_6:22

.= (doms q) . i by A33, A27, A35, FUNCT_6:22 ;

:: thesis: verum

then doms p = doms q by A27, A34, FINSEQ_1:13, TREES_3:37;

hence dom t = tree (doms q) by A6, A24, TREES_4:10

.= dom t1 by A7, A9, A32, TREES_4:10 ;

:: thesis: verum

proof

for k being Nat holds S
let v be Vertex of IIG; :: thesis: for e, e1 being Element of the Sorts of (FreeEnv A) . v

for t, t1 being DecoratedTree st t = e & t1 = e1 & depth (v,A) <= 0 & e1 = ((Fix_inp_ext iv) . v) . e holds

dom t = dom t1

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

dom t = dom t1

let t, t1 be DecoratedTree; :: thesis: ( t = e & t1 = e1 & depth (v,A) <= 0 & e1 = ((Fix_inp_ext iv) . 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 = ((Fix_inp_ext iv) . v) . e ; :: thesis: dom t = dom t1

A42: depth (v,A) = 0 by A40, NAT_1:3;

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 (FreeEnv A) . 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 A2, A43;

end;for t, t1 being DecoratedTree st t = e & t1 = e1 & depth (v,A) <= 0 & e1 = ((Fix_inp_ext iv) . v) . e holds

dom t = dom t1

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

dom t = dom t1

let t, t1 be DecoratedTree; :: thesis: ( t = e & t1 = e1 & depth (v,A) <= 0 & e1 = ((Fix_inp_ext iv) . 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 = ((Fix_inp_ext iv) . v) . e ; :: thesis: dom t = dom t1

A42: depth (v,A) = 0 by A40, NAT_1:3;

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 (FreeEnv A) . 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 A2, A43;

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 A42, A45, CIRCUIT1:18;

end;

( 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 A42, A45, CIRCUIT1:18;

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 A45, Th3, MSAFREE2:2;

thus dom t = {{}} by A38, A44, A45, A46, MSAFREE2:2, TREES_1:29, TREES_4:3

.= dom t1 by A39, A41, A44, A47, TREES_1:29, TREES_4:3 ; :: thesis: verum

end;thus dom t = {{}} by A38, A44, A45, A46, MSAFREE2:2, TREES_1:29, TREES_4:3

.= dom t1 by A39, A41, A44, A47, TREES_1:29, TREES_4:3 ; :: thesis: verum

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

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 [(action_at v), the carrier of IIG]
by A44, A48, Th5;

thus dom t = {{}} by A38, A44, A49, TREES_1:29, TREES_4:3

.= dom t1 by A39, A41, A44, A50, TREES_1:29, TREES_4:3 ; :: thesis: verum

end;thus dom t = {{}} by A38, A44, A49, TREES_1:29, TREES_4:3

.= dom t1 by A39, A41, A44, A50, TREES_1:29, TREES_4:3 ; :: thesis: verum

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

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 [(action_at v), the carrier of IIG]
by A44, A51, Th5;

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 A51, A55, MSAFREE2:def 7;

then consider p being DTree-yielding FinSequence such that

A57: a = [(action_at v), the carrier of IIG] -tree p by A44, A54, CIRCUIT1:9;

v in { s where s is SortSymbol of IIG : s is with_const_op } by A51, MSAFREE2:def 1;

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 A59, MSUALG_1:def 2;

then A61: o9 = action_at v by A51, A56, MSAFREE2:def 7;

then len p = len (the_arity_of o9) by A44, A60, A57, MSAFREE2:10

.= len {} by A58, MSUALG_1:def 1

.= 0 ;

then p = {} ;

then a = root-tree [o9, the carrier of IIG] by A61, A57, TREES_4:20;

hence dom t = {{}} by A38, A44, TREES_1:29, TREES_4:3

.= dom t1 by A39, A41, A44, A53, TREES_1:29, TREES_4:3 ;

:: thesis: verum

end;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 A51, A55, MSAFREE2:def 7;

then consider p being DTree-yielding FinSequence such that

A57: a = [(action_at v), the carrier of IIG] -tree p by A44, A54, CIRCUIT1:9;

v in { s where s is SortSymbol of IIG : s is with_const_op } by A51, MSAFREE2:def 1;

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 A59, MSUALG_1:def 2;

then A61: o9 = action_at v by A51, A56, MSAFREE2:def 7;

then len p = len (the_arity_of o9) by A44, A60, A57, MSAFREE2:10

.= len {} by A58, MSUALG_1:def 1

.= 0 ;

then p = {} ;

then a = root-tree [o9, the carrier of IIG] by A61, A57, TREES_4:20;

hence dom t = {{}} by A38, A44, TREES_1:29, TREES_4:3

.= dom t1 by A39, A41, A44, A53, TREES_1:29, TREES_4:3 ;

:: thesis: verum

hence ( t = e & t1 = e1 & e1 = ((Fix_inp_ext iv) . v) . e implies dom t = dom t1 ) by A1; :: thesis: verum