defpred S1[ 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; ( 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 assume A4:
ex
n being
Nat st
S1[
n]
;
contradictionconsider n being
Nat such that A5:
S1[
n]
and A6:
for
k being
Nat st
S1[
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;
per cases
( v in InputVertices IIG or v in SortsWithConstants IIG or ( not v in InputVertices IIG & not v in SortsWithConstants IIG ) )
;
suppose that A18:
not
v in InputVertices IIG
and A19:
not
v in SortsWithConstants IIG
;
contradictionset 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;
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;
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;
A30:
dom p1 = dom ((Fix_inp_ext iv) * (the_arity_of (action_at v)))
by A26, PRALG_1:def 17;
dom p2 = dom ((Fix_inp_ext iv) * (the_arity_of (action_at v)))
by A28, PRALG_1:def 17;
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;
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;
then reconsider w =
(the_arity_of (action_at v)) . i as
Vertex of
IIG by A30, A31, 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;
[(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 A28, A30, A31, PRALG_1:def 17;
len q2 = len (the_arity_of (action_at v))
by A24, MSAFREE2:10;
then
i in dom q2
by 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;
len q1 = len (the_arity_of (action_at v))
by A34, MSAFREE2:10;
then
i in dom q1
by 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, A30, A31, A36, PRALG_1:def 17;
hence
contradiction
by A6, A7, A20, A32, A39, A38, A37, A40, CIRCUIT1:14;
verum end; end;
hence
( 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 )
; verum