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);
A1:
FreeMSA the Sorts of A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #)
by MSAFREE:def 16;
defpred S1[ Element of 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;
A2:
S1[ 0 ]
proof
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 t1let 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 t1let 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 A3:
(
t = e &
t1 = e1 )
and A4:
depth v,
A <= 0
and A5:
e1 = ((Fix_inp_ext iv) . v) . e
;
:: thesis: dom t = dom t1
A6:
depth v,
A = 0
by A4, NAT_1:3;
A7:
e in the
Sorts of
(FreeEnv A) . v
;
A8:
(FreeSort the Sorts of A) . v = FreeSort the
Sorts of
A,
v
by MSAFREE:def 13;
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 12;
then consider a being
Element of
TS (DTConMSA the Sorts of A) such that A9:
a = e
and A10:
( 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 A1, A7, A8;
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 A6, A10, CIRCUIT1:19;
suppose A11:
v in InputVertices IIG
;
:: thesis: dom t = dom t1then consider x being
set such that A12:
x in the
Sorts of
A . v
and A13:
a = root-tree [x,v]
by A10, MSAFREE2:2;
A14:
((Fix_inp_ext iv) . v) . a = root-tree [(iv . v),v]
by A11, A12, A13, Th3;
thus dom t =
{{} }
by A3, A9, A13, TREES_1:56, TREES_4:3
.=
dom t1
by A3, A5, A9, A14, TREES_1:56, TREES_4:3
;
:: thesis: verum end; suppose that A15:
v in SortsWithConstants IIG
and A16:
ex
x being
set st
(
x in the
Sorts of
A . v &
a = root-tree [x,v] )
;
:: thesis: dom t = dom t1consider x being
set such that
x in the
Sorts of
A . v
and A17:
a = root-tree [x,v]
by A16;
A18:
((Fix_inp_ext iv) . v) . a = root-tree [(action_at v),the carrier of IIG]
by A9, A15, Th5;
thus dom t =
{{} }
by A3, A9, A17, TREES_1:56, TREES_4:3
.=
dom t1
by A3, A5, A9, A18, TREES_1:56, TREES_4:3
;
:: thesis: verum end; suppose that A19:
v in SortsWithConstants 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 t1consider o being
OperSymbol of
IIG such that A21:
[o,the carrier of IIG] = a . {}
and A22:
the_result_sort_of o = v
by A20;
v in { s where s is SortSymbol of IIG : s is with_const_op }
by A19, MSAFREE2:def 1;
then consider s being
SortSymbol of
IIG such that A23:
v = s
and A24:
s is
with_const_op
;
consider o' being
OperSymbol of
IIG such that A25:
the
Arity of
IIG . o' = {}
and A26:
the
ResultSort of
IIG . o' = v
by A23, A24, MSUALG_2:def 2;
A27:
SortsWithConstants IIG c= InnerVertices IIG
by MSAFREE2:5;
A28:
the_result_sort_of o' = v
by A26, MSUALG_1:def 7;
then A29:
o' = action_at v
by A19, A27, MSAFREE2:def 7;
o = action_at v
by A19, A22, A27, MSAFREE2:def 7;
then consider p being
DTree-yielding FinSequence such that A30:
a = [(action_at v),the carrier of IIG] -tree p
by A9, A21, CIRCUIT1:10;
len p =
len (the_arity_of o')
by A9, A28, A29, A30, MSAFREE2:13
.=
len {}
by A25, MSUALG_1:def 6
.=
0
;
then
p = {}
;
then A31:
a = root-tree [o',the carrier of IIG]
by A29, A30, TREES_4:20;
A32:
((Fix_inp_ext iv) . v) . a = root-tree [(action_at v),the carrier of IIG]
by A9, A19, Th5;
thus dom t =
{{} }
by A3, A9, A31, TREES_1:56, TREES_4:3
.=
dom t1
by A3, A5, A9, A32, TREES_1:56, TREES_4:3
;
:: thesis: verum end;
end;
A33:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A34:
S1[
k]
;
:: thesis: S1[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 t1let 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 t1let 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 A35:
(
t = e &
t1 = e1 &
depth v,
A <= k + 1 &
e1 = ((Fix_inp_ext iv) . v) . e )
;
:: thesis: dom t = dom t1
A36:
e in the
Sorts of
(FreeEnv A) . v
;
A37:
(FreeSort the Sorts of A) . v = FreeSort the
Sorts of
A,
v
by MSAFREE:def 13;
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 12;
then consider a being
Element of
TS (DTConMSA the Sorts of A) such that A38:
a = e
and A39:
( 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 A1, A36, A37;
(InputVertices IIG) \/ (InnerVertices IIG) = the
carrier of
IIG
by XBOOLE_1:45;
then A40:
(
v in InputVertices IIG or
v in InnerVertices IIG )
by XBOOLE_0:def 3;
A41:
((InnerVertices IIG) \ (SortsWithConstants IIG)) \/ (SortsWithConstants IIG) = InnerVertices IIG
by MSAFREE2:5, XBOOLE_1:45;
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 A39, A40, A41, XBOOLE_0:def 3;
suppose A42:
v in InputVertices IIG
;
:: thesis: dom t = dom t1then consider x being
set such that A43:
x in the
Sorts of
A . v
and A44:
a = root-tree [x,v]
by A39, MSAFREE2:2;
A45:
((Fix_inp_ext iv) . v) . a = root-tree [(iv . v),v]
by A42, A43, A44, Th3;
thus dom t =
{{} }
by A35, A38, A44, TREES_1:56, TREES_4:3
.=
dom t1
by A35, A38, A45, TREES_1:56, TREES_4:3
;
:: thesis: verum end; suppose that A49:
v in SortsWithConstants IIG
and A50:
ex
x being
set st
(
x in the
Sorts of
A . v &
a = root-tree [x,v] )
;
:: thesis: dom t = dom t1consider x being
set such that
x in the
Sorts of
A . v
and A51:
a = root-tree [x,v]
by A50;
A52:
((Fix_inp_ext iv) . v) . a = root-tree [(action_at v),the carrier of IIG]
by A38, A49, Th5;
thus dom t =
{{} }
by A35, A38, A51, TREES_1:56, TREES_4:3
.=
dom t1
by A35, A38, A52, TREES_1:56, TREES_4:3
;
:: thesis: verum end; suppose that A53:
v in InnerVertices IIG
and A54:
ex
o being
OperSymbol of
IIG st
(
[o,the carrier of IIG] = a . {} &
the_result_sort_of o = v )
;
:: thesis: dom t = dom t1consider o being
OperSymbol of
IIG such that A55:
[o,the carrier of IIG] = a . {}
and A56:
the_result_sort_of o = v
by A54;
A57:
o = action_at v
by A53, A56, MSAFREE2:def 7;
then consider p being
DTree-yielding FinSequence such that A58:
e = [(action_at v),the carrier of IIG] -tree p
by A38, A55, CIRCUIT1:10;
deffunc H1(
Nat)
-> set =
((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. $1)) . (p . $1);
consider q being
FinSequence such that A59:
len q = len p
and A60:
for
k being
Nat st
k in dom q holds
q . k = H1(
k)
from FINSEQ_1:sch 2();
A61:
for
k being
Element of
NAT st
k in dom q holds
q . k = H1(
k)
by A60;
len p = len (the_arity_of (action_at v))
by A56, A57, A58, MSAFREE2:13;
then A62:
dom p = dom (the_arity_of (action_at v))
by FINSEQ_3:31;
A63:
dom (doms p) = dom p
by TREES_3:39;
A64:
dom p = dom q
by A59, FINSEQ_3:31;
now let x be
set ;
:: thesis: ( x in dom q implies q . x is DecoratedTree )assume A65:
x in dom q
;
:: thesis: q . x is DecoratedTreethen reconsider i =
x as
Element of
NAT ;
set v1 =
(the_arity_of (action_at v)) /. i;
A66:
i in dom p
by A59, A65, FINSEQ_3:31;
(the_arity_of (action_at v)) /. i = (the_arity_of o) . i
by A57, A62, A64, A65, PARTFUN1:def 8;
then reconsider ee =
p . i as
Element of the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) /. i) by A56, A57, A58, A62, A64, A65, MSAFREE2:14;
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 A60, A66, A64;
hence
q . x is
DecoratedTree
;
:: thesis: verum end; then reconsider q =
q as
DTree-yielding FinSequence by TREES_3:26;
A67:
((Fix_inp_ext iv) . v) . e = [(action_at v),the carrier of IIG] -tree q
by A53, A58, A61, A64, Th4;
A68:
dom q = dom (doms q)
by TREES_3:39;
now 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;
assume A69:
i in dom (doms p)
;
:: thesis: (doms p) . i = (doms q) . ithen A70:
q . i = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. i)) . (p . i)
by A60, A63, A64;
(the_arity_of (action_at v)) /. i = (the_arity_of o) . i
by A57, A62, A63, A69, PARTFUN1:def 8;
then reconsider ee =
p . i as
Element of the
Sorts of
(FreeEnv A) . ((the_arity_of (action_at v)) /. i) by A56, A57, A58, A62, A63, A69, MSAFREE2:14;
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 A60, A63, A69, A64;
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 A62, A63, A69, PARTFUN2:4;
then
depth ((the_arity_of (action_at v)) /. i),
A < k + 1
by A35, A53, CIRCUIT1:20, XXREAL_0:2;
then
depth ((the_arity_of (action_at v)) /. i),
A <= k
by NAT_1:13;
then
dom ee = dom ee1
by A34, A70;
hence (doms p) . i =
dom ee1
by A63, A69, FUNCT_6:31
.=
(doms q) . i
by A63, A64, A69, FUNCT_6:31
;
:: thesis: verum end; then
doms p = doms q
by A63, A64, A68, FINSEQ_1:17;
hence dom t =
tree (doms q)
by A35, A58, TREES_4:10
.=
dom t1
by A35, A67, TREES_4:10
;
:: thesis: verum end;
end;
A71:
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A2, A33);
reconsider k = depth v,A as Element of NAT by ORDINAL1:def 13;
depth v,A <= k
;
hence
( t = e & t1 = e1 & e1 = ((Fix_inp_ext iv) . v) . e implies dom t = dom t1 )
by A71; :: thesis: verum