:: MSATERM semantic presentation
begin
Lm1: for n being set
for p being FinSequence st n in dom p holds
ex k being Element of NAT st
( n = k + 1 & k < len p )
proof
let n be set ; ::_thesis: for p being FinSequence st n in dom p holds
ex k being Element of NAT st
( n = k + 1 & k < len p )
let p be FinSequence; ::_thesis: ( n in dom p implies ex k being Element of NAT st
( n = k + 1 & k < len p ) )
assume A1: n in dom p ; ::_thesis: ex k being Element of NAT st
( n = k + 1 & k < len p )
then reconsider n = n as Element of NAT ;
n >= 1 by A1, FINSEQ_3:25;
then consider k being Nat such that
A2: n = 1 + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
take k ; ::_thesis: ( n = k + 1 & k < len p )
n <= len p by A1, FINSEQ_3:25;
hence ( n = k + 1 & k < len p ) by A2, NAT_1:13; ::_thesis: verum
end;
Lm2: now__::_thesis:_for_n_being_Element_of_NAT_
for_x_being_set_
for_p_being_FinSequence_of_x_st_n_<_len_p_holds_
p_._(n_+_1)_in_x
let n be Element of NAT ; ::_thesis: for x being set
for p being FinSequence of x st n < len p holds
p . (n + 1) in x
let x be set ; ::_thesis: for p being FinSequence of x st n < len p holds
p . (n + 1) in x
let p be FinSequence of x; ::_thesis: ( n < len p implies p . (n + 1) in x )
n >= 0 by NAT_1:2;
then A1: n + 1 >= 0 + 1 by XREAL_1:7;
assume n < len p ; ::_thesis: p . (n + 1) in x
then n + 1 <= len p by NAT_1:13;
then n + 1 in dom p by A1, FINSEQ_3:25;
then A2: p . (n + 1) in rng p by FUNCT_1:def_3;
rng p c= x by FINSEQ_1:def_4;
hence p . (n + 1) in x by A2; ::_thesis: verum
end;
definition
let S be non empty non void ManySortedSign ;
let V be ManySortedSet of the carrier of S;
funcS -Terms V -> Subset of (FinTrees the carrier of (DTConMSA V)) equals :Def1: :: MSATERM:def 1
TS (DTConMSA V);
correctness
coherence
TS (DTConMSA V) is Subset of (FinTrees the carrier of (DTConMSA V));
;
end;
:: deftheorem Def1 defines -Terms MSATERM:def_1_:_
for S being non empty non void ManySortedSign
for V being ManySortedSet of the carrier of S holds S -Terms V = TS (DTConMSA V);
registration
let S be non empty non void ManySortedSign ;
let V be V16() ManySortedSet of the carrier of S;
clusterS -Terms V -> non empty ;
correctness
coherence
not S -Terms V is empty ;
;
end;
definition
let S be non empty non void ManySortedSign ;
let V be V16() ManySortedSet of the carrier of S;
mode Term of S,V is Element of S -Terms V;
end;
definition
let S be non empty non void ManySortedSign ;
let V be V16() ManySortedSet of the carrier of S;
let o be OperSymbol of S;
:: original: Sym
redefine func Sym (o,V) -> NonTerminal of (DTConMSA V);
coherence
Sym (o,V) is NonTerminal of (DTConMSA V)
proof
A1: the carrier of S in { the carrier of S} by TARSKI:def_1;
A2: NonTerminals (DTConMSA V) = [: the carrier' of S,{ the carrier of S}:] by MSAFREE:6;
Sym (o,V) = [o, the carrier of S] by MSAFREE:def_9;
hence Sym (o,V) is NonTerminal of (DTConMSA V) by A2, A1, ZFMISC_1:87; ::_thesis: verum
end;
end;
definition
let S be non empty non void ManySortedSign ;
let V be V16() ManySortedSet of the carrier of S;
let sy be NonTerminal of (DTConMSA V);
mode ArgumentSeq of sy -> FinSequence of S -Terms V means :Def2: :: MSATERM:def 2
it is SubtreeSeq of sy;
existence
ex b1 being FinSequence of S -Terms V st b1 is SubtreeSeq of sy
proof
set q = the SubtreeSeq of sy;
the SubtreeSeq of sy is FinSequence of S -Terms V ;
hence ex b1 being FinSequence of S -Terms V st b1 is SubtreeSeq of sy ; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines ArgumentSeq MSATERM:def_2_:_
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for sy being NonTerminal of (DTConMSA V)
for b4 being FinSequence of S -Terms V holds
( b4 is ArgumentSeq of sy iff b4 is SubtreeSeq of sy );
theorem Th1: :: MSATERM:1
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being FinSequence holds
( ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) iff a is ArgumentSeq of Sym (o,V) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being FinSequence holds
( ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) iff a is ArgumentSeq of Sym (o,V) )
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for o being OperSymbol of S
for a being FinSequence holds
( ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) iff a is ArgumentSeq of Sym (o,V) )
let o be OperSymbol of S; ::_thesis: for a being FinSequence holds
( ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) iff a is ArgumentSeq of Sym (o,V) )
let a be FinSequence; ::_thesis: ( ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) iff a is ArgumentSeq of Sym (o,V) )
A1: [o, the carrier of S] = Sym (o,V) by MSAFREE:def_9;
A2: S -Terms V = TS (DTConMSA V) ;
hereby ::_thesis: ( a is ArgumentSeq of Sym (o,V) implies ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) )
assume [o, the carrier of S] -tree a in S -Terms V ; ::_thesis: ( a is DTree-yielding implies a is ArgumentSeq of Sym (o,V) )
then reconsider t = [o, the carrier of S] -tree a as Element of TS (DTConMSA V) ;
assume A3: a is DTree-yielding ; ::_thesis: a is ArgumentSeq of Sym (o,V)
then t . {} = [o, the carrier of S] by TREES_4:def_4;
then consider p being FinSequence of TS (DTConMSA V) such that
A4: t = (Sym (o,V)) -tree p and
A5: Sym (o,V) ==> roots p by A1, DTCONSTR:10;
a = p by A3, A4, TREES_4:15;
then a is SubtreeSeq of Sym (o,V) by A5, DTCONSTR:def_6;
hence a is ArgumentSeq of Sym (o,V) by A2, Def2; ::_thesis: verum
end;
assume a is ArgumentSeq of Sym (o,V) ; ::_thesis: ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding )
then reconsider a = a as ArgumentSeq of Sym (o,V) ;
reconsider p = a as FinSequence of TS (DTConMSA V) by Def1;
p is SubtreeSeq of Sym (o,V) by Def2;
then Sym (o,V) ==> roots p by DTCONSTR:def_6;
hence ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) by A1, DTCONSTR:def_1; ::_thesis: verum
end;
Lm3: now__::_thesis:_for_S_being_non_empty_non_void_ManySortedSign_
for_V_being_V16()_ManySortedSet_of_the_carrier_of_S
for_x_being_set_holds_
(_(_x_in_Terminals_(DTConMSA_V)_implies_ex_s_being_SortSymbol_of_S_ex_v_being_Element_of_V_._s_st_x_=_[v,s]_)_&_(_for_s_being_SortSymbol_of_S
for_a_being_Element_of_V_._s_st_x_=_[a,s]_holds_
x_in_Terminals_(DTConMSA_V)_)_)
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for x being set holds
( ( x in Terminals (DTConMSA V) implies ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S
for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA V) ) )
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for x being set holds
( ( x in Terminals (DTConMSA V) implies ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S
for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA V) ) )
let x be set ; ::_thesis: ( ( x in Terminals (DTConMSA V) implies ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S
for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA V) ) )
set X = V;
set G = DTConMSA V;
A1: Terminals (DTConMSA V) = Union (coprod V) by MSAFREE:6;
hereby ::_thesis: for s being SortSymbol of S
for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA V)
assume x in Terminals (DTConMSA V) ; ::_thesis: ex s being SortSymbol of S ex v being Element of V . s st x = [v,s]
then consider s being set such that
A2: s in dom (coprod V) and
A3: x in (coprod V) . s by A1, CARD_5:2;
reconsider s = s as SortSymbol of S by A2, PARTFUN1:def_2;
(coprod V) . s = coprod (s,V) by MSAFREE:def_3;
then ex a being set st
( a in V . s & x = [a,s] ) by A3, MSAFREE:def_2;
hence ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ; ::_thesis: verum
end;
let s be SortSymbol of S; ::_thesis: for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA V)
let a be Element of V . s; ::_thesis: ( x = [a,s] implies x in Terminals (DTConMSA V) )
assume x = [a,s] ; ::_thesis: x in Terminals (DTConMSA V)
then x in coprod (s,V) by MSAFREE:def_2;
then A4: x in (coprod V) . s by MSAFREE:def_3;
dom (coprod V) = the carrier of S by PARTFUN1:def_2;
hence x in Terminals (DTConMSA V) by A1, A4, CARD_5:2; ::_thesis: verum
end;
Lm4: now__::_thesis:_for_S_being_non_empty_non_void_ManySortedSign_
for_A_being_MSAlgebra_over_S
for_V_being_V16()_ManySortedSet_of_the_carrier_of_S
for_x_being_set_holds_
(_(_not_x_in_Terminals_(DTConMSA_(_the_Sorts_of_A_\/_V))_or_ex_s_being_SortSymbol_of_S_ex_a_being_set_st_
(_a_in_the_Sorts_of_A_._s_&_x_=_[a,s]_)_or_ex_s_being_SortSymbol_of_S_ex_v_being_Element_of_V_._s_st_x_=_[v,s]_)_&_(_for_s_being_SortSymbol_of_S_holds_
(_(_for_a_being_set_st_a_in_the_Sorts_of_A_._s_&_x_=_[a,s]_holds_
x_in_Terminals_(DTConMSA_(_the_Sorts_of_A_\/_V))_)_&_(_for_a_being_Element_of_V_._s_st_x_=_[a,s]_holds_
x_in_Terminals_(DTConMSA_(_the_Sorts_of_A_\/_V))_)_)_)_)
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra over S
for V being V16() ManySortedSet of the carrier of S
for x being set holds
( ( not x in Terminals (DTConMSA ( the Sorts of A \/ V)) or ex s being SortSymbol of S ex a being set st
( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S holds
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) ) ) )
let A be MSAlgebra over S; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for x being set holds
( ( not x in Terminals (DTConMSA ( the Sorts of A \/ V)) or ex s being SortSymbol of S ex a being set st
( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S holds
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) ) ) )
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for x being set holds
( ( not x in Terminals (DTConMSA ( the Sorts of A \/ V)) or ex s being SortSymbol of S ex a being set st
( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S holds
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) ) ) )
let x be set ; ::_thesis: ( ( not x in Terminals (DTConMSA ( the Sorts of A \/ V)) or ex s being SortSymbol of S ex a being set st
( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S holds
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) ) ) )
set X = the Sorts of A \/ V;
set G = DTConMSA ( the Sorts of A \/ V);
A1: dom (coprod ( the Sorts of A \/ V)) = the carrier of S by PARTFUN1:def_2;
A2: Terminals (DTConMSA ( the Sorts of A \/ V)) = Union (coprod ( the Sorts of A \/ V)) by MSAFREE:6;
hereby ::_thesis: for s being SortSymbol of S holds
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) )
assume x in Terminals (DTConMSA ( the Sorts of A \/ V)) ; ::_thesis: ( ex s being SortSymbol of S ex a being set st
( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] )
then consider s being set such that
A3: s in dom (coprod ( the Sorts of A \/ V)) and
A4: x in (coprod ( the Sorts of A \/ V)) . s by A2, CARD_5:2;
reconsider s = s as SortSymbol of S by A3, PARTFUN1:def_2;
(coprod ( the Sorts of A \/ V)) . s = coprod (s,( the Sorts of A \/ V)) by MSAFREE:def_3;
then consider a being set such that
A5: a in ( the Sorts of A \/ V) . s and
A6: x = [a,s] by A4, MSAFREE:def_2;
( the Sorts of A \/ V) . s = ( the Sorts of A . s) \/ (V . s) by PBOOLE:def_4;
then ( a in the Sorts of A . s or a in V . s ) by A5, XBOOLE_0:def_3;
hence ( ex s being SortSymbol of S ex a being set st
( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) by A6; ::_thesis: verum
end;
let s be SortSymbol of S; ::_thesis: ( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) )
A7: ( the Sorts of A \/ V) . s = ( the Sorts of A . s) \/ (V . s) by PBOOLE:def_4;
hereby ::_thesis: for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A \/ V))
let a be set ; ::_thesis: ( a in the Sorts of A . s & x = [a,s] implies x in Terminals (DTConMSA ( the Sorts of A \/ V)) )
assume a in the Sorts of A . s ; ::_thesis: ( x = [a,s] implies x in Terminals (DTConMSA ( the Sorts of A \/ V)) )
then A8: a in ( the Sorts of A \/ V) . s by A7, XBOOLE_0:def_3;
assume x = [a,s] ; ::_thesis: x in Terminals (DTConMSA ( the Sorts of A \/ V))
then x in coprod (s,( the Sorts of A \/ V)) by A8, MSAFREE:def_2;
then x in (coprod ( the Sorts of A \/ V)) . s by MSAFREE:def_3;
hence x in Terminals (DTConMSA ( the Sorts of A \/ V)) by A2, A1, CARD_5:2; ::_thesis: verum
end;
let a be Element of V . s; ::_thesis: ( x = [a,s] implies x in Terminals (DTConMSA ( the Sorts of A \/ V)) )
assume A9: x = [a,s] ; ::_thesis: x in Terminals (DTConMSA ( the Sorts of A \/ V))
a in ( the Sorts of A \/ V) . s by A7, XBOOLE_0:def_3;
then x in coprod (s,( the Sorts of A \/ V)) by A9, MSAFREE:def_2;
then x in (coprod ( the Sorts of A \/ V)) . s by MSAFREE:def_3;
hence x in Terminals (DTConMSA ( the Sorts of A \/ V)) by A2, A1, CARD_5:2; ::_thesis: verum
end;
Lm5: now__::_thesis:_for_S_being_non_empty_non_void_ManySortedSign_
for_V_being_V16()_ManySortedSet_of_the_carrier_of_S
for_x_being_set_holds_
(_x_is_NonTerminal_of_(DTConMSA_V)_iff_x_in_[:_the_carrier'_of_S,{_the_carrier_of_S}:]_)
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for x being set holds
( x is NonTerminal of (DTConMSA V) iff x in [: the carrier' of S,{ the carrier of S}:] )
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for x being set holds
( x is NonTerminal of (DTConMSA V) iff x in [: the carrier' of S,{ the carrier of S}:] )
set G = DTConMSA V;
let x be set ; ::_thesis: ( x is NonTerminal of (DTConMSA V) iff x in [: the carrier' of S,{ the carrier of S}:] )
NonTerminals (DTConMSA V) = [: the carrier' of S,{ the carrier of S}:] by MSAFREE:6;
hence ( x is NonTerminal of (DTConMSA V) iff x in [: the carrier' of S,{ the carrier of S}:] ) ; ::_thesis: verum
end;
scheme :: MSATERM:sch 1
TermInd{ F1() -> non empty non void ManySortedSign , F2() -> V16() ManySortedSet of the carrier of F1(), P1[ set ] } :
for t being Term of F1(),F2() holds P1[t]
provided
A1: for s being SortSymbol of F1()
for v being Element of F2() . s holds P1[ root-tree [v,s]] and
A2: for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,F2()) st ( for t being Term of F1(),F2() st t in rng p holds
P1[t] ) holds
P1[[o, the carrier of F1()] -tree p]
proof
set X = F2();
set G = DTConMSA F2();
A3: for nt being Symbol of (DTConMSA F2())
for ts being FinSequence of TS (DTConMSA F2()) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA F2()) st t in rng ts holds
P1[t] ) holds
P1[nt -tree ts]
proof
let nt be Symbol of (DTConMSA F2()); ::_thesis: for ts being FinSequence of TS (DTConMSA F2()) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA F2()) st t in rng ts holds
P1[t] ) holds
P1[nt -tree ts]
let ts be FinSequence of TS (DTConMSA F2()); ::_thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA F2()) st t in rng ts holds
P1[t] ) implies P1[nt -tree ts] )
assume that
A4: nt ==> roots ts and
A5: for t being DecoratedTree of the carrier of (DTConMSA F2()) st t in rng ts holds
P1[t] ; ::_thesis: P1[nt -tree ts]
nt in { s where s is Symbol of (DTConMSA F2()) : ex n being FinSequence st s ==> n } by A4;
then reconsider sy = nt as NonTerminal of (DTConMSA F2()) by LANG1:def_3;
reconsider p = ts as FinSequence of F1() -Terms F2() ;
sy in [: the carrier' of F1(),{ the carrier of F1()}:] by Lm5;
then consider o being OperSymbol of F1(), x2 being Element of { the carrier of F1()} such that
A6: sy = [o,x2] by DOMAIN_1:1;
A7: x2 = the carrier of F1() by TARSKI:def_1;
[o, the carrier of F1()] = Sym (o,F2()) by MSAFREE:def_9;
then ts is SubtreeSeq of Sym (o,F2()) by A4, A6, A7, DTCONSTR:def_6;
then reconsider p = p as ArgumentSeq of Sym (o,F2()) by Def2;
for t being Term of F1(),F2() st t in rng p holds
P1[t] by A5;
hence P1[nt -tree ts] by A2, A6, A7; ::_thesis: verum
end;
A8: for s being Symbol of (DTConMSA F2()) st s in Terminals (DTConMSA F2()) holds
P1[ root-tree s]
proof
let x be Symbol of (DTConMSA F2()); ::_thesis: ( x in Terminals (DTConMSA F2()) implies P1[ root-tree x] )
assume x in Terminals (DTConMSA F2()) ; ::_thesis: P1[ root-tree x]
then ex s being SortSymbol of F1() ex v being Element of F2() . s st x = [v,s] by Lm3;
hence P1[ root-tree x] by A1; ::_thesis: verum
end;
for t being DecoratedTree of the carrier of (DTConMSA F2()) st t in TS (DTConMSA F2()) holds
P1[t] from DTCONSTR:sch_7(A8, A3);
hence for t being Term of F1(),F2() holds P1[t] ; ::_thesis: verum
end;
definition
let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
let V be V16() ManySortedSet of the carrier of S;
mode c-Term of A,V is Term of S,( the Sorts of A \/ V);
end;
definition
let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
let V be V16() ManySortedSet of the carrier of S;
let o be OperSymbol of S;
mode ArgumentSeq of o,A,V is ArgumentSeq of Sym (o,( the Sorts of A \/ V));
end;
scheme :: MSATERM:sch 2
CTermInd{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), F3() -> V16() ManySortedSet of the carrier of F1(), P1[ set ] } :
for t being c-Term of F2(),F3() holds P1[t]
provided
A1: for s being SortSymbol of F1()
for x being Element of the Sorts of F2() . s holds P1[ root-tree [x,s]] and
A2: for s being SortSymbol of F1()
for v being Element of F3() . s holds P1[ root-tree [v,s]] and
A3: for o being OperSymbol of F1()
for p being ArgumentSeq of o,F2(),F3() st ( for t being c-Term of F2(),F3() st t in rng p holds
P1[t] ) holds
P1[(Sym (o,( the Sorts of F2() \/ F3()))) -tree p]
proof
set X = the Sorts of F2() \/ F3();
set G = DTConMSA ( the Sorts of F2() \/ F3());
A4: for nt being Symbol of (DTConMSA ( the Sorts of F2() \/ F3()))
for ts being FinSequence of TS (DTConMSA ( the Sorts of F2() \/ F3())) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) st t in rng ts holds
P1[t] ) holds
P1[nt -tree ts]
proof
let nt be Symbol of (DTConMSA ( the Sorts of F2() \/ F3())); ::_thesis: for ts being FinSequence of TS (DTConMSA ( the Sorts of F2() \/ F3())) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) st t in rng ts holds
P1[t] ) holds
P1[nt -tree ts]
let ts be FinSequence of TS (DTConMSA ( the Sorts of F2() \/ F3())); ::_thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) st t in rng ts holds
P1[t] ) implies P1[nt -tree ts] )
assume that
A5: nt ==> roots ts and
A6: for t being DecoratedTree of the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) st t in rng ts holds
P1[t] ; ::_thesis: P1[nt -tree ts]
nt in { s where s is Symbol of (DTConMSA ( the Sorts of F2() \/ F3())) : ex n being FinSequence st s ==> n } by A5;
then reconsider sy = nt as NonTerminal of (DTConMSA ( the Sorts of F2() \/ F3())) by LANG1:def_3;
reconsider p = ts as FinSequence of F1() -Terms ( the Sorts of F2() \/ F3()) ;
sy in [: the carrier' of F1(),{ the carrier of F1()}:] by Lm5;
then consider o being OperSymbol of F1(), x2 being Element of { the carrier of F1()} such that
A7: sy = [o,x2] by DOMAIN_1:1;
A8: [o, the carrier of F1()] = Sym (o,( the Sorts of F2() \/ F3())) by MSAFREE:def_9;
A9: x2 = the carrier of F1() by TARSKI:def_1;
then ts is SubtreeSeq of Sym (o,( the Sorts of F2() \/ F3())) by A5, A7, A8, DTCONSTR:def_6;
then reconsider p = p as ArgumentSeq of Sym (o,( the Sorts of F2() \/ F3())) by Def2;
for t being c-Term of F2(),F3() st t in rng p holds
P1[t] by A6;
hence P1[nt -tree ts] by A3, A7, A9, A8; ::_thesis: verum
end;
A10: for s being Symbol of (DTConMSA ( the Sorts of F2() \/ F3())) st s in Terminals (DTConMSA ( the Sorts of F2() \/ F3())) holds
P1[ root-tree s]
proof
let x be Symbol of (DTConMSA ( the Sorts of F2() \/ F3())); ::_thesis: ( x in Terminals (DTConMSA ( the Sorts of F2() \/ F3())) implies P1[ root-tree x] )
assume x in Terminals (DTConMSA ( the Sorts of F2() \/ F3())) ; ::_thesis: P1[ root-tree x]
then ( ex s being SortSymbol of F1() ex a being set st
( a in the Sorts of F2() . s & x = [a,s] ) or ex s being SortSymbol of F1() ex v being Element of F3() . s st x = [v,s] ) by Lm4;
hence P1[ root-tree x] by A1, A2; ::_thesis: verum
end;
for t being DecoratedTree of the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) st t in TS (DTConMSA ( the Sorts of F2() \/ F3())) holds
P1[t] from DTCONSTR:sch_7(A10, A4);
hence for t being c-Term of F2(),F3() holds P1[t] ; ::_thesis: verum
end;
definition
let S be non empty non void ManySortedSign ;
let V be V16() ManySortedSet of the carrier of S;
let t be Term of S,V;
let p be Node of t;
:: original: .
redefine funct . p -> Symbol of (DTConMSA V);
coherence
t . p is Symbol of (DTConMSA V)
proof
reconsider t = t as Element of TS (DTConMSA V) ;
reconsider t = t as DecoratedTree of the carrier of (DTConMSA V) ;
reconsider p = p as Node of t ;
t . p = t . p ;
hence t . p is Symbol of (DTConMSA V) ; ::_thesis: verum
end;
end;
registration
let S be non empty non void ManySortedSign ;
let V be V16() ManySortedSet of the carrier of S;
cluster -> finite for Element of S -Terms V;
coherence
for b1 being Term of S,V holds b1 is finite ;
end;
Lm6: now__::_thesis:_for_G_being_non_empty_with_terminals_with_nonterminals_DTConstrStr_
for_s_being_Symbol_of_G_holds_
(_(_s_is_Terminal_of_G_or_s_is_NonTerminal_of_G_)_&_(_not_s_is_Terminal_of_G_or_not_s_is_NonTerminal_of_G_)_)
let G be non empty with_terminals with_nonterminals DTConstrStr ; ::_thesis: for s being Symbol of G holds
( ( s is Terminal of G or s is NonTerminal of G ) & ( not s is Terminal of G or not s is NonTerminal of G ) )
let s be Symbol of G; ::_thesis: ( ( s is Terminal of G or s is NonTerminal of G ) & ( not s is Terminal of G or not s is NonTerminal of G ) )
the carrier of G = (Terminals G) \/ (NonTerminals G) by LANG1:1;
hence ( s is Terminal of G or s is NonTerminal of G ) by XBOOLE_0:def_3; ::_thesis: ( not s is Terminal of G or not s is NonTerminal of G )
Terminals G misses NonTerminals G by DTCONSTR:8;
hence ( not s is Terminal of G or not s is NonTerminal of G ) by XBOOLE_0:3; ::_thesis: verum
end;
theorem Th2: :: MSATERM:2
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V holds
( ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V holds
( ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] )
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,V holds
( ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] )
let t be Term of S,V; ::_thesis: ( ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] )
set G = DTConMSA V;
A1: the carrier of (DTConMSA V) = (Terminals (DTConMSA V)) \/ (NonTerminals (DTConMSA V)) by LANG1:1;
reconsider e = {} as Node of t by TREES_1:22;
NonTerminals (DTConMSA V) = [: the carrier' of S,{ the carrier of S}:] by MSAFREE:6;
then ( t . e in Terminals (DTConMSA V) or t . e in [: the carrier' of S,{ the carrier of S}:] ) by A1, XBOOLE_0:def_3;
hence ( ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] ) by Lm3; ::_thesis: verum
end;
theorem :: MSATERM:3
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for t being c-Term of A,V holds
( ex s being SortSymbol of S ex x being set st
( x in the Sorts of A . s & t . {} = [x,s] ) or ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for t being c-Term of A,V holds
( ex s being SortSymbol of S ex x being set st
( x in the Sorts of A . s & t . {} = [x,s] ) or ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] )
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for A being MSAlgebra over S
for t being c-Term of A,V holds
( ex s being SortSymbol of S ex x being set st
( x in the Sorts of A . s & t . {} = [x,s] ) or ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] )
let A be MSAlgebra over S; ::_thesis: for t being c-Term of A,V holds
( ex s being SortSymbol of S ex x being set st
( x in the Sorts of A . s & t . {} = [x,s] ) or ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] )
let t be c-Term of A,V; ::_thesis: ( ex s being SortSymbol of S ex x being set st
( x in the Sorts of A . s & t . {} = [x,s] ) or ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] )
set G = DTConMSA ( the Sorts of A \/ V);
A1: the carrier of (DTConMSA ( the Sorts of A \/ V)) = (Terminals (DTConMSA ( the Sorts of A \/ V))) \/ (NonTerminals (DTConMSA ( the Sorts of A \/ V))) by LANG1:1;
reconsider e = {} as Node of t by TREES_1:22;
NonTerminals (DTConMSA ( the Sorts of A \/ V)) = [: the carrier' of S,{ the carrier of S}:] by MSAFREE:6;
then ( t . e in Terminals (DTConMSA ( the Sorts of A \/ V)) or t . e in [: the carrier' of S,{ the carrier of S}:] ) by A1, XBOOLE_0:def_3;
hence ( ex s being SortSymbol of S ex x being set st
( x in the Sorts of A . s & t . {} = [x,s] ) or ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] ) by Lm4; ::_thesis: verum
end;
theorem Th4: :: MSATERM:4
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for s being SortSymbol of S
for v being Element of V . s holds root-tree [v,s] is Term of S,V
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for s being SortSymbol of S
for v being Element of V . s holds root-tree [v,s] is Term of S,V
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for s being SortSymbol of S
for v being Element of V . s holds root-tree [v,s] is Term of S,V
let s be SortSymbol of S; ::_thesis: for v being Element of V . s holds root-tree [v,s] is Term of S,V
let v be Element of V . s; ::_thesis: root-tree [v,s] is Term of S,V
reconsider vs = [v,s] as Terminal of (DTConMSA V) by MSAFREE:7;
root-tree vs in TS (DTConMSA V) ;
hence root-tree [v,s] is Term of S,V ; ::_thesis: verum
end;
theorem Th5: :: MSATERM:5
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V
for s being SortSymbol of S
for v being Element of V . s st t . {} = [v,s] holds
t = root-tree [v,s]
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V
for s being SortSymbol of S
for v being Element of V . s st t . {} = [v,s] holds
t = root-tree [v,s]
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,V
for s being SortSymbol of S
for v being Element of V . s st t . {} = [v,s] holds
t = root-tree [v,s]
let t be Term of S,V; ::_thesis: for s being SortSymbol of S
for v being Element of V . s st t . {} = [v,s] holds
t = root-tree [v,s]
let s be SortSymbol of S; ::_thesis: for v being Element of V . s st t . {} = [v,s] holds
t = root-tree [v,s]
let x be Element of V . s; ::_thesis: ( t . {} = [x,s] implies t = root-tree [x,s] )
set G = DTConMSA V;
reconsider a = [x,s] as Terminal of (DTConMSA V) by Lm3;
reconsider t = t as Element of TS (DTConMSA V) ;
( t . {} = a implies t = root-tree a ) by DTCONSTR:9;
hence ( t . {} = [x,s] implies t = root-tree [x,s] ) ; ::_thesis: verum
end;
theorem Th6: :: MSATERM:6
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for s being SortSymbol of S
for x being set st x in the Sorts of A . s holds
root-tree [x,s] is c-Term of A,V
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for s being SortSymbol of S
for x being set st x in the Sorts of A . s holds
root-tree [x,s] is c-Term of A,V
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for A being MSAlgebra over S
for s being SortSymbol of S
for x being set st x in the Sorts of A . s holds
root-tree [x,s] is c-Term of A,V
let A be MSAlgebra over S; ::_thesis: for s being SortSymbol of S
for x being set st x in the Sorts of A . s holds
root-tree [x,s] is c-Term of A,V
let s be SortSymbol of S; ::_thesis: for x being set st x in the Sorts of A . s holds
root-tree [x,s] is c-Term of A,V
let x be set ; ::_thesis: ( x in the Sorts of A . s implies root-tree [x,s] is c-Term of A,V )
A1: ( the Sorts of A \/ V) . s = ( the Sorts of A . s) \/ (V . s) by PBOOLE:def_4;
assume x in the Sorts of A . s ; ::_thesis: root-tree [x,s] is c-Term of A,V
then x in ( the Sorts of A \/ V) . s by A1, XBOOLE_0:def_3;
then reconsider xs = [x,s] as Terminal of (DTConMSA ( the Sorts of A \/ V)) by MSAFREE:7;
root-tree xs in TS (DTConMSA ( the Sorts of A \/ V)) ;
hence root-tree [x,s] is c-Term of A,V ; ::_thesis: verum
end;
theorem :: MSATERM:7
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for t being c-Term of A,V
for s being SortSymbol of S
for x being set st x in the Sorts of A . s & t . {} = [x,s] holds
t = root-tree [x,s]
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for t being c-Term of A,V
for s being SortSymbol of S
for x being set st x in the Sorts of A . s & t . {} = [x,s] holds
t = root-tree [x,s]
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for A being MSAlgebra over S
for t being c-Term of A,V
for s being SortSymbol of S
for x being set st x in the Sorts of A . s & t . {} = [x,s] holds
t = root-tree [x,s]
let A be MSAlgebra over S; ::_thesis: for t being c-Term of A,V
for s being SortSymbol of S
for x being set st x in the Sorts of A . s & t . {} = [x,s] holds
t = root-tree [x,s]
let t be c-Term of A,V; ::_thesis: for s being SortSymbol of S
for x being set st x in the Sorts of A . s & t . {} = [x,s] holds
t = root-tree [x,s]
let s be SortSymbol of S; ::_thesis: for x being set st x in the Sorts of A . s & t . {} = [x,s] holds
t = root-tree [x,s]
let x be set ; ::_thesis: ( x in the Sorts of A . s & t . {} = [x,s] implies t = root-tree [x,s] )
set G = DTConMSA ( the Sorts of A \/ V);
reconsider t = t as Element of TS (DTConMSA ( the Sorts of A \/ V)) ;
assume x in the Sorts of A . s ; ::_thesis: ( not t . {} = [x,s] or t = root-tree [x,s] )
then reconsider a = [x,s] as Terminal of (DTConMSA ( the Sorts of A \/ V)) by Lm4;
( t . {} = a implies t = root-tree a ) by DTCONSTR:9;
hence ( not t . {} = [x,s] or t = root-tree [x,s] ) ; ::_thesis: verum
end;
theorem Th8: :: MSATERM:8
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for s being SortSymbol of S
for v being Element of V . s holds root-tree [v,s] is c-Term of A,V
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for s being SortSymbol of S
for v being Element of V . s holds root-tree [v,s] is c-Term of A,V
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for A being MSAlgebra over S
for s being SortSymbol of S
for v being Element of V . s holds root-tree [v,s] is c-Term of A,V
let A be MSAlgebra over S; ::_thesis: for s being SortSymbol of S
for v being Element of V . s holds root-tree [v,s] is c-Term of A,V
let s be SortSymbol of S; ::_thesis: for v being Element of V . s holds root-tree [v,s] is c-Term of A,V
let v be Element of V . s; ::_thesis: root-tree [v,s] is c-Term of A,V
( the Sorts of A \/ V) . s = ( the Sorts of A . s) \/ (V . s) by PBOOLE:def_4;
then v in ( the Sorts of A \/ V) . s by XBOOLE_0:def_3;
then reconsider vs = [v,s] as Terminal of (DTConMSA ( the Sorts of A \/ V)) by MSAFREE:7;
root-tree vs in TS (DTConMSA ( the Sorts of A \/ V)) ;
hence root-tree [v,s] is c-Term of A,V ; ::_thesis: verum
end;
theorem :: MSATERM:9
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for t being c-Term of A,V
for s being SortSymbol of S
for v being Element of V . s st t . {} = [v,s] holds
t = root-tree [v,s]
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for t being c-Term of A,V
for s being SortSymbol of S
for v being Element of V . s st t . {} = [v,s] holds
t = root-tree [v,s]
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for A being MSAlgebra over S
for t being c-Term of A,V
for s being SortSymbol of S
for v being Element of V . s st t . {} = [v,s] holds
t = root-tree [v,s]
let A be MSAlgebra over S; ::_thesis: for t being c-Term of A,V
for s being SortSymbol of S
for v being Element of V . s st t . {} = [v,s] holds
t = root-tree [v,s]
let t be c-Term of A,V; ::_thesis: for s being SortSymbol of S
for v being Element of V . s st t . {} = [v,s] holds
t = root-tree [v,s]
let s be SortSymbol of S; ::_thesis: for v being Element of V . s st t . {} = [v,s] holds
t = root-tree [v,s]
let x be Element of V . s; ::_thesis: ( t . {} = [x,s] implies t = root-tree [x,s] )
set G = DTConMSA ( the Sorts of A \/ V);
reconsider a = [x,s] as Terminal of (DTConMSA ( the Sorts of A \/ V)) by Lm4;
reconsider t = t as Element of TS (DTConMSA ( the Sorts of A \/ V)) ;
( t . {} = a implies t = root-tree a ) by DTCONSTR:9;
hence ( t . {} = [x,s] implies t = root-tree [x,s] ) ; ::_thesis: verum
end;
theorem Th10: :: MSATERM:10
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V
for o being OperSymbol of S st t . {} = [o, the carrier of S] holds
ex a being ArgumentSeq of Sym (o,V) st t = [o, the carrier of S] -tree a
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V
for o being OperSymbol of S st t . {} = [o, the carrier of S] holds
ex a being ArgumentSeq of Sym (o,V) st t = [o, the carrier of S] -tree a
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,V
for o being OperSymbol of S st t . {} = [o, the carrier of S] holds
ex a being ArgumentSeq of Sym (o,V) st t = [o, the carrier of S] -tree a
let t be Term of S,V; ::_thesis: for o being OperSymbol of S st t . {} = [o, the carrier of S] holds
ex a being ArgumentSeq of Sym (o,V) st t = [o, the carrier of S] -tree a
let o be OperSymbol of S; ::_thesis: ( t . {} = [o, the carrier of S] implies ex a being ArgumentSeq of Sym (o,V) st t = [o, the carrier of S] -tree a )
assume A1: t . {} = [o, the carrier of S] ; ::_thesis: ex a being ArgumentSeq of Sym (o,V) st t = [o, the carrier of S] -tree a
set X = V;
set G = DTConMSA V;
reconsider t = t as Element of TS (DTConMSA V) ;
[o, the carrier of S] = Sym (o,V) by MSAFREE:def_9;
then consider p being FinSequence of TS (DTConMSA V) such that
A2: t = (Sym (o,V)) -tree p and
A3: Sym (o,V) ==> roots p by A1, DTCONSTR:10;
reconsider a = p as FinSequence of S -Terms V ;
a is SubtreeSeq of Sym (o,V) by A3, DTCONSTR:def_6;
then reconsider a = a as ArgumentSeq of Sym (o,V) by Def2;
take a ; ::_thesis: t = [o, the carrier of S] -tree a
thus t = [o, the carrier of S] -tree a by A2, MSAFREE:def_9; ::_thesis: verum
end;
definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let V be V16() ManySortedSet of the carrier of S;
let s be SortSymbol of S;
let x be Element of the Sorts of A . s;
funcx -term (A,V) -> c-Term of A,V equals :: MSATERM:def 3
root-tree [x,s];
correctness
coherence
root-tree [x,s] is c-Term of A,V;
by Th6;
end;
:: deftheorem defines -term MSATERM:def_3_:_
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being V16() ManySortedSet of the carrier of S
for s being SortSymbol of S
for x being Element of the Sorts of A . s holds x -term (A,V) = root-tree [x,s];
definition
let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
let V be V16() ManySortedSet of the carrier of S;
let s be SortSymbol of S;
let v be Element of V . s;
funcv -term A -> c-Term of A,V equals :: MSATERM:def 4
root-tree [v,s];
correctness
coherence
root-tree [v,s] is c-Term of A,V;
by Th8;
end;
:: deftheorem defines -term MSATERM:def_4_:_
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for V being V16() ManySortedSet of the carrier of S
for s being SortSymbol of S
for v being Element of V . s holds v -term A = root-tree [v,s];
definition
let S be non empty non void ManySortedSign ;
let V be V16() ManySortedSet of the carrier of S;
let sy be NonTerminal of (DTConMSA V);
let p be ArgumentSeq of sy;
:: original: -tree
redefine funcsy -tree p -> Term of S,V;
coherence
sy -tree p is Term of S,V
proof
sy in [: the carrier' of S,{ the carrier of S}:] by Lm5;
then consider o being OperSymbol of S, x2 being Element of { the carrier of S} such that
A1: sy = [o,x2] by DOMAIN_1:1;
A2: x2 = the carrier of S by TARSKI:def_1;
then sy = Sym (o,V) by A1, MSAFREE:def_9;
hence sy -tree p is Term of S,V by A1, A2, Th1; ::_thesis: verum
end;
end;
scheme :: MSATERM:sch 3
TermInd2{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), F3() -> V16() ManySortedSet of the carrier of F1(), P1[ set ] } :
for t being c-Term of F2(),F3() holds P1[t]
provided
A1: for s being SortSymbol of F1()
for x being Element of the Sorts of F2() . s holds P1[x -term (F2(),F3())] and
A2: for s being SortSymbol of F1()
for v being Element of F3() . s holds P1[v -term F2()] and
A3: for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,( the Sorts of F2() \/ F3())) st ( for t being c-Term of F2(),F3() st t in rng p holds
P1[t] ) holds
P1[(Sym (o,( the Sorts of F2() \/ F3()))) -tree p]
proof
A4: now__::_thesis:_for_s_being_SortSymbol_of_F1()
for_x_being_Element_of_the_Sorts_of_F2()_._s_holds_P1[_root-tree_[x,s]]
let s be SortSymbol of F1(); ::_thesis: for x being Element of the Sorts of F2() . s holds P1[ root-tree [x,s]]
let x be Element of the Sorts of F2() . s; ::_thesis: P1[ root-tree [x,s]]
P1[x -term (F2(),F3())] by A1;
hence P1[ root-tree [x,s]] ; ::_thesis: verum
end;
A5: now__::_thesis:_for_s_being_SortSymbol_of_F1()
for_v_being_Element_of_F3()_._s_holds_P1[_root-tree_[v,s]]
let s be SortSymbol of F1(); ::_thesis: for v being Element of F3() . s holds P1[ root-tree [v,s]]
let v be Element of F3() . s; ::_thesis: P1[ root-tree [v,s]]
P1[v -term F2()] by A2;
hence P1[ root-tree [v,s]] ; ::_thesis: verum
end;
A6: for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,( the Sorts of F2() \/ F3())) st ( for t being c-Term of F2(),F3() st t in rng p holds
P1[t] ) holds
P1[(Sym (o,( the Sorts of F2() \/ F3()))) -tree p] by A3;
for t being c-Term of F2(),F3() holds P1[t] from MSATERM:sch_2(A4, A5, A6);
hence for t being c-Term of F2(),F3() holds P1[t] ; ::_thesis: verum
end;
begin
theorem Th11: :: MSATERM:11
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V ex s being SortSymbol of S st t in FreeSort (V,s)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V ex s being SortSymbol of S st t in FreeSort (V,s)
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,V ex s being SortSymbol of S st t in FreeSort (V,s)
let t be Term of S,V; ::_thesis: ex s being SortSymbol of S st t in FreeSort (V,s)
set X = V;
set G = DTConMSA V;
reconsider e = {} as Node of t by TREES_1:22;
percases ( t . {} is Terminal of (DTConMSA V) or not t . {} is Terminal of (DTConMSA V) ) ;
suppose t . {} is Terminal of (DTConMSA V) ; ::_thesis: ex s being SortSymbol of S st t in FreeSort (V,s)
then reconsider ts = t . {} as Terminal of (DTConMSA V) ;
consider s being SortSymbol of S, x being set such that
A1: x in V . s and
A2: ts = [x,s] by MSAFREE:7;
take s ; ::_thesis: t in FreeSort (V,s)
t = root-tree [x,s] by A2, DTCONSTR:9;
then t in { a where a is Element of TS (DTConMSA V) : ( ex x being set st
( x in V . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } by A1;
hence t in FreeSort (V,s) by MSAFREE:def_10; ::_thesis: verum
end;
suppose t . {} is not Terminal of (DTConMSA V) ; ::_thesis: ex s being SortSymbol of S st t in FreeSort (V,s)
then reconsider nt = t . e as NonTerminal of (DTConMSA V) by Lm6;
nt in [: the carrier' of S,{ the carrier of S}:] by Lm5;
then consider o being OperSymbol of S, x2 being Element of { the carrier of S} such that
A3: nt = [o,x2] by DOMAIN_1:1;
take s = the_result_sort_of o; ::_thesis: t in FreeSort (V,s)
x2 = the carrier of S by TARSKI:def_1;
then t in { a where a is Element of TS (DTConMSA V) : ( ex x being set st
( x in V . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } by A3;
hence t in FreeSort (V,s) by MSAFREE:def_10; ::_thesis: verum
end;
end;
end;
theorem :: MSATERM:12
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for s being SortSymbol of S holds FreeSort (V,s) c= S -Terms V ;
theorem :: MSATERM:13
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S holds S -Terms V = Union (FreeSort V)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S holds S -Terms V = Union (FreeSort V)
let V be V16() ManySortedSet of the carrier of S; ::_thesis: S -Terms V = Union (FreeSort V)
set T = S -Terms V;
set X = V;
A1: dom (FreeSort V) = the carrier of S by PARTFUN1:def_2;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: Union (FreeSort V) c= S -Terms V
let x be set ; ::_thesis: ( x in S -Terms V implies x in Union (FreeSort V) )
assume x in S -Terms V ; ::_thesis: x in Union (FreeSort V)
then reconsider t = x as Term of S,V ;
consider s being SortSymbol of S such that
A2: t in FreeSort (V,s) by Th11;
FreeSort (V,s) = (FreeSort V) . s by MSAFREE:def_11;
hence x in Union (FreeSort V) by A1, A2, CARD_5:2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union (FreeSort V) or x in S -Terms V )
assume x in Union (FreeSort V) ; ::_thesis: x in S -Terms V
then consider y being set such that
A3: y in dom (FreeSort V) and
A4: x in (FreeSort V) . y by CARD_5:2;
reconsider y = y as SortSymbol of S by A3, PARTFUN1:def_2;
x in FreeSort (V,y) by A4, MSAFREE:def_11;
hence x in S -Terms V ; ::_thesis: verum
end;
Lm7: for x being set holds not x in x
;
definition
let S be non empty non void ManySortedSign ;
let V be V16() ManySortedSet of the carrier of S;
let t be Term of S,V;
func the_sort_of t -> SortSymbol of S means :Def5: :: MSATERM:def 5
t in FreeSort (V,it);
existence
ex b1 being SortSymbol of S st t in FreeSort (V,b1) by Th11;
uniqueness
for b1, b2 being SortSymbol of S st t in FreeSort (V,b1) & t in FreeSort (V,b2) holds
b1 = b2
proof
set X = V;
let s1, s2 be SortSymbol of S; ::_thesis: ( t in FreeSort (V,s1) & t in FreeSort (V,s2) implies s1 = s2 )
assume that
A1: t in FreeSort (V,s1) and
A2: t in FreeSort (V,s2) ; ::_thesis: s1 = s2
FreeSort (V,s1) = { a where a is Element of TS (DTConMSA V) : ( ex x being set st
( x in V . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = s1 ) ) } by MSAFREE:def_10;
then consider a1 being Element of TS (DTConMSA V) such that
A3: t = a1 and
A4: ( ex x being set st
( x in V . s1 & a1 = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a1 . {} & the_result_sort_of o = s1 ) ) by A1;
FreeSort (V,s2) = { a where a is Element of TS (DTConMSA V) : ( ex x being set st
( x in V . s2 & a = root-tree [x,s2] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = s2 ) ) } by MSAFREE:def_10;
then consider a2 being Element of TS (DTConMSA V) such that
A5: t = a2 and
A6: ( ex x being set st
( x in V . s2 & a2 = root-tree [x,s2] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a2 . {} & the_result_sort_of o = s2 ) ) by A2;
percases ( ex x being set st
( x in V . s1 & a1 = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a1 . {} & the_result_sort_of o = s1 ) ) by A4;
suppose ex x being set st
( x in V . s1 & a1 = root-tree [x,s1] ) ; ::_thesis: s1 = s2
then consider x1 being set such that
x1 in V . s1 and
A7: a1 = root-tree [x1,s1] ;
now__::_thesis:_for_o_being_OperSymbol_of_S_holds_not_[o,_the_carrier_of_S]_=_[x1,s1]
let o be OperSymbol of S; ::_thesis: not [o, the carrier of S] = [x1,s1]
assume [o, the carrier of S] = [x1,s1] ; ::_thesis: contradiction
then the carrier of S = s1 by XTUPLE_0:1;
hence contradiction by Lm7; ::_thesis: verum
end;
then consider x2 being set such that
x2 in V . s2 and
A8: a2 = root-tree [x2,s2] by A3, A5, A6, A7, TREES_4:3;
[x1,s1] = [x2,s2] by A3, A5, A7, A8, TREES_4:4;
hence s1 = s2 by XTUPLE_0:1; ::_thesis: verum
end;
suppose ex o being OperSymbol of S st
( [o, the carrier of S] = a1 . {} & the_result_sort_of o = s1 ) ; ::_thesis: s1 = s2
then consider o1 being OperSymbol of S such that
A9: [o1, the carrier of S] = a1 . {} and
A10: the_result_sort_of o1 = s1 ;
now__::_thesis:_for_x2_being_set_holds_
(_not_x2_in_V_._s2_or_not_a2_=_root-tree_[x2,s2]_)
given x2 being set such that x2 in V . s2 and
A11: a2 = root-tree [x2,s2] ; ::_thesis: contradiction
[o1, the carrier of S] = [x2,s2] by A3, A5, A9, A11, TREES_4:3;
then the carrier of S = s2 by XTUPLE_0:1;
hence contradiction by Lm7; ::_thesis: verum
end;
hence s1 = s2 by A3, A5, A6, A9, A10, XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
end;
:: deftheorem Def5 defines the_sort_of MSATERM:def_5_:_
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V
for b4 being SortSymbol of S holds
( b4 = the_sort_of t iff t in FreeSort (V,b4) );
theorem Th14: :: MSATERM:14
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V
for s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
the_sort_of t = s
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V
for s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
the_sort_of t = s
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,V
for s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
the_sort_of t = s
let t be Term of S,V; ::_thesis: for s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
the_sort_of t = s
let s be SortSymbol of S; ::_thesis: for v being Element of V . s st t = root-tree [v,s] holds
the_sort_of t = s
let x be Element of V . s; ::_thesis: ( t = root-tree [x,s] implies the_sort_of t = s )
set X = V;
set G = DTConMSA V;
set tst = the_sort_of t;
A1: FreeSort (V,(the_sort_of t)) = { a where a is Element of TS (DTConMSA V) : ( ex x being set st
( x in V . (the_sort_of t) & a = root-tree [x,(the_sort_of t)] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = the_sort_of t ) ) } by MSAFREE:def_10;
t in FreeSort (V,(the_sort_of t)) by Def5;
then consider a being Element of TS (DTConMSA V) such that
A2: t = a and
A3: ( ex x being set st
( x in V . (the_sort_of t) & a = root-tree [x,(the_sort_of t)] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = the_sort_of t ) ) by A1;
A4: [x,s] in Terminals (DTConMSA V) by Lm3;
assume A5: t = root-tree [x,s] ; ::_thesis: the_sort_of t = s
then t . {} = [x,s] by TREES_4:3;
then t . {} is not NonTerminal of (DTConMSA V) by A4, Lm6;
then A6: not t . {} in [: the carrier' of S,{ the carrier of S}:] by Lm5;
the carrier of S in { the carrier of S} by TARSKI:def_1;
then consider y being set such that
y in V . (the_sort_of t) and
A7: a = root-tree [y,(the_sort_of t)] by A2, A3, A6, ZFMISC_1:87;
[y,(the_sort_of t)] = [x,s] by A2, A5, A7, TREES_4:4;
hence the_sort_of t = s by XTUPLE_0:1; ::_thesis: verum
end;
theorem Th15: :: MSATERM:15
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for t being c-Term of A,V
for s being SortSymbol of S
for x being set st x in the Sorts of A . s & t = root-tree [x,s] holds
the_sort_of t = s
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for t being c-Term of A,V
for s being SortSymbol of S
for x being set st x in the Sorts of A . s & t = root-tree [x,s] holds
the_sort_of t = s
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for A being MSAlgebra over S
for t being c-Term of A,V
for s being SortSymbol of S
for x being set st x in the Sorts of A . s & t = root-tree [x,s] holds
the_sort_of t = s
let A be MSAlgebra over S; ::_thesis: for t being c-Term of A,V
for s being SortSymbol of S
for x being set st x in the Sorts of A . s & t = root-tree [x,s] holds
the_sort_of t = s
let t be c-Term of A,V; ::_thesis: for s being SortSymbol of S
for x being set st x in the Sorts of A . s & t = root-tree [x,s] holds
the_sort_of t = s
let s be SortSymbol of S; ::_thesis: for x being set st x in the Sorts of A . s & t = root-tree [x,s] holds
the_sort_of t = s
let x be set ; ::_thesis: ( x in the Sorts of A . s & t = root-tree [x,s] implies the_sort_of t = s )
assume x in the Sorts of A . s ; ::_thesis: ( not t = root-tree [x,s] or the_sort_of t = s )
then x in ( the Sorts of A . s) \/ (V . s) by XBOOLE_0:def_3;
then x in ( the Sorts of A \/ V) . s by PBOOLE:def_4;
hence ( not t = root-tree [x,s] or the_sort_of t = s ) by Th14; ::_thesis: verum
end;
theorem :: MSATERM:16
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for t being c-Term of A,V
for s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
the_sort_of t = s
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for t being c-Term of A,V
for s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
the_sort_of t = s
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for A being MSAlgebra over S
for t being c-Term of A,V
for s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
the_sort_of t = s
let A be MSAlgebra over S; ::_thesis: for t being c-Term of A,V
for s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
the_sort_of t = s
let t be c-Term of A,V; ::_thesis: for s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
the_sort_of t = s
let s be SortSymbol of S; ::_thesis: for v being Element of V . s st t = root-tree [v,s] holds
the_sort_of t = s
let x be Element of V . s; ::_thesis: ( t = root-tree [x,s] implies the_sort_of t = s )
x in ( the Sorts of A . s) \/ (V . s) by XBOOLE_0:def_3;
then x in ( the Sorts of A \/ V) . s by PBOOLE:def_4;
hence ( t = root-tree [x,s] implies the_sort_of t = s ) by Th14; ::_thesis: verum
end;
theorem Th17: :: MSATERM:17
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V
for o being OperSymbol of S st t . {} = [o, the carrier of S] holds
the_sort_of t = the_result_sort_of o
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V
for o being OperSymbol of S st t . {} = [o, the carrier of S] holds
the_sort_of t = the_result_sort_of o
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,V
for o being OperSymbol of S st t . {} = [o, the carrier of S] holds
the_sort_of t = the_result_sort_of o
let t be Term of S,V; ::_thesis: for o being OperSymbol of S st t . {} = [o, the carrier of S] holds
the_sort_of t = the_result_sort_of o
let o be OperSymbol of S; ::_thesis: ( t . {} = [o, the carrier of S] implies the_sort_of t = the_result_sort_of o )
set X = V;
set G = DTConMSA V;
set tst = the_sort_of t;
A1: FreeSort (V,(the_sort_of t)) = { a where a is Element of TS (DTConMSA V) : ( ex x being set st
( x in V . (the_sort_of t) & a = root-tree [x,(the_sort_of t)] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = the_sort_of t ) ) } by MSAFREE:def_10;
t in FreeSort (V,(the_sort_of t)) by Def5;
then consider a being Element of TS (DTConMSA V) such that
A2: t = a and
A3: ( ex x being set st
( x in V . (the_sort_of t) & a = root-tree [x,(the_sort_of t)] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = the_sort_of t ) ) by A1;
assume A4: t . {} = [o, the carrier of S] ; ::_thesis: the_sort_of t = the_result_sort_of o
percases ( ex x being set st
( x in V . (the_sort_of t) & a = root-tree [x,(the_sort_of t)] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = the_sort_of t ) ) by A3;
suppose ex x being set st
( x in V . (the_sort_of t) & a = root-tree [x,(the_sort_of t)] ) ; ::_thesis: the_sort_of t = the_result_sort_of o
then consider x being set such that
x in V . (the_sort_of t) and
A5: a = root-tree [x,(the_sort_of t)] ;
[o, the carrier of S] = [x,(the_sort_of t)] by A2, A4, A5, TREES_4:3;
then the carrier of S = the_sort_of t by XTUPLE_0:1;
hence the_sort_of t = the_result_sort_of o by Lm7; ::_thesis: verum
end;
suppose ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = the_sort_of t ) ; ::_thesis: the_sort_of t = the_result_sort_of o
hence the_sort_of t = the_result_sort_of o by A2, A4, XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
theorem :: MSATERM:18
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for A being non-empty MSAlgebra over S
for s being SortSymbol of S
for x being Element of the Sorts of A . s holds the_sort_of (x -term (A,V)) = s by Th15;
theorem Th19: :: MSATERM:19
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for s being SortSymbol of S
for v being Element of V . s holds the_sort_of (v -term A) = s
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for s being SortSymbol of S
for v being Element of V . s holds the_sort_of (v -term A) = s
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for A being MSAlgebra over S
for s being SortSymbol of S
for v being Element of V . s holds the_sort_of (v -term A) = s
let A be MSAlgebra over S; ::_thesis: for s being SortSymbol of S
for v being Element of V . s holds the_sort_of (v -term A) = s
let s be SortSymbol of S; ::_thesis: for v being Element of V . s holds the_sort_of (v -term A) = s
let v be Element of V . s; ::_thesis: the_sort_of (v -term A) = s
( the Sorts of A \/ V) . s = ( the Sorts of A . s) \/ (V . s) by PBOOLE:def_4;
then v in ( the Sorts of A \/ V) . s by XBOOLE_0:def_3;
hence the_sort_of (v -term A) = s by Th14; ::_thesis: verum
end;
theorem Th20: :: MSATERM:20
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,V) holds the_sort_of ((Sym (o,V)) -tree p) = the_result_sort_of o
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,V) holds the_sort_of ((Sym (o,V)) -tree p) = the_result_sort_of o
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,V) holds the_sort_of ((Sym (o,V)) -tree p) = the_result_sort_of o
let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of Sym (o,V) holds the_sort_of ((Sym (o,V)) -tree p) = the_result_sort_of o
let p be ArgumentSeq of Sym (o,V); ::_thesis: the_sort_of ((Sym (o,V)) -tree p) = the_result_sort_of o
A1: ([o, the carrier of S] -tree p) . {} = [o, the carrier of S] by TREES_4:def_4;
[o, the carrier of S] = Sym (o,V) by MSAFREE:def_9;
hence the_sort_of ((Sym (o,V)) -tree p) = the_result_sort_of o by A1, Th17; ::_thesis: verum
end;
begin
theorem Th21: :: MSATERM:21
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being FinSequence of S -Terms V holds
( a is ArgumentSeq of Sym (o,V) iff Sym (o,V) ==> roots a )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being FinSequence of S -Terms V holds
( a is ArgumentSeq of Sym (o,V) iff Sym (o,V) ==> roots a )
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for o being OperSymbol of S
for a being FinSequence of S -Terms V holds
( a is ArgumentSeq of Sym (o,V) iff Sym (o,V) ==> roots a )
let o be OperSymbol of S; ::_thesis: for a being FinSequence of S -Terms V holds
( a is ArgumentSeq of Sym (o,V) iff Sym (o,V) ==> roots a )
let a be FinSequence of S -Terms V; ::_thesis: ( a is ArgumentSeq of Sym (o,V) iff Sym (o,V) ==> roots a )
( a is SubtreeSeq of Sym (o,V) iff Sym (o,V) ==> roots a ) by DTCONSTR:def_6;
hence ( a is ArgumentSeq of Sym (o,V) iff Sym (o,V) ==> roots a ) by Def2; ::_thesis: verum
end;
Lm8: for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being ArgumentSeq of Sym (o,V) holds
( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) & ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) ) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being ArgumentSeq of Sym (o,V) holds
( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) & ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) ) )
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for o being OperSymbol of S
for a being ArgumentSeq of Sym (o,V) holds
( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) & ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) ) )
let o be OperSymbol of S; ::_thesis: for a being ArgumentSeq of Sym (o,V) holds
( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) & ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) ) )
let a be ArgumentSeq of Sym (o,V); ::_thesis: ( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) & ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) ) )
set X = V;
reconsider p = a as FinSequence of TS (DTConMSA V) by Def1;
Sym (o,V) ==> roots a by Th21;
then A1: p in (((FreeSort V) #) * the Arity of S) . o by MSAFREE:10;
then A2: dom p = dom (the_arity_of o) by MSAFREE:9;
hence ( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) ) by FINSEQ_3:29; ::_thesis: for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i )
let i be Nat; ::_thesis: ( i in dom a implies ex t being Term of S,V st
( t = a . i & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) )
reconsider t = a /. i as Term of S,V ;
assume A3: i in dom a ; ::_thesis: ex t being Term of S,V st
( t = a . i & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i )
then A4: i <= len a by FINSEQ_3:25;
take t ; ::_thesis: ( t = a . i & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i )
1 <= i by A3, FINSEQ_3:25;
hence t = a . i by A4, FINSEQ_4:15; ::_thesis: ( t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i )
then t in FreeSort (V,((the_arity_of o) /. i)) by A1, A3, MSAFREE:9;
then the_sort_of t = (the_arity_of o) /. i by Def5;
hence ( t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) by A2, A3, PARTFUN1:def_6; ::_thesis: verum
end;
theorem Th22: :: MSATERM:22
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being ArgumentSeq of Sym (o,V) holds
( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) & ( for i being Nat st i in dom a holds
a . i is Term of S,V ) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being ArgumentSeq of Sym (o,V) holds
( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) & ( for i being Nat st i in dom a holds
a . i is Term of S,V ) )
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for o being OperSymbol of S
for a being ArgumentSeq of Sym (o,V) holds
( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) & ( for i being Nat st i in dom a holds
a . i is Term of S,V ) )
let o be OperSymbol of S; ::_thesis: for a being ArgumentSeq of Sym (o,V) holds
( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) & ( for i being Nat st i in dom a holds
a . i is Term of S,V ) )
let a be ArgumentSeq of Sym (o,V); ::_thesis: ( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) & ( for i being Nat st i in dom a holds
a . i is Term of S,V ) )
thus ( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) ) by Lm8; ::_thesis: for i being Nat st i in dom a holds
a . i is Term of S,V
let i be Nat; ::_thesis: ( i in dom a implies a . i is Term of S,V )
assume i in dom a ; ::_thesis: a . i is Term of S,V
then ex t being Term of S,V st
( t = a . i & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) by Lm8;
hence a . i is Term of S,V ; ::_thesis: verum
end;
theorem :: MSATERM:23
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being ArgumentSeq of Sym (o,V)
for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
( t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being ArgumentSeq of Sym (o,V)
for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
( t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i )
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for o being OperSymbol of S
for a being ArgumentSeq of Sym (o,V)
for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
( t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i )
let o be OperSymbol of S; ::_thesis: for a being ArgumentSeq of Sym (o,V)
for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
( t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i )
let a be ArgumentSeq of Sym (o,V); ::_thesis: for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
( t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i )
let i be Nat; ::_thesis: ( i in dom a implies for t being Term of S,V st t = a . i holds
( t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) )
assume i in dom a ; ::_thesis: for t being Term of S,V st t = a . i holds
( t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i )
then ex t being Term of S,V st
( t = a . i & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) by Lm8;
hence for t being Term of S,V st t = a . i holds
( t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) ; ::_thesis: verum
end;
theorem Th24: :: MSATERM:24
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being FinSequence st ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i ) or for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) holds
a is ArgumentSeq of Sym (o,V)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being FinSequence st ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i ) or for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) holds
a is ArgumentSeq of Sym (o,V)
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for o being OperSymbol of S
for a being FinSequence st ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i ) or for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) holds
a is ArgumentSeq of Sym (o,V)
set X = V;
let o be OperSymbol of S; ::_thesis: for a being FinSequence st ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i ) or for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) holds
a is ArgumentSeq of Sym (o,V)
let a be FinSequence; ::_thesis: ( ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i ) or for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) implies a is ArgumentSeq of Sym (o,V) )
assume that
A1: ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) and
A2: ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i ) or for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) ; ::_thesis: a is ArgumentSeq of Sym (o,V)
rng a c= TS (DTConMSA V)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng a or x in TS (DTConMSA V) )
assume x in rng a ; ::_thesis: x in TS (DTConMSA V)
then consider i being set such that
A3: i in dom a and
A4: x = a . i by FUNCT_1:def_3;
reconsider i = i as Nat by A3;
( ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i ) or ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) by A2, A3;
hence x in TS (DTConMSA V) by A4; ::_thesis: verum
end;
then reconsider p = a as FinSequence of TS (DTConMSA V) by FINSEQ_1:def_4;
A5: dom a = dom (the_arity_of o) by A1, FINSEQ_3:29;
now__::_thesis:_for_n_being_Nat_st_n_in_dom_p_holds_
p_._n_in_FreeSort_(V,((the_arity_of_o)_/._n))
let n be Nat; ::_thesis: ( n in dom p implies p . n in FreeSort (V,((the_arity_of o) /. n)) )
assume A6: n in dom p ; ::_thesis: p . n in FreeSort (V,((the_arity_of o) /. n))
thus p . n in FreeSort (V,((the_arity_of o) /. n)) ::_thesis: verum
proof
percases ( ex t being Term of S,V st
( t = a . n & the_sort_of t = (the_arity_of o) . n ) or ex t being Term of S,V st
( t = a . n & the_sort_of t = (the_arity_of o) /. n ) ) by A2, A6;
suppose ex t being Term of S,V st
( t = a . n & the_sort_of t = (the_arity_of o) . n ) ; ::_thesis: p . n in FreeSort (V,((the_arity_of o) /. n))
then consider t being Term of S,V such that
A7: t = a . n and
A8: the_sort_of t = (the_arity_of o) . n ;
the_sort_of t = (the_arity_of o) /. n by A5, A6, A8, PARTFUN1:def_6;
hence p . n in FreeSort (V,((the_arity_of o) /. n)) by A7, Def5; ::_thesis: verum
end;
suppose ex t being Term of S,V st
( t = a . n & the_sort_of t = (the_arity_of o) /. n ) ; ::_thesis: p . n in FreeSort (V,((the_arity_of o) /. n))
hence p . n in FreeSort (V,((the_arity_of o) /. n)) by Def5; ::_thesis: verum
end;
end;
end;
end;
then p in (((FreeSort V) #) * the Arity of S) . o by A5, MSAFREE:9;
then A9: Sym (o,V) ==> roots p by MSAFREE:10;
S -Terms V = TS (DTConMSA V) ;
hence a is ArgumentSeq of Sym (o,V) by A9, Th21; ::_thesis: verum
end;
theorem :: MSATERM:25
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being FinSequence of S -Terms V st ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) . i or for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) /. i ) holds
a is ArgumentSeq of Sym (o,V)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being FinSequence of S -Terms V st ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) . i or for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) /. i ) holds
a is ArgumentSeq of Sym (o,V)
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for o being OperSymbol of S
for a being FinSequence of S -Terms V st ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) . i or for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) /. i ) holds
a is ArgumentSeq of Sym (o,V)
let o be OperSymbol of S; ::_thesis: for a being FinSequence of S -Terms V st ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) . i or for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) /. i ) holds
a is ArgumentSeq of Sym (o,V)
let a be FinSequence of S -Terms V; ::_thesis: ( ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) . i or for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) /. i ) implies a is ArgumentSeq of Sym (o,V) )
assume that
A1: ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) and
A2: ( for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) . i or for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) /. i ) ; ::_thesis: a is ArgumentSeq of Sym (o,V)
A3: now__::_thesis:_for_i_being_Nat_st_i_in_dom_a_holds_
a_._i_in_S_-Terms_V
let i be Nat; ::_thesis: ( i in dom a implies a . i in S -Terms V )
assume i in dom a ; ::_thesis: a . i in S -Terms V
then A4: a . i in rng a by FUNCT_1:def_3;
rng a c= S -Terms V by FINSEQ_1:def_4;
hence a . i in S -Terms V by A4; ::_thesis: verum
end;
now__::_thesis:_(_(_(_for_i_being_Nat_st_i_in_dom_a_holds_
for_t_being_Term_of_S,V_st_t_=_a_._i_holds_
the_sort_of_t_=_(the_arity_of_o)_._i_)_&_(_for_i_being_Nat_st_i_in_dom_a_holds_
ex_t_being_Term_of_S,V_st_
(_t_=_a_._i_&_the_sort_of_t_=_(the_arity_of_o)_._i_)_)_)_or_(_(_for_i_being_Nat_st_i_in_dom_a_holds_
for_t_being_Term_of_S,V_st_t_=_a_._i_holds_
the_sort_of_t_=_(the_arity_of_o)_/._i_)_&_(_for_i_being_Nat_st_i_in_dom_a_holds_
ex_t_being_Term_of_S,V_st_
(_t_=_a_._i_&_the_sort_of_t_=_(the_arity_of_o)_/._i_)_)_)_)
percases ( for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) . i or for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) /. i ) by A2;
caseA5: for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) . i ; ::_thesis: for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i )
let i be Nat; ::_thesis: ( i in dom a implies ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i ) )
assume A6: i in dom a ; ::_thesis: ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i )
then reconsider t = a . i as Term of S,V by A3;
take t = t; ::_thesis: ( t = a . i & the_sort_of t = (the_arity_of o) . i )
thus ( t = a . i & the_sort_of t = (the_arity_of o) . i ) by A5, A6; ::_thesis: verum
end;
caseA7: for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) /. i ; ::_thesis: for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i )
let i be Nat; ::_thesis: ( i in dom a implies ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) )
assume A8: i in dom a ; ::_thesis: ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i )
then reconsider t = a . i as Term of S,V by A3;
take t = t; ::_thesis: ( t = a . i & the_sort_of t = (the_arity_of o) /. i )
thus ( t = a . i & the_sort_of t = (the_arity_of o) /. i ) by A7, A8; ::_thesis: verum
end;
end;
end;
hence a is ArgumentSeq of Sym (o,V) by A1, Th24; ::_thesis: verum
end;
theorem Th26: :: MSATERM:26
for S being non empty non void ManySortedSign
for V1, V2 being V16() ManySortedSet of the carrier of S st V1 c= V2 holds
for t being Term of S,V1 holds t is Term of S,V2
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V1, V2 being V16() ManySortedSet of the carrier of S st V1 c= V2 holds
for t being Term of S,V1 holds t is Term of S,V2
let V1, V2 be V16() ManySortedSet of the carrier of S; ::_thesis: ( V1 c= V2 implies for t being Term of S,V1 holds t is Term of S,V2 )
assume A1: for s being set st s in the carrier of S holds
V1 . s c= V2 . s ; :: according to PBOOLE:def_2 ::_thesis: for t being Term of S,V1 holds t is Term of S,V2
defpred S1[ set ] means $1 is Term of S,V2;
A2: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,V1) st ( for t being Term of S,V1 st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S] -tree p]
proof
let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of Sym (o,V1) st ( for t being Term of S,V1 st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S] -tree p]
let p be ArgumentSeq of Sym (o,V1); ::_thesis: ( ( for t being Term of S,V1 st t in rng p holds
S1[t] ) implies S1[[o, the carrier of S] -tree p] )
assume A3: for t being Term of S,V1 st t in rng p holds
t is Term of S,V2 ; ::_thesis: S1[[o, the carrier of S] -tree p]
rng p c= S -Terms V2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in S -Terms V2 )
assume A4: x in rng p ; ::_thesis: x in S -Terms V2
rng p c= S -Terms V1 by FINSEQ_1:def_4;
then reconsider x = x as Term of S,V1 by A4;
x is Term of S,V2 by A3, A4;
hence x in S -Terms V2 ; ::_thesis: verum
end;
then reconsider q = p as FinSequence of S -Terms V2 by FINSEQ_1:def_4;
A5: now__::_thesis:_for_i_being_Nat_st_i_in_dom_q_holds_
ex_T_being_Term_of_S,V2_st_
(_T_=_q_._i_&_the_sort_of_T_=_(the_arity_of_o)_._i_)
let i be Nat; ::_thesis: ( i in dom q implies ex T being Term of S,V2 st
( T = q . i & the_sort_of T = (the_arity_of o) . i ) )
assume A6: i in dom q ; ::_thesis: ex T being Term of S,V2 st
( T = q . i & the_sort_of T = (the_arity_of o) . i )
then consider t being Term of S,V1 such that
A7: t = q . i and
t = p /. i and
A8: the_sort_of t = (the_arity_of o) . i and
the_sort_of t = (the_arity_of o) /. i by Lm8;
t in rng p by A6, A7, FUNCT_1:def_3;
then reconsider T = t as Term of S,V2 by A3;
take T = T; ::_thesis: ( T = q . i & the_sort_of T = (the_arity_of o) . i )
thus T = q . i by A7; ::_thesis: the_sort_of T = (the_arity_of o) . i
thus the_sort_of T = (the_arity_of o) . i ::_thesis: verum
proof
percases ( ex s being SortSymbol of S ex v being Element of V1 . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] ) by Th2;
suppose ex s being SortSymbol of S ex v being Element of V1 . s st t . {} = [v,s] ; ::_thesis: the_sort_of T = (the_arity_of o) . i
then consider s being SortSymbol of S, v being Element of V1 . s such that
A9: t . {} = [v,s] ;
A10: t = root-tree [v,s] by A9, Th5;
V1 . s c= V2 . s by A1;
then v in V2 . s by TARSKI:def_3;
hence the_sort_of T = s by A10, Th14
.= (the_arity_of o) . i by A8, A10, Th14 ;
::_thesis: verum
end;
suppose t . {} in [: the carrier' of S,{ the carrier of S}:] ; ::_thesis: the_sort_of T = (the_arity_of o) . i
then consider o9 being OperSymbol of S, x2 being Element of { the carrier of S} such that
A11: t . {} = [o9,x2] by DOMAIN_1:1;
A12: x2 = the carrier of S by TARSKI:def_1;
hence the_sort_of T = the_result_sort_of o9 by A11, Th17
.= (the_arity_of o) . i by A8, A11, A12, Th17 ;
::_thesis: verum
end;
end;
end;
end;
len p = len (the_arity_of o) by Lm8;
then q is ArgumentSeq of Sym (o,V2) by A5, Th24;
hence S1[[o, the carrier of S] -tree p] by Th1; ::_thesis: verum
end;
A13: for s being SortSymbol of S
for v being Element of V1 . s holds S1[ root-tree [v,s]]
proof
let s be SortSymbol of S; ::_thesis: for v being Element of V1 . s holds S1[ root-tree [v,s]]
let v be Element of V1 . s; ::_thesis: S1[ root-tree [v,s]]
V1 . s c= V2 . s by A1;
then v in V2 . s by TARSKI:def_3;
hence S1[ root-tree [v,s]] by Th4; ::_thesis: verum
end;
for t being Term of S,V1 holds S1[t] from MSATERM:sch_1(A13, A2);
hence for t being Term of S,V1 holds t is Term of S,V2 ; ::_thesis: verum
end;
theorem :: MSATERM:27
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V holds t is c-Term of A,V by Th26, PBOOLE:14;
begin
definition
let S be non empty non void ManySortedSign ;
let V be V16() ManySortedSet of the carrier of S;
mode CompoundTerm of S,V -> Term of S,V means :: MSATERM:def 6
it . {} in [: the carrier' of S,{ the carrier of S}:];
existence
ex b1 being Term of S,V st b1 . {} in [: the carrier' of S,{ the carrier of S}:]
proof
set s = the OperSymbol of S;
reconsider nt = Sym ( the OperSymbol of S,V) as NonTerminal of (DTConMSA V) ;
set p = the SubtreeSeq of nt;
reconsider t = nt -tree the SubtreeSeq of nt as Term of S,V ;
take t ; ::_thesis: t . {} in [: the carrier' of S,{ the carrier of S}:]
nt = [ the OperSymbol of S, the carrier of S] by MSAFREE:def_9;
then A1: [ the OperSymbol of S, the carrier of S] = t . {} by TREES_4:def_4;
the carrier of S in { the carrier of S} by TARSKI:def_1;
hence t . {} in [: the carrier' of S,{ the carrier of S}:] by A1, ZFMISC_1:87; ::_thesis: verum
end;
end;
:: deftheorem defines CompoundTerm MSATERM:def_6_:_
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for b3 being Term of S,V holds
( b3 is CompoundTerm of S,V iff b3 . {} in [: the carrier' of S,{ the carrier of S}:] );
definition
let S be non empty non void ManySortedSign ;
let V be V16() ManySortedSet of the carrier of S;
mode SetWithCompoundTerm of S,V -> non empty Subset of (S -Terms V) means :: MSATERM:def 7
ex t being CompoundTerm of S,V st t in it;
existence
ex b1 being non empty Subset of (S -Terms V) ex t being CompoundTerm of S,V st t in b1
proof
set t = the CompoundTerm of S,V;
reconsider X = { the CompoundTerm of S,V} as non empty Subset of (S -Terms V) by ZFMISC_1:31;
take X ; ::_thesis: ex t being CompoundTerm of S,V st t in X
take the CompoundTerm of S,V ; ::_thesis: the CompoundTerm of S,V in X
thus the CompoundTerm of S,V in X by TARSKI:def_1; ::_thesis: verum
end;
end;
:: deftheorem defines SetWithCompoundTerm MSATERM:def_7_:_
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for b3 being non empty Subset of (S -Terms V) holds
( b3 is SetWithCompoundTerm of S,V iff ex t being CompoundTerm of S,V st t in b3 );
theorem :: MSATERM:28
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V st not t is root holds
t is CompoundTerm of S,V
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V st not t is root holds
t is CompoundTerm of S,V
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,V st not t is root holds
t is CompoundTerm of S,V
let t be Term of S,V; ::_thesis: ( not t is root implies t is CompoundTerm of S,V )
assume A1: not t is root ; ::_thesis: t is CompoundTerm of S,V
percases ( ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] ) by Th2;
suppose ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] ; ::_thesis: t is CompoundTerm of S,V
then consider s being SortSymbol of S, x being Element of V . s such that
A2: t . {} = [x,s] ;
t = root-tree [x,s] by A2, Th5;
hence t is CompoundTerm of S,V by A1; ::_thesis: verum
end;
suppose t . {} in [: the carrier' of S,{ the carrier of S}:] ; ::_thesis: t is CompoundTerm of S,V
hence t . {} in [: the carrier' of S,{ the carrier of S}:] ; :: according to MSATERM:def_6 ::_thesis: verum
end;
end;
end;
Lm9: for n being Element of NAT
for p being FinSequence st n < len p holds
( n + 1 in dom p & p . (n + 1) in rng p )
proof
let n be Element of NAT ; ::_thesis: for p being FinSequence st n < len p holds
( n + 1 in dom p & p . (n + 1) in rng p )
let p be FinSequence; ::_thesis: ( n < len p implies ( n + 1 in dom p & p . (n + 1) in rng p ) )
n >= 0 by NAT_1:2;
then A1: n + 1 >= 0 + 1 by XREAL_1:7;
assume n < len p ; ::_thesis: ( n + 1 in dom p & p . (n + 1) in rng p )
then n + 1 <= len p by NAT_1:13;
then n + 1 in dom p by A1, FINSEQ_3:25;
hence ( n + 1 in dom p & p . (n + 1) in rng p ) by FUNCT_1:def_3; ::_thesis: verum
end;
theorem Th29: :: MSATERM:29
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V
for p being Node of t holds t | p is Term of S,V
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V
for p being Node of t holds t | p is Term of S,V
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,V
for p being Node of t holds t | p is Term of S,V
let t be Term of S,V; ::_thesis: for p being Node of t holds t | p is Term of S,V
defpred S1[ set ] means for q being Node of t st q = $1 holds
t | q is Term of S,V;
A1: for p being Node of t
for n being Element of NAT st S1[p] & p ^ <*n*> in dom t holds
S1[p ^ <*n*>]
proof
let p be Node of t; ::_thesis: for n being Element of NAT st S1[p] & p ^ <*n*> in dom t holds
S1[p ^ <*n*>]
let n be Element of NAT ; ::_thesis: ( S1[p] & p ^ <*n*> in dom t implies S1[p ^ <*n*>] )
assume that
A2: for q being Node of t st q = p holds
t | q is Term of S,V and
A3: p ^ <*n*> in dom t ; ::_thesis: S1[p ^ <*n*>]
reconsider u = t | p as Term of S,V by A2;
A4: dom u = (dom t) | p by TREES_2:def_10;
A5: <*n*> in (dom t) | p by A3, TREES_1:def_6;
A6: now__::_thesis:_for_s_being_SortSymbol_of_S
for_x_being_Element_of_V_._s_holds_not_u_._{}_=_[x,s]
given s being SortSymbol of S, x being Element of V . s such that A7: u . {} = [x,s] ; ::_thesis: contradiction
u = root-tree [x,s] by A7, Th5;
then <*n*> in {{}} by A5, A4, TREES_1:29, TREES_4:3;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
( ex s being SortSymbol of S ex v being Element of V . s st u . {} = [v,s] or u . {} in [: the carrier' of S,{ the carrier of S}:] ) by Th2;
then consider o being OperSymbol of S, x2 being Element of { the carrier of S} such that
A8: u . {} = [o,x2] by A6, DOMAIN_1:1;
x2 = the carrier of S by TARSKI:def_1;
then consider a being ArgumentSeq of Sym (o,V) such that
A9: u = [o, the carrier of S] -tree a by A8, Th10;
consider i being Element of NAT , T being DecoratedTree, r being Node of T such that
A10: i < len a and
T = a . (i + 1) and
A11: <*n*> = <*i*> ^ r by A5, A4, A9, TREES_4:11;
A12: n = <*n*> . 1 by FINSEQ_1:40
.= i by A11, FINSEQ_1:41 ;
then A13: u | <*n*> = a . (n + 1) by A9, A10, TREES_4:def_4;
let q be Node of t; ::_thesis: ( q = p ^ <*n*> implies t | q is Term of S,V )
assume A14: q = p ^ <*n*> ; ::_thesis: t | q is Term of S,V
n + 1 in dom a by A10, A12, Lm9;
then ex t being Term of S,V st
( t = u | <*n*> & t = a /. (n + 1) & the_sort_of t = (the_arity_of o) . (n + 1) & the_sort_of t = (the_arity_of o) /. (n + 1) ) by A13, Lm8;
hence t | q is Term of S,V by A14, TREES_9:3; ::_thesis: verum
end;
A15: S1[ {} ] by TREES_9:1;
for p being Node of t holds S1[p] from TREES_2:sch_1(A15, A1);
hence for p being Node of t holds t | p is Term of S,V ; ::_thesis: verum
end;
definition
let S be non empty non void ManySortedSign ;
let V be V16() ManySortedSet of the carrier of S;
let t be Term of S,V;
let p be Node of t;
:: original: |
redefine funct | p -> Term of S,V;
coherence
t | p is Term of S,V by Th29;
end;
begin
definition
let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
mode Variables of A -> V16() ManySortedSet of the carrier of S means :Def8: :: MSATERM:def 8
it misses the Sorts of A;
existence
ex b1 being V16() ManySortedSet of the carrier of S st b1 misses the Sorts of A
proof
deffunc H1( set ) -> set = {( the Sorts of A . $1)};
consider V being ManySortedSet of the carrier of S such that
A1: for s being set st s in the carrier of S holds
V . s = H1(s) from PBOOLE:sch_4();
V is V16()
proof
let s be set ; :: according to PBOOLE:def_13 ::_thesis: ( not s in the carrier of S or not V . s is empty )
assume s in the carrier of S ; ::_thesis: not V . s is empty
then V . s = {( the Sorts of A . s)} by A1;
hence not V . s is empty ; ::_thesis: verum
end;
then reconsider V = V as V16() ManySortedSet of the carrier of S ;
take V ; ::_thesis: V misses the Sorts of A
let s be set ; :: according to PBOOLE:def_8 ::_thesis: ( not s in the carrier of S or V . s misses the Sorts of A . s )
assume s in the carrier of S ; ::_thesis: V . s misses the Sorts of A . s
then A2: V . s = {( the Sorts of A . s)} by A1;
now__::_thesis:_for_x_being_set_st_x_in_V_._s_holds_
not_x_in_the_Sorts_of_A_._s
let x be set ; ::_thesis: ( x in V . s implies not x in the Sorts of A . s )
assume x in V . s ; ::_thesis: not x in the Sorts of A . s
then x = the Sorts of A . s by A2, TARSKI:def_1;
hence not x in the Sorts of A . s ; ::_thesis: verum
end;
hence V . s misses the Sorts of A . s by XBOOLE_0:3; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines Variables MSATERM:def_8_:_
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for b3 being V16() ManySortedSet of the carrier of S holds
( b3 is Variables of A iff b3 misses the Sorts of A );
theorem Th30: :: MSATERM:30
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for V being Variables of A
for s being SortSymbol of S
for x being set st x in the Sorts of A . s holds
for v being Element of V . s holds x <> v
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra over S
for V being Variables of A
for s being SortSymbol of S
for x being set st x in the Sorts of A . s holds
for v being Element of V . s holds x <> v
let A be MSAlgebra over S; ::_thesis: for V being Variables of A
for s being SortSymbol of S
for x being set st x in the Sorts of A . s holds
for v being Element of V . s holds x <> v
let V be Variables of A; ::_thesis: for s being SortSymbol of S
for x being set st x in the Sorts of A . s holds
for v being Element of V . s holds x <> v
let s be SortSymbol of S; ::_thesis: for x being set st x in the Sorts of A . s holds
for v being Element of V . s holds x <> v
let x be set ; ::_thesis: ( x in the Sorts of A . s implies for v being Element of V . s holds x <> v )
assume A1: x in the Sorts of A . s ; ::_thesis: for v being Element of V . s holds x <> v
let v be Element of V . s; ::_thesis: x <> v
V misses the Sorts of A by Def8;
then V . s misses the Sorts of A . s by PBOOLE:def_8;
hence x <> v by A1, XBOOLE_0:3; ::_thesis: verum
end;
definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let V be V16() ManySortedSet of the carrier of S;
let t be c-Term of A,V;
let f be ManySortedFunction of V, the Sorts of A;
let vt be finite DecoratedTree;
predvt is_an_evaluation_of t,f means :Def9: :: MSATERM:def 9
( dom vt = dom t & ( for p being Node of vt holds
( ( for s being SortSymbol of S
for v being Element of V . s st t . p = [v,s] holds
vt . p = (f . s) . v ) & ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st t . p = [x,s] holds
vt . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds
vt . p = (Den (o,A)) . (succ (vt,p)) ) ) ) );
end;
:: deftheorem Def9 defines is_an_evaluation_of MSATERM:def_9_:_
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being V16() ManySortedSet of the carrier of S
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for vt being finite DecoratedTree holds
( vt is_an_evaluation_of t,f iff ( dom vt = dom t & ( for p being Node of vt holds
( ( for s being SortSymbol of S
for v being Element of V . s st t . p = [v,s] holds
vt . p = (f . s) . v ) & ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st t . p = [x,s] holds
vt . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds
vt . p = (Den (o,A)) . (succ (vt,p)) ) ) ) ) );
theorem Th31: :: MSATERM:31
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for s being SortSymbol of S
for x being Element of the Sorts of A . s st t = root-tree [x,s] holds
root-tree x is_an_evaluation_of t,f
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for s being SortSymbol of S
for x being Element of the Sorts of A . s st t = root-tree [x,s] holds
root-tree x is_an_evaluation_of t,f
let A be non-empty MSAlgebra over S; ::_thesis: for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for s being SortSymbol of S
for x being Element of the Sorts of A . s st t = root-tree [x,s] holds
root-tree x is_an_evaluation_of t,f
let V be Variables of A; ::_thesis: for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for s being SortSymbol of S
for x being Element of the Sorts of A . s st t = root-tree [x,s] holds
root-tree x is_an_evaluation_of t,f
let t be c-Term of A,V; ::_thesis: for f being ManySortedFunction of V, the Sorts of A
for s being SortSymbol of S
for x being Element of the Sorts of A . s st t = root-tree [x,s] holds
root-tree x is_an_evaluation_of t,f
let f be ManySortedFunction of V, the Sorts of A; ::_thesis: for s being SortSymbol of S
for x being Element of the Sorts of A . s st t = root-tree [x,s] holds
root-tree x is_an_evaluation_of t,f
let s be SortSymbol of S; ::_thesis: for x being Element of the Sorts of A . s st t = root-tree [x,s] holds
root-tree x is_an_evaluation_of t,f
let x be Element of the Sorts of A . s; ::_thesis: ( t = root-tree [x,s] implies root-tree x is_an_evaluation_of t,f )
assume A1: t = root-tree [x,s] ; ::_thesis: root-tree x is_an_evaluation_of t,f
A2: t . {} = [x,s] by A1, TREES_4:3;
set vt = root-tree x;
A3: dom (root-tree x) = elementary_tree 0 by TREES_4:3;
hence dom (root-tree x) = dom t by A1, TREES_4:3; :: according to MSATERM:def_9 ::_thesis: for p being Node of (root-tree x) holds
( ( for s being SortSymbol of S
for v being Element of V . s st t . p = [v,s] holds
(root-tree x) . p = (f . s) . v ) & ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st t . p = [x,s] holds
(root-tree x) . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds
(root-tree x) . p = (Den (o,A)) . (succ ((root-tree x),p)) ) )
let p be Node of (root-tree x); ::_thesis: ( ( for s being SortSymbol of S
for v being Element of V . s st t . p = [v,s] holds
(root-tree x) . p = (f . s) . v ) & ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st t . p = [x,s] holds
(root-tree x) . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds
(root-tree x) . p = (Den (o,A)) . (succ ((root-tree x),p)) ) )
reconsider e = p as empty FinSequence of NAT by A3, TARSKI:def_1, TREES_1:29;
hereby ::_thesis: ( ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st t . p = [x,s] holds
(root-tree x) . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds
(root-tree x) . p = (Den (o,A)) . (succ ((root-tree x),p)) ) )
let s1 be SortSymbol of S; ::_thesis: for v being Element of V . s1 st t . p = [v,s1] holds
(root-tree x) . p = (f . s1) . v
let v be Element of V . s1; ::_thesis: ( t . p = [v,s1] implies (root-tree x) . p = (f . s1) . v )
assume t . p = [v,s1] ; ::_thesis: (root-tree x) . p = (f . s1) . v
then A4: [v,s1] = t . e
.= [x,s] by A1, TREES_4:3 ;
then A5: x = v by XTUPLE_0:1;
s = s1 by A4, XTUPLE_0:1;
hence (root-tree x) . p = (f . s1) . v by A5, Th30; ::_thesis: verum
end;
A6: (root-tree x) . {} = x by TREES_4:3;
hereby ::_thesis: for o being OperSymbol of S st t . p = [o, the carrier of S] holds
(root-tree x) . p = (Den (o,A)) . (succ ((root-tree x),p))
let s1 be SortSymbol of S; ::_thesis: for x1 being Element of the Sorts of A . s1 st t . p = [x1,s1] holds
(root-tree x) . p = x1
let x1 be Element of the Sorts of A . s1; ::_thesis: ( t . p = [x1,s1] implies (root-tree x) . p = x1 )
assume t . p = [x1,s1] ; ::_thesis: (root-tree x) . p = x1
then [x1,s1] = t . e ;
hence (root-tree x) . p = x1 by A2, A6, XTUPLE_0:1; ::_thesis: verum
end;
let o be OperSymbol of S; ::_thesis: ( t . p = [o, the carrier of S] implies (root-tree x) . p = (Den (o,A)) . (succ ((root-tree x),p)) )
assume t . p = [o, the carrier of S] ; ::_thesis: (root-tree x) . p = (Den (o,A)) . (succ ((root-tree x),p))
then the carrier of S = (t . e) `2 by MCART_1:7
.= s by A2, MCART_1:7 ;
hence (root-tree x) . p = (Den (o,A)) . (succ ((root-tree x),p)) by Lm7; ::_thesis: verum
end;
theorem Th32: :: MSATERM:32
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
root-tree ((f . s) . v) is_an_evaluation_of t,f
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
root-tree ((f . s) . v) is_an_evaluation_of t,f
let A be non-empty MSAlgebra over S; ::_thesis: for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
root-tree ((f . s) . v) is_an_evaluation_of t,f
let V be Variables of A; ::_thesis: for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
root-tree ((f . s) . v) is_an_evaluation_of t,f
let t be c-Term of A,V; ::_thesis: for f being ManySortedFunction of V, the Sorts of A
for s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
root-tree ((f . s) . v) is_an_evaluation_of t,f
let f be ManySortedFunction of V, the Sorts of A; ::_thesis: for s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
root-tree ((f . s) . v) is_an_evaluation_of t,f
let s be SortSymbol of S; ::_thesis: for v being Element of V . s st t = root-tree [v,s] holds
root-tree ((f . s) . v) is_an_evaluation_of t,f
let x be Element of V . s; ::_thesis: ( t = root-tree [x,s] implies root-tree ((f . s) . x) is_an_evaluation_of t,f )
assume A1: t = root-tree [x,s] ; ::_thesis: root-tree ((f . s) . x) is_an_evaluation_of t,f
set vt = root-tree ((f . s) . x);
A2: dom (root-tree ((f . s) . x)) = elementary_tree 0 by TREES_4:3;
hence dom (root-tree ((f . s) . x)) = dom t by A1, TREES_4:3; :: according to MSATERM:def_9 ::_thesis: for p being Node of (root-tree ((f . s) . x)) holds
( ( for s being SortSymbol of S
for v being Element of V . s st t . p = [v,s] holds
(root-tree ((f . s) . x)) . p = (f . s) . v ) & ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st t . p = [x,s] holds
(root-tree ((f . s) . x)) . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds
(root-tree ((f . s) . x)) . p = (Den (o,A)) . (succ ((root-tree ((f . s) . x)),p)) ) )
let p be Node of (root-tree ((f . s) . x)); ::_thesis: ( ( for s being SortSymbol of S
for v being Element of V . s st t . p = [v,s] holds
(root-tree ((f . s) . x)) . p = (f . s) . v ) & ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st t . p = [x,s] holds
(root-tree ((f . s) . x)) . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds
(root-tree ((f . s) . x)) . p = (Den (o,A)) . (succ ((root-tree ((f . s) . x)),p)) ) )
reconsider e = p as empty FinSequence of NAT by A2, TARSKI:def_1, TREES_1:29;
A3: t . {} = [x,s] by A1, TREES_4:3;
hereby ::_thesis: ( ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st t . p = [x,s] holds
(root-tree ((f . s) . x)) . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds
(root-tree ((f . s) . x)) . p = (Den (o,A)) . (succ ((root-tree ((f . s) . x)),p)) ) )
let s1 be SortSymbol of S; ::_thesis: for x1 being Element of V . s1 st t . p = [x1,s1] holds
(root-tree ((f . s) . x)) . p = (f . s1) . x1
let x1 be Element of V . s1; ::_thesis: ( t . p = [x1,s1] implies (root-tree ((f . s) . x)) . p = (f . s1) . x1 )
A4: e = p ;
assume t . p = [x1,s1] ; ::_thesis: (root-tree ((f . s) . x)) . p = (f . s1) . x1
then A5: [x1,s1] = t . e ;
then A6: s = s1 by A3, XTUPLE_0:1;
x = x1 by A3, A5, XTUPLE_0:1;
hence (root-tree ((f . s) . x)) . p = (f . s1) . x1 by A6, A4, TREES_4:3; ::_thesis: verum
end;
hereby ::_thesis: for o being OperSymbol of S st t . p = [o, the carrier of S] holds
(root-tree ((f . s) . x)) . p = (Den (o,A)) . (succ ((root-tree ((f . s) . x)),p))
let s1 be SortSymbol of S; ::_thesis: for v being Element of the Sorts of A . s1 st t . p = [v,s1] holds
(root-tree ((f . s) . x)) . p = v
let v be Element of the Sorts of A . s1; ::_thesis: ( t . p = [v,s1] implies (root-tree ((f . s) . x)) . p = v )
assume t . p = [v,s1] ; ::_thesis: (root-tree ((f . s) . x)) . p = v
then A7: [v,s1] = t . e
.= [x,s] by A1, TREES_4:3 ;
then A8: x = v by XTUPLE_0:1;
s = s1 by A7, XTUPLE_0:1;
hence (root-tree ((f . s) . x)) . p = v by A8, Th30; ::_thesis: verum
end;
let o be OperSymbol of S; ::_thesis: ( t . p = [o, the carrier of S] implies (root-tree ((f . s) . x)) . p = (Den (o,A)) . (succ ((root-tree ((f . s) . x)),p)) )
assume t . p = [o, the carrier of S] ; ::_thesis: (root-tree ((f . s) . x)) . p = (Den (o,A)) . (succ ((root-tree ((f . s) . x)),p))
then the carrier of S = (t . e) `2 by MCART_1:7
.= s by A3, MCART_1:7 ;
hence (root-tree ((f . s) . x)) . p = (Den (o,A)) . (succ ((root-tree ((f . s) . x)),p)) by Lm7; ::_thesis: verum
end;
theorem Th33: :: MSATERM:33
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for q being DTree-yielding FinSequence st len q = len p & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) holds
ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for q being DTree-yielding FinSequence st len q = len p & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) holds
ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f )
let A be non-empty MSAlgebra over S; ::_thesis: for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for q being DTree-yielding FinSequence st len q = len p & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) holds
ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f )
let V be Variables of A; ::_thesis: for f being ManySortedFunction of V, the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for q being DTree-yielding FinSequence st len q = len p & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) holds
ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f )
let f be ManySortedFunction of V, the Sorts of A; ::_thesis: for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for q being DTree-yielding FinSequence st len q = len p & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) holds
ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f )
let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of o,A,V
for q being DTree-yielding FinSequence st len q = len p & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) holds
ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f )
let p be ArgumentSeq of o,A,V; ::_thesis: for q being DTree-yielding FinSequence st len q = len p & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) holds
ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f )
A1: Sym (o,( the Sorts of A \/ V)) = [o, the carrier of S] by MSAFREE:def_9;
A2: dom (doms p) = dom p by TREES_3:37;
A3: tree (doms p) = dom ([o, the carrier of S] -tree p) by TREES_4:10;
A4: dom p = Seg (len p) by FINSEQ_1:def_3;
let q be DTree-yielding FinSequence; ::_thesis: ( len q = len p & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) implies ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f ) )
assume that
A5: len q = len p and
A6: for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ; ::_thesis: ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f )
A7: dom q = Seg (len q) by FINSEQ_1:def_3;
now__::_thesis:_for_x_being_set_st_x_in_dom_(doms_q)_holds_
(doms_q)_._x_is_finite_Tree
let x be set ; ::_thesis: ( x in dom (doms q) implies (doms q) . x is finite Tree )
A8: rng p c= S -Terms ( the Sorts of A \/ V) by FINSEQ_1:def_4;
assume A9: x in dom (doms q) ; ::_thesis: (doms q) . x is finite Tree
then A10: x in dom q by TREES_3:37;
then p . x in rng p by A5, A4, A7, FUNCT_1:def_3;
then reconsider t = p . x as c-Term of A,V by A8;
reconsider i = x as Nat by A9;
consider vt being finite DecoratedTree such that
A11: vt = q . i and
vt is_an_evaluation_of t,f by A5, A6, A4, A7, A10;
(doms q) . x = dom vt by A10, A11, FUNCT_6:22;
hence (doms q) . x is finite Tree ; ::_thesis: verum
end;
then reconsider r = doms q as FinTree-yielding FinSequence by TREES_3:23;
A12: now__::_thesis:_for_i_being_Nat_st_i_in_dom_p_holds_
r_._i_=_(doms_p)_._i
let i be Nat; ::_thesis: ( i in dom p implies r . i = (doms p) . i )
A13: rng p c= S -Terms ( the Sorts of A \/ V) by FINSEQ_1:def_4;
assume A14: i in dom p ; ::_thesis: r . i = (doms p) . i
then p . i in rng p by FUNCT_1:def_3;
then reconsider t = p . i as c-Term of A,V by A13;
consider vt being finite DecoratedTree such that
A15: vt = q . i and
A16: vt is_an_evaluation_of t,f by A6, A14;
thus r . i = dom vt by A5, A4, A7, A14, A15, FUNCT_6:22
.= dom t by A16, Def9
.= (doms p) . i by A14, FUNCT_6:22 ; ::_thesis: verum
end;
set vt = ((Den (o,A)) . (roots q)) -tree q;
A17: len (doms q) = len q by TREES_3:38;
A18: dom (((Den (o,A)) . (roots q)) -tree q) = tree r by TREES_4:10;
then reconsider vt = ((Den (o,A)) . (roots q)) -tree q as finite DecoratedTree by FINSET_1:10;
take vt ; ::_thesis: ( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f )
thus vt = ((Den (o,A)) . (roots q)) -tree q ; ::_thesis: vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f
dom (doms q) = dom q by TREES_3:37;
hence dom vt = dom ((Sym (o,( the Sorts of A \/ V))) -tree p) by A1, A5, A4, A7, A18, A3, A2, A12, FINSEQ_1:13; :: according to MSATERM:def_9 ::_thesis: for p being Node of vt holds
( ( for s being SortSymbol of S
for v being Element of V . s st ((Sym (o,( the Sorts of A \/ V))) -tree p) . p = [v,s] holds
vt . p = (f . s) . v ) & ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st ((Sym (o,( the Sorts of A \/ V))) -tree p) . p = [x,s] holds
vt . p = x ) & ( for o being OperSymbol of S st ((Sym (o,( the Sorts of A \/ V))) -tree p) . p = [o, the carrier of S] holds
vt . p = (Den (o,A)) . (succ (vt,p)) ) )
let n be Node of vt; ::_thesis: ( ( for s being SortSymbol of S
for v being Element of V . s st ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [v,s] holds
vt . n = (f . s) . v ) & ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [x,s] holds
vt . n = x ) & ( for o being OperSymbol of S st ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [o, the carrier of S] holds
vt . n = (Den (o,A)) . (succ (vt,n)) ) )
A19: ([o, the carrier of S] -tree p) . {} = [o, the carrier of S] by TREES_4:def_4;
hereby ::_thesis: ( ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [x,s] holds
vt . n = x ) & ( for o being OperSymbol of S st ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [o, the carrier of S] holds
vt . n = (Den (o,A)) . (succ (vt,n)) ) )
let s be SortSymbol of S; ::_thesis: for v being Element of V . s st ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [v,s] holds
vt . n = (f . s) . v
let v be Element of V . s; ::_thesis: ( ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [v,s] implies vt . n = (f . s) . v )
assume A20: ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [v,s] ; ::_thesis: vt . n = (f . s) . v
now__::_thesis:_not_n_=_{}
assume n = {} ; ::_thesis: contradiction
then s = the carrier of S by A1, A19, A20, XTUPLE_0:1;
hence contradiction by Lm7; ::_thesis: verum
end;
then consider w being FinSequence of NAT , i being Element of NAT such that
A21: n = <*i*> ^ w by FINSEQ_2:130;
A22: w in (doms q) . (i + 1) by A18, A21, TREES_3:48;
A23: i < len p by A5, A18, A17, A21, TREES_3:48;
then reconsider t = p . (i + 1) as c-Term of A,V by Lm2;
consider e being finite DecoratedTree such that
A24: e = q . (i + 1) and
A25: e is_an_evaluation_of t,f by A6, A23, Lm9;
i + 1 in dom p by A23, Lm9;
then reconsider w = w as Node of e by A5, A4, A7, A22, A24, FUNCT_6:22;
dom e = dom t by A25, Def9;
then A26: t . w = [v,s] by A20, A21, A23, TREES_4:12;
thus vt . n = e . w by A5, A21, A23, A24, TREES_4:12
.= (f . s) . v by A25, A26, Def9 ; ::_thesis: verum
end;
hereby ::_thesis: for o being OperSymbol of S st ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [o, the carrier of S] holds
vt . n = (Den (o,A)) . (succ (vt,n))
let s be SortSymbol of S; ::_thesis: for x being Element of the Sorts of A . s st ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [x,s] holds
vt . n = x
let x be Element of the Sorts of A . s; ::_thesis: ( ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [x,s] implies vt . n = x )
assume A27: ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [x,s] ; ::_thesis: vt . n = x
now__::_thesis:_not_n_=_{}
assume n = {} ; ::_thesis: contradiction
then s = the carrier of S by A1, A19, A27, XTUPLE_0:1;
hence contradiction by Lm7; ::_thesis: verum
end;
then consider w being FinSequence of NAT , i being Element of NAT such that
A28: n = <*i*> ^ w by FINSEQ_2:130;
A29: w in (doms q) . (i + 1) by A18, A28, TREES_3:48;
A30: i < len p by A5, A18, A17, A28, TREES_3:48;
then reconsider t = p . (i + 1) as c-Term of A,V by Lm2;
consider e being finite DecoratedTree such that
A31: e = q . (i + 1) and
A32: e is_an_evaluation_of t,f by A6, A30, Lm9;
i + 1 in dom p by A30, Lm9;
then reconsider w = w as Node of e by A5, A4, A7, A29, A31, FUNCT_6:22;
dom e = dom t by A32, Def9;
then A33: t . w = [x,s] by A27, A28, A30, TREES_4:12;
thus vt . n = e . w by A5, A28, A30, A31, TREES_4:12
.= x by A32, A33, Def9 ; ::_thesis: verum
end;
let o1 be OperSymbol of S; ::_thesis: ( ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [o1, the carrier of S] implies vt . n = (Den (o1,A)) . (succ (vt,n)) )
assume A34: ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [o1, the carrier of S] ; ::_thesis: vt . n = (Den (o1,A)) . (succ (vt,n))
percases ( n = {} or n <> {} ) ;
supposeA35: n = {} ; ::_thesis: vt . n = (Den (o1,A)) . (succ (vt,n))
then ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = Sym (o,( the Sorts of A \/ V)) by TREES_4:def_4
.= [o, the carrier of S] by MSAFREE:def_9 ;
then A36: o = o1 by A34, XTUPLE_0:1;
succ (vt,n) = roots q by A35, TREES_9:30;
hence vt . n = (Den (o1,A)) . (succ (vt,n)) by A35, A36, TREES_4:def_4; ::_thesis: verum
end;
suppose n <> {} ; ::_thesis: vt . n = (Den (o1,A)) . (succ (vt,n))
then consider w being FinSequence of NAT , i being Element of NAT such that
A37: n = <*i*> ^ w by FINSEQ_2:130;
reconsider ii = <*i*> as Node of vt by A37, TREES_1:21;
A38: w in (doms q) . (i + 1) by A18, A37, TREES_3:48;
A39: i < len p by A5, A18, A17, A37, TREES_3:48;
then reconsider t = p . (i + 1) as c-Term of A,V by Lm2;
consider e being finite DecoratedTree such that
A40: e = q . (i + 1) and
A41: e is_an_evaluation_of t,f by A6, A39, Lm9;
A42: e = vt | ii by A5, A39, A40, TREES_4:def_4;
i + 1 in dom p by A39, Lm9;
then reconsider w = w as Node of e by A5, A4, A7, A38, A40, FUNCT_6:22;
dom e = dom t by A41, Def9;
then t . w = [o1, the carrier of S] by A34, A37, A39, TREES_4:12;
then e . w = (Den (o1,A)) . (succ (e,w)) by A41, Def9
.= (Den (o1,A)) . (succ (vt,n)) by A37, A42, TREES_9:31 ;
hence vt . n = (Den (o1,A)) . (succ (vt,n)) by A5, A37, A39, A40, TREES_4:12; ::_thesis: verum
end;
end;
end;
theorem Th34: :: MSATERM:34
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for t being c-Term of A,V
for e being finite DecoratedTree st e is_an_evaluation_of t,f holds
for p being Node of t
for n being Node of e st n = p holds
e | n is_an_evaluation_of t | p,f
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for t being c-Term of A,V
for e being finite DecoratedTree st e is_an_evaluation_of t,f holds
for p being Node of t
for n being Node of e st n = p holds
e | n is_an_evaluation_of t | p,f
let A be non-empty MSAlgebra over S; ::_thesis: for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for t being c-Term of A,V
for e being finite DecoratedTree st e is_an_evaluation_of t,f holds
for p being Node of t
for n being Node of e st n = p holds
e | n is_an_evaluation_of t | p,f
let V be Variables of A; ::_thesis: for f being ManySortedFunction of V, the Sorts of A
for t being c-Term of A,V
for e being finite DecoratedTree st e is_an_evaluation_of t,f holds
for p being Node of t
for n being Node of e st n = p holds
e | n is_an_evaluation_of t | p,f
let f be ManySortedFunction of V, the Sorts of A; ::_thesis: for t being c-Term of A,V
for e being finite DecoratedTree st e is_an_evaluation_of t,f holds
for p being Node of t
for n being Node of e st n = p holds
e | n is_an_evaluation_of t | p,f
let t be c-Term of A,V; ::_thesis: for e being finite DecoratedTree st e is_an_evaluation_of t,f holds
for p being Node of t
for n being Node of e st n = p holds
e | n is_an_evaluation_of t | p,f
let e be finite DecoratedTree; ::_thesis: ( e is_an_evaluation_of t,f implies for p being Node of t
for n being Node of e st n = p holds
e | n is_an_evaluation_of t | p,f )
assume that
A1: dom e = dom t and
A2: for p being Node of e holds
( ( for s being SortSymbol of S
for v being Element of V . s st t . p = [v,s] holds
e . p = (f . s) . v ) & ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st t . p = [x,s] holds
e . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds
e . p = (Den (o,A)) . (succ (e,p)) ) ) ; :: according to MSATERM:def_9 ::_thesis: for p being Node of t
for n being Node of e st n = p holds
e | n is_an_evaluation_of t | p,f
let p be Node of t; ::_thesis: for n being Node of e st n = p holds
e | n is_an_evaluation_of t | p,f
let n be Node of e; ::_thesis: ( n = p implies e | n is_an_evaluation_of t | p,f )
set vt = e | n;
set tp = t | p;
A3: dom (e | n) = (dom e) | n by TREES_2:def_10;
assume A4: n = p ; ::_thesis: e | n is_an_evaluation_of t | p,f
hence dom (e | n) = dom (t | p) by A1, A3, TREES_2:def_10; :: according to MSATERM:def_9 ::_thesis: for p being Node of (e | n) holds
( ( for s being SortSymbol of S
for v being Element of V . s st (t | p) . p = [v,s] holds
(e | n) . p = (f . s) . v ) & ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st (t | p) . p = [x,s] holds
(e | n) . p = x ) & ( for o being OperSymbol of S st (t | p) . p = [o, the carrier of S] holds
(e | n) . p = (Den (o,A)) . (succ ((e | n),p)) ) )
let q be Node of (e | n); ::_thesis: ( ( for s being SortSymbol of S
for v being Element of V . s st (t | p) . q = [v,s] holds
(e | n) . q = (f . s) . v ) & ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st (t | p) . q = [x,s] holds
(e | n) . q = x ) & ( for o being OperSymbol of S st (t | p) . q = [o, the carrier of S] holds
(e | n) . q = (Den (o,A)) . (succ ((e | n),q)) ) )
reconsider nq = n ^ q as Node of e by A3, TREES_1:def_6;
reconsider pq = p ^ q as Node of t by A1, A4, A3, TREES_1:def_6;
hereby ::_thesis: ( ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st (t | p) . q = [x,s] holds
(e | n) . q = x ) & ( for o being OperSymbol of S st (t | p) . q = [o, the carrier of S] holds
(e | n) . q = (Den (o,A)) . (succ ((e | n),q)) ) )
let s be SortSymbol of S; ::_thesis: for v being Element of V . s st (t | p) . q = [v,s] holds
(e | n) . q = (f . s) . v
let v be Element of V . s; ::_thesis: ( (t | p) . q = [v,s] implies (e | n) . q = (f . s) . v )
assume (t | p) . q = [v,s] ; ::_thesis: (e | n) . q = (f . s) . v
then t . pq = [v,s] by A1, A4, A3, TREES_2:def_10;
then e . nq = (f . s) . v by A2, A4;
hence (e | n) . q = (f . s) . v by A3, TREES_2:def_10; ::_thesis: verum
end;
hereby ::_thesis: for o being OperSymbol of S st (t | p) . q = [o, the carrier of S] holds
(e | n) . q = (Den (o,A)) . (succ ((e | n),q))
let s be SortSymbol of S; ::_thesis: for x being Element of the Sorts of A . s st (t | p) . q = [x,s] holds
(e | n) . q = x
let x be Element of the Sorts of A . s; ::_thesis: ( (t | p) . q = [x,s] implies (e | n) . q = x )
assume (t | p) . q = [x,s] ; ::_thesis: (e | n) . q = x
then t . pq = [x,s] by A1, A4, A3, TREES_2:def_10;
then e . nq = x by A2, A4;
hence (e | n) . q = x by A3, TREES_2:def_10; ::_thesis: verum
end;
let o be OperSymbol of S; ::_thesis: ( (t | p) . q = [o, the carrier of S] implies (e | n) . q = (Den (o,A)) . (succ ((e | n),q)) )
assume (t | p) . q = [o, the carrier of S] ; ::_thesis: (e | n) . q = (Den (o,A)) . (succ ((e | n),q))
then t . pq = [o, the carrier of S] by A1, A4, A3, TREES_2:def_10;
then e . nq = (Den (o,A)) . (succ (e,nq)) by A2, A4;
then (e | n) . q = (Den (o,A)) . (succ (e,(n ^ q))) by A3, TREES_2:def_10;
hence (e | n) . q = (Den (o,A)) . (succ ((e | n),q)) by TREES_9:31; ::_thesis: verum
end;
theorem Th35: :: MSATERM:35
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f holds
ex q being DTree-yielding FinSequence st
( len q = len p & vt = ((Den (o,A)) . (roots q)) -tree q & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f holds
ex q being DTree-yielding FinSequence st
( len q = len p & vt = ((Den (o,A)) . (roots q)) -tree q & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) )
let A be non-empty MSAlgebra over S; ::_thesis: for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f holds
ex q being DTree-yielding FinSequence st
( len q = len p & vt = ((Den (o,A)) . (roots q)) -tree q & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) )
let V be Variables of A; ::_thesis: for f being ManySortedFunction of V, the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f holds
ex q being DTree-yielding FinSequence st
( len q = len p & vt = ((Den (o,A)) . (roots q)) -tree q & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) )
let f be ManySortedFunction of V, the Sorts of A; ::_thesis: for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f holds
ex q being DTree-yielding FinSequence st
( len q = len p & vt = ((Den (o,A)) . (roots q)) -tree q & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) )
let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of o,A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f holds
ex q being DTree-yielding FinSequence st
( len q = len p & vt = ((Den (o,A)) . (roots q)) -tree q & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) )
let p be ArgumentSeq of o,A,V; ::_thesis: for vt being finite DecoratedTree st vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f holds
ex q being DTree-yielding FinSequence st
( len q = len p & vt = ((Den (o,A)) . (roots q)) -tree q & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) )
let vt be finite DecoratedTree; ::_thesis: ( vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f implies ex q being DTree-yielding FinSequence st
( len q = len p & vt = ((Den (o,A)) . (roots q)) -tree q & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) ) )
assume A1: vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f ; ::_thesis: ex q being DTree-yielding FinSequence st
( len q = len p & vt = ((Den (o,A)) . (roots q)) -tree q & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) )
reconsider r = {} as empty Element of dom vt by TREES_1:22;
consider x being set , q being DTree-yielding FinSequence such that
A2: vt = x -tree q by TREES_9:8;
A3: dom vt = tree (doms q) by A2, TREES_4:10;
take q ; ::_thesis: ( len q = len p & vt = ((Den (o,A)) . (roots q)) -tree q & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) )
A4: len (doms q) = len q by TREES_3:38;
A5: Sym (o,( the Sorts of A \/ V)) = [o, the carrier of S] by MSAFREE:def_9;
then A6: dom vt = dom ([o, the carrier of S] -tree p) by A1, Def9;
then dom vt = tree (doms p) by TREES_4:10;
then A7: doms q = doms p by A3, TREES_3:50;
hence len q = len p by A4, TREES_3:38; ::_thesis: ( vt = ((Den (o,A)) . (roots q)) -tree q & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) )
([o, the carrier of S] -tree p) . r = [o, the carrier of S] by TREES_4:def_4;
then vt . r = (Den (o,A)) . (succ (vt,r)) by A5, A1, Def9
.= (Den (o,A)) . (roots q) by A2, TREES_9:30 ;
hence vt = ((Den (o,A)) . (roots q)) -tree q by A2, TREES_4:def_4; ::_thesis: for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f )
let i be Nat; ::_thesis: for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f )
let t be c-Term of A,V; ::_thesis: ( i in dom p & t = p . i implies ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) )
assume that
A8: i in dom p and
A9: t = p . i ; ::_thesis: ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f )
reconsider u = {} as Node of t by TREES_1:22;
consider k being Element of NAT such that
A10: i = k + 1 and
A11: k < len p by A8, Lm1;
<*k*> ^ u = <*k*> by FINSEQ_1:34;
then reconsider r = <*k*> as Node of vt by A6, A9, A10, A11, TREES_4:11;
take e = vt | r; ::_thesis: ( e = q . i & e is_an_evaluation_of t,f )
len (doms p) = len p by TREES_3:38;
hence e = q . i by A2, A7, A4, A10, A11, TREES_4:def_4; ::_thesis: e is_an_evaluation_of t,f
reconsider r1 = r as Node of ([o, the carrier of S] -tree p) by A5, A1, Def9;
t = ([o, the carrier of S] -tree p) | r1 by A9, A10, A11, TREES_4:def_4;
hence e is_an_evaluation_of t,f by A5, A1, Th34; ::_thesis: verum
end;
theorem Th36: :: MSATERM:36
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f
let A be non-empty MSAlgebra over S; ::_thesis: for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f
let V be Variables of A; ::_thesis: for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f
let t be c-Term of A,V; ::_thesis: for f being ManySortedFunction of V, the Sorts of A ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f
let f be ManySortedFunction of V, the Sorts of A; ::_thesis: ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f
defpred S1[ set ] means ex t being c-Term of A,V ex vt being finite DecoratedTree st
( t = $1 & vt is_an_evaluation_of t,f );
A1: for o being OperSymbol of S
for p being ArgumentSeq of o,A,V st ( for t being c-Term of A,V st t in rng p holds
S1[t] ) holds
S1[(Sym (o,( the Sorts of A \/ V))) -tree p]
proof
let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of o,A,V st ( for t being c-Term of A,V st t in rng p holds
S1[t] ) holds
S1[(Sym (o,( the Sorts of A \/ V))) -tree p]
let p be ArgumentSeq of o,A,V; ::_thesis: ( ( for t being c-Term of A,V st t in rng p holds
S1[t] ) implies S1[(Sym (o,( the Sorts of A \/ V))) -tree p] )
assume A2: for t being c-Term of A,V st t in rng p holds
ex u being c-Term of A,V ex vt being finite DecoratedTree st
( u = t & vt is_an_evaluation_of u,f ) ; ::_thesis: S1[(Sym (o,( the Sorts of A \/ V))) -tree p]
defpred S2[ set , set ] means ex t being c-Term of A,V ex vt being finite DecoratedTree st
( $2 = vt & t = p . $1 & vt is_an_evaluation_of t,f );
A3: for e being set st e in dom p holds
ex u being set st S2[e,u]
proof
let x be set ; ::_thesis: ( x in dom p implies ex u being set st S2[x,u] )
assume x in dom p ; ::_thesis: ex u being set st S2[x,u]
then A4: p . x in rng p by FUNCT_1:def_3;
rng p c= S -Terms ( the Sorts of A \/ V) by FINSEQ_1:def_4;
then reconsider t = p . x as c-Term of A,V by A4;
ex u being c-Term of A,V ex vt being finite DecoratedTree st
( u = t & vt is_an_evaluation_of u,f ) by A2, A4;
hence ex u being set st S2[x,u] ; ::_thesis: verum
end;
consider q being Function such that
A5: ( dom q = dom p & ( for x being set st x in dom p holds
S2[x,q . x] ) ) from CLASSES1:sch_1(A3);
dom p = Seg (len p) by FINSEQ_1:def_3;
then reconsider q = q as FinSequence by A5, FINSEQ_1:def_2;
A6: len p = len q by A5, FINSEQ_3:29;
now__::_thesis:_for_x_being_set_st_x_in_dom_q_holds_
q_._x_is_DecoratedTree
let x be set ; ::_thesis: ( x in dom q implies q . x is DecoratedTree )
assume x in dom q ; ::_thesis: q . x is DecoratedTree
then ex t being c-Term of A,V ex vt being finite DecoratedTree st
( q . x = vt & t = p . x & vt is_an_evaluation_of t,f ) by A5;
hence q . x is DecoratedTree ; ::_thesis: verum
end;
then reconsider q = q as DTree-yielding FinSequence by TREES_3:24;
now__::_thesis:_for_i_being_Nat
for_t_being_c-Term_of_A,V_st_i_in_dom_p_&_t_=_p_._i_holds_
ex_vt_being_finite_DecoratedTree_st_
(_vt_=_q_._i_&_vt_is_an_evaluation_of_t,f_)
let i be Nat; ::_thesis: for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f )
let t be c-Term of A,V; ::_thesis: ( i in dom p & t = p . i implies ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) )
assume i in dom p ; ::_thesis: ( t = p . i implies ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) )
then ex t being c-Term of A,V ex vt being finite DecoratedTree st
( q . i = vt & t = p . i & vt is_an_evaluation_of t,f ) by A5;
hence ( t = p . i implies ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) ; ::_thesis: verum
end;
then ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f ) by A6, Th33;
hence S1[(Sym (o,( the Sorts of A \/ V))) -tree p] ; ::_thesis: verum
end;
A7: for s being SortSymbol of S
for v being Element of V . s holds S1[ root-tree [v,s]]
proof
let s be SortSymbol of S; ::_thesis: for v being Element of V . s holds S1[ root-tree [v,s]]
let x be Element of V . s; ::_thesis: S1[ root-tree [x,s]]
reconsider t = root-tree [x,s] as c-Term of A,V by Th8;
take t ; ::_thesis: ex vt being finite DecoratedTree st
( t = root-tree [x,s] & vt is_an_evaluation_of t,f )
take root-tree ((f . s) . x) ; ::_thesis: ( t = root-tree [x,s] & root-tree ((f . s) . x) is_an_evaluation_of t,f )
thus t = root-tree [x,s] ; ::_thesis: root-tree ((f . s) . x) is_an_evaluation_of t,f
thus root-tree ((f . s) . x) is_an_evaluation_of t,f by Th32; ::_thesis: verum
end;
A8: for s being SortSymbol of S
for x being Element of the Sorts of A . s holds S1[ root-tree [x,s]]
proof
let s be SortSymbol of S; ::_thesis: for x being Element of the Sorts of A . s holds S1[ root-tree [x,s]]
let x be Element of the Sorts of A . s; ::_thesis: S1[ root-tree [x,s]]
reconsider t = root-tree [x,s] as c-Term of A,V by Th6;
take t ; ::_thesis: ex vt being finite DecoratedTree st
( t = root-tree [x,s] & vt is_an_evaluation_of t,f )
take root-tree x ; ::_thesis: ( t = root-tree [x,s] & root-tree x is_an_evaluation_of t,f )
thus t = root-tree [x,s] ; ::_thesis: root-tree x is_an_evaluation_of t,f
thus root-tree x is_an_evaluation_of t,f by Th31; ::_thesis: verum
end;
for t being c-Term of A,V holds S1[t] from MSATERM:sch_2(A8, A7, A1);
then ex u being c-Term of A,V ex vt being finite DecoratedTree st
( u = t & vt is_an_evaluation_of u,f ) ;
hence ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f ; ::_thesis: verum
end;
theorem Th37: :: MSATERM:37
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds
e1 = e2
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds
e1 = e2
let A be non-empty MSAlgebra over S; ::_thesis: for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds
e1 = e2
let V be Variables of A; ::_thesis: for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds
e1 = e2
let t be c-Term of A,V; ::_thesis: for f being ManySortedFunction of V, the Sorts of A
for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds
e1 = e2
let f be ManySortedFunction of V, the Sorts of A; ::_thesis: for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds
e1 = e2
defpred S1[ c-Term of A,V] means for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of $1,f & e2 is_an_evaluation_of $1,f holds
e1 = e2;
A1: now__::_thesis:_for_s_being_SortSymbol_of_S
for_v_being_Element_of_V_._s_holds_S1[v_-term_A]
let s be SortSymbol of S; ::_thesis: for v being Element of V . s holds S1[v -term A]
let v be Element of V . s; ::_thesis: S1[v -term A]
thus S1[v -term A] ::_thesis: verum
proof
let e1, e2 be finite DecoratedTree; ::_thesis: ( e1 is_an_evaluation_of v -term A,f & e2 is_an_evaluation_of v -term A,f implies e1 = e2 )
set t = v -term A;
assume that
A2: e1 is_an_evaluation_of v -term A,f and
A3: e2 is_an_evaluation_of v -term A,f ; ::_thesis: e1 = e2
A4: dom e1 = dom (v -term A) by A2, Def9;
A5: {} is Node of e1 by TREES_1:22;
A6: (root-tree [v,s]) . {} = [v,s] by TREES_4:3;
then e1 . {} = (f . s) . v by A2, A5, Def9;
then A7: e1 = root-tree ((f . s) . v) by A4, TREES_4:3, TREES_4:5;
A8: dom e2 = dom (v -term A) by A3, Def9;
then e2 . {} = (f . s) . v by A3, A4, A6, A5, Def9;
hence e1 = e2 by A8, A7, TREES_4:3, TREES_4:5; ::_thesis: verum
end;
end;
A9: now__::_thesis:_for_o_being_OperSymbol_of_S
for_p_being_ArgumentSeq_of_o,A,V_st_(_for_t_being_c-Term_of_A,V_st_t_in_rng_p_holds_
S1[t]_)_holds_
S1[(Sym_(o,(_the_Sorts_of_A_\/_V)))_-tree_p]
let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of o,A,V st ( for t being c-Term of A,V st t in rng p holds
S1[t] ) holds
S1[(Sym (o,( the Sorts of A \/ V))) -tree p]
let p be ArgumentSeq of o,A,V; ::_thesis: ( ( for t being c-Term of A,V st t in rng p holds
S1[t] ) implies S1[(Sym (o,( the Sorts of A \/ V))) -tree p] )
assume A10: for t being c-Term of A,V st t in rng p holds
S1[t] ; ::_thesis: S1[(Sym (o,( the Sorts of A \/ V))) -tree p]
thus S1[(Sym (o,( the Sorts of A \/ V))) -tree p] ::_thesis: verum
proof
set t = (Sym (o,( the Sorts of A \/ V))) -tree p;
let e1, e2 be finite DecoratedTree; ::_thesis: ( e1 is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f & e2 is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f implies e1 = e2 )
assume that
A11: e1 is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f and
A12: e2 is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f ; ::_thesis: e1 = e2
consider q1 being DTree-yielding FinSequence such that
A13: len q1 = len p and
A14: e1 = ((Den (o,A)) . (roots q1)) -tree q1 and
A15: for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q1 . i & vt is_an_evaluation_of t,f ) by A11, Th35;
consider q2 being DTree-yielding FinSequence such that
A16: len q2 = len p and
A17: e2 = ((Den (o,A)) . (roots q2)) -tree q2 and
A18: for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q2 . i & vt is_an_evaluation_of t,f ) by A12, Th35;
A19: now__::_thesis:_for_i_being_Element_of_NAT_st_i_<_len_p_holds_
q1_._(i_+_1)_=_q2_._(i_+_1)
let i be Element of NAT ; ::_thesis: ( i < len p implies q1 . (i + 1) = q2 . (i + 1) )
assume A20: i < len p ; ::_thesis: q1 . (i + 1) = q2 . (i + 1)
then reconsider t = p . (i + 1) as c-Term of A,V by Lm2;
A21: ex vt2 being finite DecoratedTree st
( vt2 = q2 . (i + 1) & vt2 is_an_evaluation_of t,f ) by A18, A20, Lm9;
ex vt1 being finite DecoratedTree st
( vt1 = q1 . (i + 1) & vt1 is_an_evaluation_of t,f ) by A15, A20, Lm9;
hence q1 . (i + 1) = q2 . (i + 1) by A10, A20, A21, Lm9; ::_thesis: verum
end;
A22: now__::_thesis:_for_i_being_Nat_st_i_in_dom_q1_holds_
q1_._i_=_q2_._i
let i be Nat; ::_thesis: ( i in dom q1 implies q1 . i = q2 . i )
assume i in dom q1 ; ::_thesis: q1 . i = q2 . i
then ex k being Element of NAT st
( i = k + 1 & k < len q1 ) by Lm1;
hence q1 . i = q2 . i by A13, A19; ::_thesis: verum
end;
A23: dom q2 = Seg (len q2) by FINSEQ_1:def_3;
dom q1 = Seg (len q1) by FINSEQ_1:def_3;
then q1 = q2 by A13, A16, A23, A22, FINSEQ_1:13;
hence e1 = e2 by A14, A17; ::_thesis: verum
end;
end;
A24: now__::_thesis:_for_s_being_SortSymbol_of_S
for_x_being_Element_of_the_Sorts_of_A_._s_holds_S1[x_-term_(A,V)]
let s be SortSymbol of S; ::_thesis: for x being Element of the Sorts of A . s holds S1[x -term (A,V)]
let x be Element of the Sorts of A . s; ::_thesis: S1[x -term (A,V)]
thus S1[x -term (A,V)] ::_thesis: verum
proof
let e1, e2 be finite DecoratedTree; ::_thesis: ( e1 is_an_evaluation_of x -term (A,V),f & e2 is_an_evaluation_of x -term (A,V),f implies e1 = e2 )
set t = x -term (A,V);
assume that
A25: e1 is_an_evaluation_of x -term (A,V),f and
A26: e2 is_an_evaluation_of x -term (A,V),f ; ::_thesis: e1 = e2
A27: dom e1 = dom (x -term (A,V)) by A25, Def9;
A28: {} is Node of e1 by TREES_1:22;
A29: (root-tree [x,s]) . {} = [x,s] by TREES_4:3;
then e1 . {} = x by A25, A28, Def9;
then A30: e1 = root-tree x by A27, TREES_4:3, TREES_4:5;
A31: dom e2 = dom (x -term (A,V)) by A26, Def9;
then e2 . {} = x by A26, A27, A29, A28, Def9;
hence e1 = e2 by A31, A30, TREES_4:3, TREES_4:5; ::_thesis: verum
end;
end;
for t being c-Term of A,V holds S1[t] from MSATERM:sch_3(A24, A1, A9);
hence for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds
e1 = e2 ; ::_thesis: verum
end;
theorem Th38: :: MSATERM:38
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
vt . {} in the Sorts of A . (the_sort_of t)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
vt . {} in the Sorts of A . (the_sort_of t)
let A be non-empty MSAlgebra over S; ::_thesis: for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
vt . {} in the Sorts of A . (the_sort_of t)
let V be Variables of A; ::_thesis: for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
vt . {} in the Sorts of A . (the_sort_of t)
let t be c-Term of A,V; ::_thesis: for f being ManySortedFunction of V, the Sorts of A
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
vt . {} in the Sorts of A . (the_sort_of t)
let f be ManySortedFunction of V, the Sorts of A; ::_thesis: for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
vt . {} in the Sorts of A . (the_sort_of t)
defpred S1[ c-Term of A,V] means for vt being finite DecoratedTree st vt is_an_evaluation_of $1,f holds
vt . {} in the Sorts of A . (the_sort_of $1);
A1: now__::_thesis:_for_s_being_SortSymbol_of_S
for_v_being_Element_of_V_._s_holds_S1[v_-term_A]
let s be SortSymbol of S; ::_thesis: for v being Element of V . s holds S1[v -term A]
let v be Element of V . s; ::_thesis: S1[v -term A]
thus S1[v -term A] ::_thesis: verum
proof
let vt be finite DecoratedTree; ::_thesis: ( vt is_an_evaluation_of v -term A,f implies vt . {} in the Sorts of A . (the_sort_of (v -term A)) )
set t = v -term A;
assume A2: vt is_an_evaluation_of v -term A,f ; ::_thesis: vt . {} in the Sorts of A . (the_sort_of (v -term A))
root-tree ((f . s) . v) is_an_evaluation_of v -term A,f by Th32;
then vt = root-tree ((f . s) . v) by A2, Th37;
then A3: vt . {} = (f . s) . v by TREES_4:3;
s = the_sort_of (v -term A) by Th19;
hence vt . {} in the Sorts of A . (the_sort_of (v -term A)) by A3; ::_thesis: verum
end;
end;
A4: now__::_thesis:_for_o_being_OperSymbol_of_S
for_p_being_ArgumentSeq_of_o,A,V_st_(_for_t_being_c-Term_of_A,V_st_t_in_rng_p_holds_
S1[t]_)_holds_
S1[(Sym_(o,(_the_Sorts_of_A_\/_V)))_-tree_p]
let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of o,A,V st ( for t being c-Term of A,V st t in rng p holds
S1[t] ) holds
S1[(Sym (o,( the Sorts of A \/ V))) -tree p]
let p be ArgumentSeq of o,A,V; ::_thesis: ( ( for t being c-Term of A,V st t in rng p holds
S1[t] ) implies S1[(Sym (o,( the Sorts of A \/ V))) -tree p] )
assume A5: for t being c-Term of A,V st t in rng p holds
S1[t] ; ::_thesis: S1[(Sym (o,( the Sorts of A \/ V))) -tree p]
thus S1[(Sym (o,( the Sorts of A \/ V))) -tree p] ::_thesis: verum
proof
let vt be finite DecoratedTree; ::_thesis: ( vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f implies vt . {} in the Sorts of A . (the_sort_of ((Sym (o,( the Sorts of A \/ V))) -tree p)) )
set t = (Sym (o,( the Sorts of A \/ V))) -tree p;
A6: dom ( the Sorts of A * the ResultSort of S) = the carrier' of S by PARTFUN1:def_2;
assume vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f ; ::_thesis: vt . {} in the Sorts of A . (the_sort_of ((Sym (o,( the Sorts of A \/ V))) -tree p))
then consider q being DTree-yielding FinSequence such that
A7: len q = len p and
A8: vt = ((Den (o,A)) . (roots q)) -tree q and
A9: for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) by Th35;
A10: vt . {} = (Den (o,A)) . (roots q) by A8, TREES_4:def_4;
now__::_thesis:_(_dom_(roots_q)_=_dom_(_the_Sorts_of_A_*_(the_arity_of_o))_&_(_for_x_being_set_st_x_in_dom_(_the_Sorts_of_A_*_(the_arity_of_o))_holds_
(roots_q)_._x_in_(_the_Sorts_of_A_*_(the_arity_of_o))_._x_)_)
A11: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4;
A12: dom the Sorts of A = the carrier of S by PARTFUN1:def_2;
A13: dom (roots q) = dom q by TREES_3:def_18;
hence A14: dom (roots q) = Seg (len q) by FINSEQ_1:def_3
.= Seg (len (the_arity_of o)) by A7, Lm8
.= dom (the_arity_of o) by FINSEQ_1:def_3
.= dom ( the Sorts of A * (the_arity_of o)) by A12, A11, RELAT_1:27 ;
::_thesis: for x being set st x in dom ( the Sorts of A * (the_arity_of o)) holds
(roots q) . x in ( the Sorts of A * (the_arity_of o)) . x
let x be set ; ::_thesis: ( x in dom ( the Sorts of A * (the_arity_of o)) implies (roots q) . x in ( the Sorts of A * (the_arity_of o)) . x )
assume A15: x in dom ( the Sorts of A * (the_arity_of o)) ; ::_thesis: (roots q) . x in ( the Sorts of A * (the_arity_of o)) . x
then consider i being Element of NAT such that
A16: x = i + 1 and
A17: i < len q by A13, A14, Lm1;
A18: ex T being DecoratedTree st
( T = q . (i + 1) & (roots q) . (i + 1) = T . {} ) by A13, A14, A15, A16, TREES_3:def_18;
i + 1 in dom p by A7, A17, Lm9;
then A19: ex t being c-Term of A,V st
( t = p . (i + 1) & t = p /. (i + 1) & the_sort_of t = (the_arity_of o) . (i + 1) & the_sort_of t = (the_arity_of o) /. (i + 1) ) by Lm8;
reconsider t = p . (i + 1) as c-Term of A,V by A7, A17, Lm2;
consider vt being finite DecoratedTree such that
A20: vt = q . (i + 1) and
A21: vt is_an_evaluation_of t,f by A7, A9, A17, Lm9;
vt . {} in the Sorts of A . (the_sort_of t) by A5, A7, A17, A21, Lm9;
hence (roots q) . x in ( the Sorts of A * (the_arity_of o)) . x by A15, A16, A18, A20, A19, FUNCT_1:12; ::_thesis: verum
end;
then roots q in product ( the Sorts of A * (the_arity_of o)) by CARD_3:9;
then roots q in ( the Sorts of A #) . (the_arity_of o) by FINSEQ_2:def_5;
then A22: roots q in ( the Sorts of A #) . ( the Arity of S . o) by MSUALG_1:def_1;
dom (( the Sorts of A #) * the Arity of S) = the carrier' of S by PARTFUN1:def_2;
then roots q in (( the Sorts of A #) * the Arity of S) . o by A22, FUNCT_1:12;
then A23: roots q in Args (o,A) by MSUALG_1:def_4;
Result (o,A) = ( the Sorts of A * the ResultSort of S) . o by MSUALG_1:def_5
.= the Sorts of A . ( the ResultSort of S . o) by A6, FUNCT_1:12
.= the Sorts of A . (the_result_sort_of o) by MSUALG_1:def_2
.= the Sorts of A . (the_sort_of ((Sym (o,( the Sorts of A \/ V))) -tree p)) by Th20 ;
hence vt . {} in the Sorts of A . (the_sort_of ((Sym (o,( the Sorts of A \/ V))) -tree p)) by A10, A23, FUNCT_2:5; ::_thesis: verum
end;
end;
A24: now__::_thesis:_for_s_being_SortSymbol_of_S
for_x_being_Element_of_the_Sorts_of_A_._s_holds_S1[x_-term_(A,V)]
let s be SortSymbol of S; ::_thesis: for x being Element of the Sorts of A . s holds S1[x -term (A,V)]
let x be Element of the Sorts of A . s; ::_thesis: S1[x -term (A,V)]
thus S1[x -term (A,V)] ::_thesis: verum
proof
let vt be finite DecoratedTree; ::_thesis: ( vt is_an_evaluation_of x -term (A,V),f implies vt . {} in the Sorts of A . (the_sort_of (x -term (A,V))) )
set t = x -term (A,V);
assume A25: vt is_an_evaluation_of x -term (A,V),f ; ::_thesis: vt . {} in the Sorts of A . (the_sort_of (x -term (A,V)))
root-tree x is_an_evaluation_of x -term (A,V),f by Th31;
then vt = root-tree x by A25, Th37;
then A26: vt . {} = x by TREES_4:3;
s = the_sort_of (x -term (A,V)) by Th15;
hence vt . {} in the Sorts of A . (the_sort_of (x -term (A,V))) by A26; ::_thesis: verum
end;
end;
for t being c-Term of A,V holds S1[t] from MSATERM:sch_3(A24, A1, A4);
hence for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
vt . {} in the Sorts of A . (the_sort_of t) ; ::_thesis: verum
end;
definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let V be Variables of A;
let t be c-Term of A,V;
let f be ManySortedFunction of V, the Sorts of A;
funct @ f -> Element of the Sorts of A . (the_sort_of t) means :Def10: :: MSATERM:def 10
ex vt being finite DecoratedTree st
( vt is_an_evaluation_of t,f & it = vt . {} );
existence
ex b1 being Element of the Sorts of A . (the_sort_of t) ex vt being finite DecoratedTree st
( vt is_an_evaluation_of t,f & b1 = vt . {} )
proof
consider vt being finite DecoratedTree such that
A1: vt is_an_evaluation_of t,f by Th36;
reconsider tf = vt . {} as Element of the Sorts of A . (the_sort_of t) by A1, Th38;
take tf ; ::_thesis: ex vt being finite DecoratedTree st
( vt is_an_evaluation_of t,f & tf = vt . {} )
take vt ; ::_thesis: ( vt is_an_evaluation_of t,f & tf = vt . {} )
thus ( vt is_an_evaluation_of t,f & tf = vt . {} ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of the Sorts of A . (the_sort_of t) st ex vt being finite DecoratedTree st
( vt is_an_evaluation_of t,f & b1 = vt . {} ) & ex vt being finite DecoratedTree st
( vt is_an_evaluation_of t,f & b2 = vt . {} ) holds
b1 = b2 by Th37;
end;
:: deftheorem Def10 defines @ MSATERM:def_10_:_
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for b6 being Element of the Sorts of A . (the_sort_of t) holds
( b6 = t @ f iff ex vt being finite DecoratedTree st
( vt is_an_evaluation_of t,f & b6 = vt . {} ) );
theorem Th39: :: MSATERM:39
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for t being c-Term of A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
t @ f = vt . {}
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for t being c-Term of A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
t @ f = vt . {}
let A be non-empty MSAlgebra over S; ::_thesis: for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for t being c-Term of A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
t @ f = vt . {}
let V be Variables of A; ::_thesis: for f being ManySortedFunction of V, the Sorts of A
for t being c-Term of A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
t @ f = vt . {}
let f be ManySortedFunction of V, the Sorts of A; ::_thesis: for t being c-Term of A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
t @ f = vt . {}
let t be c-Term of A,V; ::_thesis: for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
t @ f = vt . {}
A1: ex e being finite DecoratedTree st
( e is_an_evaluation_of t,f & t @ f = e . {} ) by Def10;
let vt be finite DecoratedTree; ::_thesis: ( vt is_an_evaluation_of t,f implies t @ f = vt . {} )
assume vt is_an_evaluation_of t,f ; ::_thesis: t @ f = vt . {}
hence t @ f = vt . {} by A1, Th37; ::_thesis: verum
end;
theorem :: MSATERM:40
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for t being c-Term of A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
for p being Node of t holds vt . p = (t | p) @ f
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for t being c-Term of A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
for p being Node of t holds vt . p = (t | p) @ f
let A be non-empty MSAlgebra over S; ::_thesis: for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for t being c-Term of A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
for p being Node of t holds vt . p = (t | p) @ f
let V be Variables of A; ::_thesis: for f being ManySortedFunction of V, the Sorts of A
for t being c-Term of A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
for p being Node of t holds vt . p = (t | p) @ f
let f be ManySortedFunction of V, the Sorts of A; ::_thesis: for t being c-Term of A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
for p being Node of t holds vt . p = (t | p) @ f
let t be c-Term of A,V; ::_thesis: for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
for p being Node of t holds vt . p = (t | p) @ f
let vt be finite DecoratedTree; ::_thesis: ( vt is_an_evaluation_of t,f implies for p being Node of t holds vt . p = (t | p) @ f )
assume A1: vt is_an_evaluation_of t,f ; ::_thesis: for p being Node of t holds vt . p = (t | p) @ f
let p be Node of t; ::_thesis: vt . p = (t | p) @ f
reconsider n = p as Node of vt by A1, Def9;
A2: n ^ {} = n by FINSEQ_1:34;
A3: {} in (dom vt) | p by TREES_1:22;
(t | p) @ f = (vt | n) . (<*> NAT) by A1, Th34, Th39;
hence vt . p = (t | p) @ f by A2, A3, TREES_2:def_10; ::_thesis: verum
end;
theorem :: MSATERM:41
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for s being SortSymbol of S
for x being Element of the Sorts of A . s holds (x -term (A,V)) @ f = x
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for s being SortSymbol of S
for x being Element of the Sorts of A . s holds (x -term (A,V)) @ f = x
let A be non-empty MSAlgebra over S; ::_thesis: for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for s being SortSymbol of S
for x being Element of the Sorts of A . s holds (x -term (A,V)) @ f = x
let V be Variables of A; ::_thesis: for f being ManySortedFunction of V, the Sorts of A
for s being SortSymbol of S
for x being Element of the Sorts of A . s holds (x -term (A,V)) @ f = x
let f be ManySortedFunction of V, the Sorts of A; ::_thesis: for s being SortSymbol of S
for x being Element of the Sorts of A . s holds (x -term (A,V)) @ f = x
let s be SortSymbol of S; ::_thesis: for x being Element of the Sorts of A . s holds (x -term (A,V)) @ f = x
let x be Element of the Sorts of A . s; ::_thesis: (x -term (A,V)) @ f = x
x = (root-tree x) . {} by TREES_4:3;
hence (x -term (A,V)) @ f = x by Th31, Th39; ::_thesis: verum
end;
theorem :: MSATERM:42
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for s being SortSymbol of S
for v being Element of V . s holds (v -term A) @ f = (f . s) . v
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for s being SortSymbol of S
for v being Element of V . s holds (v -term A) @ f = (f . s) . v
let A be non-empty MSAlgebra over S; ::_thesis: for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for s being SortSymbol of S
for v being Element of V . s holds (v -term A) @ f = (f . s) . v
let V be Variables of A; ::_thesis: for f being ManySortedFunction of V, the Sorts of A
for s being SortSymbol of S
for v being Element of V . s holds (v -term A) @ f = (f . s) . v
let f be ManySortedFunction of V, the Sorts of A; ::_thesis: for s being SortSymbol of S
for v being Element of V . s holds (v -term A) @ f = (f . s) . v
let s be SortSymbol of S; ::_thesis: for v being Element of V . s holds (v -term A) @ f = (f . s) . v
let v be Element of V . s; ::_thesis: (v -term A) @ f = (f . s) . v
(f . s) . v = (root-tree ((f . s) . v)) . {} by TREES_4:3;
hence (v -term A) @ f = (f . s) . v by Th32, Th39; ::_thesis: verum
end;
theorem :: MSATERM:43
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for q being FinSequence st len q = len p & ( for i being Nat st i in dom p holds
for t being c-Term of A,V st t = p . i holds
q . i = t @ f ) holds
((Sym (o,( the Sorts of A \/ V))) -tree p) @ f = (Den (o,A)) . q
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for q being FinSequence st len q = len p & ( for i being Nat st i in dom p holds
for t being c-Term of A,V st t = p . i holds
q . i = t @ f ) holds
((Sym (o,( the Sorts of A \/ V))) -tree p) @ f = (Den (o,A)) . q
let A be non-empty MSAlgebra over S; ::_thesis: for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for q being FinSequence st len q = len p & ( for i being Nat st i in dom p holds
for t being c-Term of A,V st t = p . i holds
q . i = t @ f ) holds
((Sym (o,( the Sorts of A \/ V))) -tree p) @ f = (Den (o,A)) . q
let V be Variables of A; ::_thesis: for f being ManySortedFunction of V, the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for q being FinSequence st len q = len p & ( for i being Nat st i in dom p holds
for t being c-Term of A,V st t = p . i holds
q . i = t @ f ) holds
((Sym (o,( the Sorts of A \/ V))) -tree p) @ f = (Den (o,A)) . q
let f be ManySortedFunction of V, the Sorts of A; ::_thesis: for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for q being FinSequence st len q = len p & ( for i being Nat st i in dom p holds
for t being c-Term of A,V st t = p . i holds
q . i = t @ f ) holds
((Sym (o,( the Sorts of A \/ V))) -tree p) @ f = (Den (o,A)) . q
let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of o,A,V
for q being FinSequence st len q = len p & ( for i being Nat st i in dom p holds
for t being c-Term of A,V st t = p . i holds
q . i = t @ f ) holds
((Sym (o,( the Sorts of A \/ V))) -tree p) @ f = (Den (o,A)) . q
let p be ArgumentSeq of o,A,V; ::_thesis: for q being FinSequence st len q = len p & ( for i being Nat st i in dom p holds
for t being c-Term of A,V st t = p . i holds
q . i = t @ f ) holds
((Sym (o,( the Sorts of A \/ V))) -tree p) @ f = (Den (o,A)) . q
let q be FinSequence; ::_thesis: ( len q = len p & ( for i being Nat st i in dom p holds
for t being c-Term of A,V st t = p . i holds
q . i = t @ f ) implies ((Sym (o,( the Sorts of A \/ V))) -tree p) @ f = (Den (o,A)) . q )
assume that
A1: len q = len p and
A2: for i being Nat st i in dom p holds
for t being c-Term of A,V st t = p . i holds
q . i = t @ f ; ::_thesis: ((Sym (o,( the Sorts of A \/ V))) -tree p) @ f = (Den (o,A)) . q
consider vt being finite DecoratedTree such that
A3: vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f by Th36;
consider r being DTree-yielding FinSequence such that
A4: len r = len p and
A5: vt = ((Den (o,A)) . (roots r)) -tree r and
A6: for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = r . i & vt is_an_evaluation_of t,f ) by A3, Th35;
now__::_thesis:_(_dom_p_=_dom_p_&_dom_q_=_dom_p_&_dom_r_=_dom_p_&_(_for_i_being_Element_of_NAT_st_i_in_dom_r_holds_
ex_T_being_DecoratedTree_st_
(_T_=_r_._i_&_q_._i_=_T_._{}_)_)_)
thus A7: ( dom p = dom p & dom q = dom p & dom r = dom p ) by A1, A4, FINSEQ_3:29; ::_thesis: for i being Element of NAT st i in dom r holds
ex T being DecoratedTree st
( T = r . i & q . i = T . {} )
let i be Element of NAT ; ::_thesis: ( i in dom r implies ex T being DecoratedTree st
( T = r . i & q . i = T . {} ) )
assume A8: i in dom r ; ::_thesis: ex T being DecoratedTree st
( T = r . i & q . i = T . {} )
then reconsider t = p . i as c-Term of A,V by A7, Th22;
consider vt being finite DecoratedTree such that
A9: vt = r . i and
A10: vt is_an_evaluation_of t,f by A6, A7, A8;
reconsider T = vt as DecoratedTree ;
take T = T; ::_thesis: ( T = r . i & q . i = T . {} )
thus T = r . i by A9; ::_thesis: q . i = T . {}
thus q . i = t @ f by A2, A7, A8
.= T . {} by A10, Th39 ; ::_thesis: verum
end;
then q = roots r by TREES_3:def_18;
hence ((Sym (o,( the Sorts of A \/ V))) -tree p) @ f = (((Den (o,A)) . q) -tree r) . {} by A3, A5, Th39
.= (Den (o,A)) . q by TREES_4:def_4 ;
::_thesis: verum
end;