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 for n being Nat holds not S1[n]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;
[(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;
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