defpred S_{1}[ Nat] means ex v being Vertex of IIG ex it1, it2 being Element of the Sorts of (FreeEnv SCS) . v st

( size (v,SCS) = $1 & ex e1 being Element of the Sorts of (FreeEnv SCS) . v st

( card e1 = size (v,SCS) & it1 = ((Fix_inp_ext iv) . v) . e1 ) & ex e2 being Element of the Sorts of (FreeEnv SCS) . v st

( card e2 = size (v,SCS) & it2 = ((Fix_inp_ext iv) . v) . e2 ) & it1 <> it2 );

let it1, it2 be Element of the Sorts of (FreeEnv SCS) . v; :: thesis: ( ex e being Element of the Sorts of (FreeEnv SCS) . v st

( card e = size (v,SCS) & it1 = ((Fix_inp_ext iv) . v) . e ) & ex e being Element of the Sorts of (FreeEnv SCS) . v st

( card e = size (v,SCS) & it2 = ((Fix_inp_ext iv) . v) . e ) implies it1 = it2 )

( card e = size (v,SCS) & it1 = ((Fix_inp_ext iv) . v) . e ) & ex e being Element of the Sorts of (FreeEnv SCS) . v st

( card e = size (v,SCS) & it2 = ((Fix_inp_ext iv) . v) . e ) implies it1 = it2 ) ; :: thesis: verum

( size (v,SCS) = $1 & ex e1 being Element of the Sorts of (FreeEnv SCS) . v st

( card e1 = size (v,SCS) & it1 = ((Fix_inp_ext iv) . v) . e1 ) & ex e2 being Element of the Sorts of (FreeEnv SCS) . v st

( card e2 = size (v,SCS) & it2 = ((Fix_inp_ext iv) . v) . e2 ) & it1 <> it2 );

let it1, it2 be Element of the Sorts of (FreeEnv SCS) . v; :: thesis: ( ex e being Element of the Sorts of (FreeEnv SCS) . v st

( card e = size (v,SCS) & it1 = ((Fix_inp_ext iv) . v) . e ) & ex e being Element of the Sorts of (FreeEnv SCS) . v st

( card e = size (v,SCS) & it2 = ((Fix_inp_ext iv) . v) . e ) implies it1 = it2 )

now :: thesis: for n being Nat holds not S_{1}[n]

hence
( ex e being Element of the Sorts of (FreeEnv SCS) . v st assume A4:
ex n being Nat st S_{1}[n]
; :: thesis: contradiction

consider n being Nat such that

A5: S_{1}[n]
and

A6: for k being Nat st S_{1}[k] holds

n <= k from NAT_1:sch 5(A4);

consider v being Vertex of IIG, it1, it2 being Element of the Sorts of (FreeEnv SCS) . v such that

A7: size (v,SCS) = n and

A8: ex e1 being Element of the Sorts of (FreeEnv SCS) . v st

( card e1 = size (v,SCS) & it1 = ((Fix_inp_ext iv) . v) . e1 ) and

A9: ex e2 being Element of the Sorts of (FreeEnv SCS) . v st

( card e2 = size (v,SCS) & it2 = ((Fix_inp_ext iv) . v) . e2 ) and

A10: it1 <> it2 by A5;

consider e2 being Element of the Sorts of (FreeEnv SCS) . v such that

A11: card e2 = size (v,SCS) and

A12: it2 = ((Fix_inp_ext iv) . v) . e2 by A9;

consider e1 being Element of the Sorts of (FreeEnv SCS) . v such that

A13: card e1 = size (v,SCS) and

A14: it1 = ((Fix_inp_ext iv) . v) . e1 by A8;

end;consider n being Nat such that

A5: S

A6: for k being Nat st S

n <= k from NAT_1:sch 5(A4);

consider v being Vertex of IIG, it1, it2 being Element of the Sorts of (FreeEnv SCS) . v such that

A7: size (v,SCS) = n and

A8: ex e1 being Element of the Sorts of (FreeEnv SCS) . v st

( card e1 = size (v,SCS) & it1 = ((Fix_inp_ext iv) . v) . e1 ) and

A9: ex e2 being Element of the Sorts of (FreeEnv SCS) . v st

( card e2 = size (v,SCS) & it2 = ((Fix_inp_ext iv) . v) . e2 ) and

A10: it1 <> it2 by A5;

consider e2 being Element of the Sorts of (FreeEnv SCS) . v such that

A11: card e2 = size (v,SCS) and

A12: it2 = ((Fix_inp_ext iv) . v) . e2 by A9;

consider e1 being Element of the Sorts of (FreeEnv SCS) . v such that

A13: card e1 = size (v,SCS) and

A14: it1 = ((Fix_inp_ext iv) . v) . e1 by A8;

per cases
( v in InputVertices IIG or v in SortsWithConstants IIG or ( not v in InputVertices IIG & not v in SortsWithConstants IIG ) )
;

end;

suppose A15:
v in InputVertices IIG
; :: thesis: contradiction

then A16:
ex x2 being Element of the Sorts of SCS . v st e2 = root-tree [x2,v]
by MSAFREE2:9;

ex x1 being Element of the Sorts of SCS . v st e1 = root-tree [x1,v] by A15, MSAFREE2:9;

then it1 = root-tree [(iv . v),v] by A14, A15, Th3

.= it2 by A12, A15, A16, Th3 ;

hence contradiction by A10; :: thesis: verum

end;ex x1 being Element of the Sorts of SCS . v st e1 = root-tree [x1,v] by A15, MSAFREE2:9;

then it1 = root-tree [(iv . v),v] by A14, A15, Th3

.= it2 by A12, A15, A16, Th3 ;

hence contradiction by A10; :: thesis: verum

suppose A17:
v in SortsWithConstants IIG
; :: thesis: contradiction

then it1 =
root-tree [(action_at v), the carrier of IIG]
by A14, Th5

.= it2 by A12, A17, Th5 ;

hence contradiction by A10; :: thesis: verum

end;.= it2 by A12, A17, Th5 ;

hence contradiction by A10; :: thesis: verum

suppose that A18:
not v in InputVertices IIG
and

A19: not v in SortsWithConstants IIG ; :: thesis: contradiction

A19: not v in SortsWithConstants IIG ; :: thesis: contradiction

set Ht = (Fix_inp_ext iv) * (the_arity_of (action_at v));

(InputVertices IIG) \/ (InnerVertices IIG) = the carrier of IIG by XBOOLE_1:45;

then A20: v in InnerVertices IIG by A18, XBOOLE_0:def 3;

then A21: v in (InnerVertices IIG) \ (SortsWithConstants IIG) by A19, XBOOLE_0:def 5;

then consider q1 being DTree-yielding FinSequence such that

A22: e1 = [(action_at v), the carrier of IIG] -tree q1 by A13, CIRCUIT1:12;

[(action_at v), the carrier of IIG] -tree q1 in the Sorts of (FreeEnv SCS) . v by A22;

then [(action_at v), the carrier of IIG] -tree q1 in the Sorts of (FreeEnv SCS) . (the_result_sort_of (action_at v)) by A20, MSAFREE2:def 7;

then B2: len q1 = len (the_arity_of (action_at v)) by MSAFREE2:10;

consider q2 being DTree-yielding FinSequence such that

A23: e2 = [(action_at v), the carrier of IIG] -tree q2 by A11, A21, CIRCUIT1:12;

[(action_at v), the carrier of IIG] -tree q2 in the Sorts of (FreeEnv SCS) . v by A23;

then A24: [(action_at v), the carrier of IIG] -tree q2 in the Sorts of (FreeEnv SCS) . (the_result_sort_of (action_at v)) by A20, MSAFREE2:def 7;

then B1: len q2 = len (the_arity_of (action_at v)) by MSAFREE2:10;

then B3: dom q1 = dom q2 by B2, FINSEQ_3:29;

set acv = action_at v;

B4: dom q2 = dom (the_arity_of (action_at v)) by FINSEQ_3:29, B1;

A25: Fix_inp_ext iv is_homomorphism FreeEnv SCS, FreeEnv SCS by Def2;

then consider p1 being DTree-yielding FinSequence such that

A26: p1 = ((Fix_inp_ext iv) * (the_arity_of (action_at v))) .. q1 and

A27: it1 = [(action_at v), the carrier of IIG] -tree p1 by A14, A20, A22, Th1;

consider p2 being DTree-yielding FinSequence such that

A28: p2 = ((Fix_inp_ext iv) * (the_arity_of (action_at v))) .. q2 and

A29: it2 = [(action_at v), the carrier of IIG] -tree p2 by A12, A20, A23, A25, Th1;

rng (the_arity_of (action_at v)) c= the carrier of IIG by FINSEQ_1:def 4;

then rng (the_arity_of (action_at v)) c= dom (Fix_inp_ext iv) by PARTFUN1:def 2;

then A33: dom (the_arity_of (action_at v)) = dom ((Fix_inp_ext iv) * (the_arity_of (action_at v))) by RELAT_1:27;

A30: dom p1 = (dom ((Fix_inp_ext iv) * (the_arity_of (action_at v)))) /\ (dom q1) by A26, PRALG_1:def 19

.= dom ((Fix_inp_ext iv) * (the_arity_of (action_at v))) by A33, B4, B3 ;

a30: dom p2 = (dom ((Fix_inp_ext iv) * (the_arity_of (action_at v)))) /\ (dom q2) by A28, PRALG_1:def 19

.= dom ((Fix_inp_ext iv) * (the_arity_of (action_at v))) by A33, B4 ;

then len p1 = len p2 by A30, FINSEQ_3:29;

then consider i being Nat such that

A31: i in dom p1 and

A32: p1 . i <> p2 . i by A10, A27, A29, FINSEQ_2:9;

reconsider w = (the_arity_of (action_at v)) . i as Vertex of IIG by A30, A31, A33, FINSEQ_2:11;

[(action_at v), the carrier of IIG] -tree q1 in the Sorts of (FreeEnv SCS) . v by A22;

then A34: [(action_at v), the carrier of IIG] -tree q1 in the Sorts of (FreeEnv SCS) . (the_result_sort_of (action_at v)) by A20, MSAFREE2:def 7;

then reconsider E1 = q1 . i, E2 = q2 . i as Element of the Sorts of (FreeEnv SCS) . w by A30, A33, A31, A24, MSAFREE2:11;

B2: len q1 = len (the_arity_of (action_at v)) by A34, MSAFREE2:10;

[(action_at v), the carrier of IIG] -tree p2 in the Sorts of (FreeEnv SCS) . v by A29;

then A35: [(action_at v), the carrier of IIG] -tree p2 in the Sorts of (FreeEnv SCS) . (the_result_sort_of (action_at v)) by A20, MSAFREE2:def 7;

[(action_at v), the carrier of IIG] -tree p1 in the Sorts of (FreeEnv SCS) . v by A27;

then [(action_at v), the carrier of IIG] -tree p1 in the Sorts of (FreeEnv SCS) . (the_result_sort_of (action_at v)) by A20, MSAFREE2:def 7;

then reconsider It1 = p1 . i, It2 = p2 . i as Element of the Sorts of (FreeEnv SCS) . w by A30, A33, A31, A35, MSAFREE2:11;

reconsider Hti = ((Fix_inp_ext iv) * (the_arity_of (action_at v))) . i as Function ;

A36: Hti = (Fix_inp_ext iv) . ((the_arity_of (action_at v)) . i) by A30, A31, FUNCT_1:12;

then A37: It2 = ((Fix_inp_ext iv) . w) . E2 by a30, A28, A30, A31, PRALG_1:def 19;

i in dom q2 by B1, A30, A33, A31, FINSEQ_3:29;

then E2 in rng q2 by FUNCT_1:def 3;

then A38: card E2 = size (w,SCS) by A11, A21, A23, CIRCUIT1:11;

i in dom q1 by B2, A30, A33, A31, FINSEQ_3:29;

then E1 in rng q1 by FUNCT_1:def 3;

then A39: card E1 = size (w,SCS) by A13, A21, A22, CIRCUIT1:11;

A40: w in rng (the_arity_of (action_at v)) by A30, A33, A31, FUNCT_1:def 3;

It1 = ((Fix_inp_ext iv) . w) . E1 by A26, A31, A36, PRALG_1:def 19;

hence contradiction by A6, A7, A20, A32, A39, A38, A37, A40, CIRCUIT1:14; :: thesis: verum

end;(InputVertices IIG) \/ (InnerVertices IIG) = the carrier of IIG by XBOOLE_1:45;

then A20: v in InnerVertices IIG by A18, XBOOLE_0:def 3;

then A21: v in (InnerVertices IIG) \ (SortsWithConstants IIG) by A19, XBOOLE_0:def 5;

then consider q1 being DTree-yielding FinSequence such that

A22: e1 = [(action_at v), the carrier of IIG] -tree q1 by A13, CIRCUIT1:12;

[(action_at v), the carrier of IIG] -tree q1 in the Sorts of (FreeEnv SCS) . v by A22;

then [(action_at v), the carrier of IIG] -tree q1 in the Sorts of (FreeEnv SCS) . (the_result_sort_of (action_at v)) by A20, MSAFREE2:def 7;

then B2: len q1 = len (the_arity_of (action_at v)) by MSAFREE2:10;

consider q2 being DTree-yielding FinSequence such that

A23: e2 = [(action_at v), the carrier of IIG] -tree q2 by A11, A21, CIRCUIT1:12;

[(action_at v), the carrier of IIG] -tree q2 in the Sorts of (FreeEnv SCS) . v by A23;

then A24: [(action_at v), the carrier of IIG] -tree q2 in the Sorts of (FreeEnv SCS) . (the_result_sort_of (action_at v)) by A20, MSAFREE2:def 7;

then B1: len q2 = len (the_arity_of (action_at v)) by MSAFREE2:10;

then B3: dom q1 = dom q2 by B2, FINSEQ_3:29;

set acv = action_at v;

B4: dom q2 = dom (the_arity_of (action_at v)) by FINSEQ_3:29, B1;

A25: Fix_inp_ext iv is_homomorphism FreeEnv SCS, FreeEnv SCS by Def2;

then consider p1 being DTree-yielding FinSequence such that

A26: p1 = ((Fix_inp_ext iv) * (the_arity_of (action_at v))) .. q1 and

A27: it1 = [(action_at v), the carrier of IIG] -tree p1 by A14, A20, A22, Th1;

consider p2 being DTree-yielding FinSequence such that

A28: p2 = ((Fix_inp_ext iv) * (the_arity_of (action_at v))) .. q2 and

A29: it2 = [(action_at v), the carrier of IIG] -tree p2 by A12, A20, A23, A25, Th1;

rng (the_arity_of (action_at v)) c= the carrier of IIG by FINSEQ_1:def 4;

then rng (the_arity_of (action_at v)) c= dom (Fix_inp_ext iv) by PARTFUN1:def 2;

then A33: dom (the_arity_of (action_at v)) = dom ((Fix_inp_ext iv) * (the_arity_of (action_at v))) by RELAT_1:27;

A30: dom p1 = (dom ((Fix_inp_ext iv) * (the_arity_of (action_at v)))) /\ (dom q1) by A26, PRALG_1:def 19

.= dom ((Fix_inp_ext iv) * (the_arity_of (action_at v))) by A33, B4, B3 ;

a30: dom p2 = (dom ((Fix_inp_ext iv) * (the_arity_of (action_at v)))) /\ (dom q2) by A28, PRALG_1:def 19

.= dom ((Fix_inp_ext iv) * (the_arity_of (action_at v))) by A33, B4 ;

then len p1 = len p2 by A30, FINSEQ_3:29;

then consider i being Nat such that

A31: i in dom p1 and

A32: p1 . i <> p2 . i by A10, A27, A29, FINSEQ_2:9;

reconsider w = (the_arity_of (action_at v)) . i as Vertex of IIG by A30, A31, A33, FINSEQ_2:11;

[(action_at v), the carrier of IIG] -tree q1 in the Sorts of (FreeEnv SCS) . v by A22;

then A34: [(action_at v), the carrier of IIG] -tree q1 in the Sorts of (FreeEnv SCS) . (the_result_sort_of (action_at v)) by A20, MSAFREE2:def 7;

then reconsider E1 = q1 . i, E2 = q2 . i as Element of the Sorts of (FreeEnv SCS) . w by A30, A33, A31, A24, MSAFREE2:11;

B2: len q1 = len (the_arity_of (action_at v)) by A34, MSAFREE2:10;

[(action_at v), the carrier of IIG] -tree p2 in the Sorts of (FreeEnv SCS) . v by A29;

then A35: [(action_at v), the carrier of IIG] -tree p2 in the Sorts of (FreeEnv SCS) . (the_result_sort_of (action_at v)) by A20, MSAFREE2:def 7;

[(action_at v), the carrier of IIG] -tree p1 in the Sorts of (FreeEnv SCS) . v by A27;

then [(action_at v), the carrier of IIG] -tree p1 in the Sorts of (FreeEnv SCS) . (the_result_sort_of (action_at v)) by A20, MSAFREE2:def 7;

then reconsider It1 = p1 . i, It2 = p2 . i as Element of the Sorts of (FreeEnv SCS) . w by A30, A33, A31, A35, MSAFREE2:11;

reconsider Hti = ((Fix_inp_ext iv) * (the_arity_of (action_at v))) . i as Function ;

A36: Hti = (Fix_inp_ext iv) . ((the_arity_of (action_at v)) . i) by A30, A31, FUNCT_1:12;

then A37: It2 = ((Fix_inp_ext iv) . w) . E2 by a30, A28, A30, A31, PRALG_1:def 19;

i in dom q2 by B1, A30, A33, A31, FINSEQ_3:29;

then E2 in rng q2 by FUNCT_1:def 3;

then A38: card E2 = size (w,SCS) by A11, A21, A23, CIRCUIT1:11;

i in dom q1 by B2, A30, A33, A31, FINSEQ_3:29;

then E1 in rng q1 by FUNCT_1:def 3;

then A39: card E1 = size (w,SCS) by A13, A21, A22, CIRCUIT1:11;

A40: w in rng (the_arity_of (action_at v)) by A30, A33, A31, FUNCT_1:def 3;

It1 = ((Fix_inp_ext iv) . w) . E1 by A26, A31, A36, PRALG_1:def 19;

hence contradiction by A6, A7, A20, A32, A39, A38, A37, A40, CIRCUIT1:14; :: thesis: verum

( card e = size (v,SCS) & it1 = ((Fix_inp_ext iv) . v) . e ) & ex e being Element of the Sorts of (FreeEnv SCS) . v st

( card e = size (v,SCS) & it2 = ((Fix_inp_ext iv) . v) . e ) implies it1 = it2 ) ; :: thesis: verum