let IIG be non empty non void Circuit-like monotonic ManySortedSign ; 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; 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; 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; 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; 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; ( 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 S1[ 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 S1[k] holds
S1[k + 1]
proof
A4:
((InnerVertices IIG) \ (SortsWithConstants IIG)) \/ (SortsWithConstants IIG) = InnerVertices IIG
by MSAFREE2:3, XBOOLE_1:45;
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A5:
S1[
k]
;
S1[k + 1]
let v be
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) <= 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;
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;
( 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
;
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;
suppose A14:
v in InputVertices IIG
;
dom t = dom t1then 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
;
verum 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] )
;
dom t = dom t1A18:
((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
;
verum end; 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 )
;
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;
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 H1(
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 = H1(
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;
A29:
now for x being object st x in dom q holds
q . x is DecoratedTreelet x be
object ;
( x in dom q implies q . x is DecoratedTree )assume A30:
x in dom q
;
q . x is DecoratedTreethen 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
;
verum end; A31:
for
k being
Element of
NAT st
k in dom q holds
q . k = H1(
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;
A34:
now for i being Nat st i in dom (doms p) holds
(doms p) . i = (doms q) . ilet i be
Nat;
( 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)
;
(doms p) . i = (doms q) . ithen
(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
;
verum end;
dom q = dom (doms q)
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
;
verum end;
end;
A37:
S1[ 0 ]
proof
let v be
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) <= 0 & e1 = ((Fix_inp_ext iv) . v) . e holds
dom t = dom t1let e,
e1 be
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 t,
t1 be
DecoratedTree;
( 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
;
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;
suppose A46:
v in InputVertices IIG
;
dom t = dom t1then 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
;
verum end; 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] )
;
dom t = dom t1A50:
((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
;
verum end; 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 )
;
dom t = dom t1A53:
((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
;
verum end;
end;
for k being Nat holds S1[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; verum