begin
theorem Th1:
theorem
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
definition
let A be
set ;
func varcl A -> set means :
Def1:
(
A c= it & ( for
x,
y being
set st
[x,y] in it holds
x c= it ) & ( for
B being
set st
A c= B & ( for
x,
y being
set st
[x,y] in B holds
x c= B ) holds
it c= B ) );
uniqueness
for b1, b2 being set st A c= b1 & ( for x, y being set st [x,y] in b1 holds
x c= b1 ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b1 c= B ) & A c= b2 & ( for x, y being set st [x,y] in b2 holds
x c= b2 ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b2 c= B ) holds
b1 = b2
existence
ex b1 being set st
( A c= b1 & ( for x, y being set st [x,y] in b1 holds
x c= b1 ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b1 c= B ) )
projectivity
for b1, b2 being set st b2 c= b1 & ( for x, y being set st [x,y] in b1 holds
x c= b1 ) & ( for B being set st b2 c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b1 c= B ) holds
( b1 c= b1 & ( for x, y being set st [x,y] in b1 holds
x c= b1 ) & ( for B being set st b1 c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b1 c= B ) )
;
end;
:: deftheorem Def1 defines varcl ABCMIZ_1:def 1 :
for A being set
for b2 being set holds
( b2 = varcl A iff ( A c= b2 & ( for x, y being set st [x,y] in b2 holds
x c= b2 ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b2 c= B ) ) );
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
deffunc H1( set , set ) -> set = { [(varcl A),j] where A is Subset of $2, j is Element of NAT : A is finite } ;
definition
func Vars -> set means :
Def2:
ex
V being
ManySortedSet of
NAT st
(
it = Union V &
V . 0 = { [{},i] where i is Element of NAT : verum } & ( for
n being
Nat holds
V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) );
existence
ex b1 being set ex V being ManySortedSet of NAT st
( b1 = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) )
uniqueness
for b1, b2 being set st ex V being ManySortedSet of NAT st
( b1 = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) ) & ex V being ManySortedSet of NAT st
( b2 = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines Vars ABCMIZ_1:def 2 :
for b1 being set holds
( b1 = Vars iff ex V being ManySortedSet of NAT st
( b1 = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) ) );
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem
theorem Th26:
theorem Th27:
theorem
begin
:: deftheorem Def3 defines QuasiLoci ABCMIZ_1:def 3 :
for b1 being FinSequenceSet of Vars holds
( b1 = QuasiLoci iff for p being FinSequence of Vars holds
( p in b1 iff ( p is one-to-one & ( for i being Nat st i in dom p holds
(p . i) `1 c= rng (p dom i) ) ) ) );
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem
theorem Th34:
theorem Th35:
theorem
begin
:: deftheorem defines a_Type ABCMIZ_1:def 4 :
a_Type = 0 ;
:: deftheorem defines an_Adj ABCMIZ_1:def 5 :
an_Adj = 1;
:: deftheorem defines a_Term ABCMIZ_1:def 6 :
a_Term = 2;
:: deftheorem defines * ABCMIZ_1:def 7 :
* = 0 ;
:: deftheorem defines non_op ABCMIZ_1:def 8 :
non_op = 1;
:: deftheorem Def9 defines constructor ABCMIZ_1:def 9 :
for C being Signature holds
( C is constructor iff ( the carrier of C = {a_Type,an_Adj,a_Term} & {*,non_op} c= the carrier' of C & the Arity of C . * = <*an_Adj,a_Type*> & the Arity of C . non_op = <*an_Adj*> & the ResultSort of C . * = a_Type & the ResultSort of C . non_op = an_Adj & ( for o being Element of the carrier' of C st o <> * & o <> non_op holds
the Arity of C . o in {a_Term} * ) ) );
:: deftheorem Def10 defines MinConstrSign ABCMIZ_1:def 10 :
for b1 being strict Signature holds
( b1 = MinConstrSign iff ( b1 is constructor & the carrier' of b1 = {*,non_op} ) );
:: deftheorem Def11 defines constructor ABCMIZ_1:def 11 :
for C being ConstructorSignature
for o being OperSymbol of C holds
( o is constructor iff ( o <> * & o <> non_op ) );
theorem
:: deftheorem Def12 defines initialized ABCMIZ_1:def 12 :
for C being non empty non void Signature holds
( C is initialized iff ex m, a being OperSymbol of C st
( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} ) );
definition
let C be
ConstructorSignature;
A1:
the
carrier of
C = {a_Type,an_Adj,a_Term}
by Def9;
func a_Type C -> SortSymbol of
C equals
a_Type ;
coherence
a_Type is SortSymbol of C
by A1, ENUMSET1:def 1;
func an_Adj C -> SortSymbol of
C equals
an_Adj ;
coherence
an_Adj is SortSymbol of C
by A1, ENUMSET1:def 1;
func a_Term C -> SortSymbol of
C equals
a_Term ;
coherence
a_Term is SortSymbol of C
by A1, ENUMSET1:def 1;
A2:
{*,non_op} c= the
carrier' of
C
by Def9;
A3:
* in {*,non_op}
by TARSKI:def 2;
A4:
non_op in {*,non_op}
by TARSKI:def 2;
func non_op C -> OperSymbol of
C equals
non_op ;
coherence
non_op is OperSymbol of C
by A2, A4;
func ast C -> OperSymbol of
C equals
* ;
coherence
* is OperSymbol of C
by A2, A3;
end;
:: deftheorem defines a_Type ABCMIZ_1:def 13 :
for C being ConstructorSignature holds a_Type C = a_Type ;
:: deftheorem defines an_Adj ABCMIZ_1:def 14 :
for C being ConstructorSignature holds an_Adj C = an_Adj ;
:: deftheorem defines a_Term ABCMIZ_1:def 15 :
for C being ConstructorSignature holds a_Term C = a_Term ;
:: deftheorem defines non_op ABCMIZ_1:def 16 :
for C being ConstructorSignature holds non_op C = non_op ;
:: deftheorem defines ast ABCMIZ_1:def 17 :
for C being ConstructorSignature holds ast C = * ;
theorem
definition
func Modes -> set equals
[:{a_Type},[:QuasiLoci,NAT:]:];
correctness
coherence
[:{a_Type},[:QuasiLoci,NAT:]:] is set ;
;
func Attrs -> set equals
[:{an_Adj},[:QuasiLoci,NAT:]:];
correctness
coherence
[:{an_Adj},[:QuasiLoci,NAT:]:] is set ;
;
func Funcs -> set equals
[:{a_Term},[:QuasiLoci,NAT:]:];
correctness
coherence
[:{a_Term},[:QuasiLoci,NAT:]:] is set ;
;
end;
:: deftheorem defines Modes ABCMIZ_1:def 18 :
Modes = [:{a_Type},[:QuasiLoci,NAT:]:];
:: deftheorem defines Attrs ABCMIZ_1:def 19 :
Attrs = [:{an_Adj},[:QuasiLoci,NAT:]:];
:: deftheorem defines Funcs ABCMIZ_1:def 20 :
Funcs = [:{a_Term},[:QuasiLoci,NAT:]:];
:: deftheorem defines Constructors ABCMIZ_1:def 21 :
Constructors = (Modes \/ Attrs) \/ Funcs;
theorem
:: deftheorem defines loci_of ABCMIZ_1:def 22 :
for c being Element of Constructors holds loci_of c = (c `2) `1 ;
:: deftheorem defines index_of ABCMIZ_1:def 23 :
for c being Element of Constructors holds index_of c = (c `2) `2 ;
theorem
:: deftheorem Def24 defines MaxConstrSign ABCMIZ_1:def 24 :
for b1 being strict ConstructorSignature holds
( b1 = MaxConstrSign iff ( the carrier' of b1 = {*,non_op} \/ Constructors & ( for o being OperSymbol of b1 st o is constructor holds
( the ResultSort of b1 . o = o `1 & card ( the Arity of b1 . o) = card ((o `2) `1) ) ) ) );
begin
:: deftheorem Def25 defines MSVars ABCMIZ_1:def 25 :
for C being ConstructorSignature
for b2 being ManySortedSet of the carrier of C holds
( b2 = MSVars C iff ( b2 . a_Type = {} & b2 . an_Adj = {} & b2 . a_Term = Vars ) );
:: deftheorem defines ground ABCMIZ_1:def 26 :
for S being non void Signature
for X being V6() ManySortedSet of the carrier of S
for t being Element of (Free (S,X)) holds
( t is ground iff Union (S variables_in t) = {} );
:: deftheorem Def27 defines compound ABCMIZ_1:def 27 :
for S being non void Signature
for X being V6() ManySortedSet of the carrier of S
for t being Element of (Free (S,X)) holds
( t is compound iff t . {} in [: the carrier' of S,{ the carrier of S}:] );
:: deftheorem Def28 defines expression ABCMIZ_1:def 28 :
for C being initialized ConstructorSignature
for s being SortSymbol of C
for b3 being expression of C holds
( b3 is expression of C,s iff b3 in the Sorts of (Free (C,(MSVars C))) . s );
theorem Th41:
:: deftheorem defines term ABCMIZ_1:def 29 :
for C being initialized ConstructorSignature
for c being constructor OperSymbol of C st len (the_arity_of c) = 0 holds
c term = [c, the carrier of C] -tree {};
theorem Th42:
:: deftheorem Def30 defines term ABCMIZ_1:def 30 :
for C being initialized ConstructorSignature
for o being OperSymbol of C st len (the_arity_of o) = 1 holds
for e being expression of C st ex s being SortSymbol of C st
( s = (the_arity_of o) . 1 & e is expression of C,s ) holds
o term e = [o, the carrier of C] -tree <*e*>;
theorem Th43:
theorem Th44:
theorem Th45:
definition
let C be
initialized ConstructorSignature;
let o be
OperSymbol of
C;
assume A1:
len (the_arity_of o) = 2
;
let e1,
e2 be
expression of
C;
assume A2:
ex
s1,
s2 being
SortSymbol of
C st
(
s1 = (the_arity_of o) . 1 &
s2 = (the_arity_of o) . 2 &
e1 is
expression of
C,
s1 &
e2 is
expression of
C,
s2 )
;
func o term (
e1,
e2)
-> expression of
C equals :
Def31:
[o, the carrier of C] -tree <*e1,e2*>;
coherence
[o, the carrier of C] -tree <*e1,e2*> is expression of C
by A1, A2, Th45;
end;
:: deftheorem Def31 defines term ABCMIZ_1:def 31 :
for C being initialized ConstructorSignature
for o being OperSymbol of C st len (the_arity_of o) = 2 holds
for e1, e2 being expression of C st ex s1, s2 being SortSymbol of C st
( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & e1 is expression of C,s1 & e2 is expression of C,s2 ) holds
o term (e1,e2) = [o, the carrier of C] -tree <*e1,e2*>;
theorem Th46:
theorem
:: deftheorem defines OperSymbol ABCMIZ_1:def 32 :
for S being non void Signature
for s being SortSymbol of S st ex o being OperSymbol of S st the_result_sort_of o = s holds
for b3 being OperSymbol of S holds
( b3 is OperSymbol of s iff the_result_sort_of b3 = s );
theorem Th48:
begin
:: deftheorem defines QuasiTerms ABCMIZ_1:def 33 :
for C being initialized ConstructorSignature holds QuasiTerms C = the Sorts of (Free (C,(MSVars C))) . (a_Term C);
theorem
:: deftheorem defines -term ABCMIZ_1:def 34 :
for x being variable
for C being initialized ConstructorSignature holds x -term C = root-tree [x,a_Term];
theorem Th50:
theorem Th51:
:: deftheorem Def35 defines -trm ABCMIZ_1:def 35 :
for C being initialized ConstructorSignature
for c being constructor OperSymbol of C
for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds
c -trm p = [c, the carrier of C] -tree p;
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem
theorem Th57:
theorem Th58:
begin
:: deftheorem Def36 defines Non ABCMIZ_1:def 36 :
for C being initialized ConstructorSignature
for a being expression of C, an_Adj C holds
( ( ex a9 being expression of C, an_Adj C st a = (non_op C) term a9 implies Non a = a | <*0*> ) & ( ( for a9 being expression of C, an_Adj C holds not a = (non_op C) term a9 ) implies Non a = (non_op C) term a ) );
:: deftheorem Def37 defines positive ABCMIZ_1:def 37 :
for C being initialized ConstructorSignature
for a being expression of C, an_Adj C holds
( a is positive iff for a9 being expression of C, an_Adj C holds not a = (non_op C) term a9 );
theorem Th59:
:: deftheorem Def38 defines negative ABCMIZ_1:def 38 :
for C being initialized ConstructorSignature
for a being expression of C, an_Adj C holds
( a is negative iff ex a9 being expression of C, an_Adj C st
( a9 is positive & a = (non_op C) term a9 ) );
theorem Th60:
theorem Th61:
theorem Th62:
:: deftheorem Def39 defines regular ABCMIZ_1:def 39 :
for C being initialized ConstructorSignature
for a being expression of C, an_Adj C holds
( a is regular iff ( a is positive or a is negative ) );
:: deftheorem defines QuasiAdjs ABCMIZ_1:def 40 :
for C being initialized ConstructorSignature holds QuasiAdjs C = { a where a is expression of C, an_Adj C : a is regular } ;
theorem Th63:
theorem
theorem Th65:
theorem Th66:
theorem Th67:
theorem
theorem
begin
:: deftheorem Def41 defines pure ABCMIZ_1:def 41 :
for C being initialized ConstructorSignature
for q being expression of C, a_Type C holds
( q is pure iff for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds not q = (ast C) term (a,t) );
theorem Th70:
theorem Th71:
:: deftheorem defines QuasiTypes ABCMIZ_1:def 42 :
for C being initialized ConstructorSignature holds QuasiTypes C = { [A,t] where t is expression of C, a_Type C, A is finite Subset of (QuasiAdjs C) : t is pure } ;
:: deftheorem Def43 defines quasi-type ABCMIZ_1:def 43 :
for C being initialized ConstructorSignature
for b2 being set holds
( b2 is quasi-type of C iff b2 in QuasiTypes C );
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75:
theorem
theorem
theorem
theorem
theorem Th80:
theorem
:: deftheorem defines ast ABCMIZ_1:def 44 :
for C being initialized ConstructorSignature
for T being quasi-type of C
for a being quasi-adjective of C holds a ast T = [({a} \/ (adjs T)),(the_base_of T)];
theorem
theorem
theorem
begin
definition
let S be non
void Signature;
let X be
V6()
ManySortedSet of the
carrier of
S;
let s be
SortSymbol of
S;
func (
X,
s)
variables_in -> Function of
(Union the Sorts of (Free (S,X))),
(bool (X . s)) means :
Def45:
for
t being
Element of
(Free (S,X)) holds
it . t = (S variables_in t) . s;
uniqueness
for b1, b2 being Function of (Union the Sorts of (Free (S,X))),(bool (X . s)) st ( for t being Element of (Free (S,X)) holds b1 . t = (S variables_in t) . s ) & ( for t being Element of (Free (S,X)) holds b2 . t = (S variables_in t) . s ) holds
b1 = b2
existence
ex b1 being Function of (Union the Sorts of (Free (S,X))),(bool (X . s)) st
for t being Element of (Free (S,X)) holds b1 . t = (S variables_in t) . s
end;
:: deftheorem Def45 defines variables_in ABCMIZ_1:def 45 :
for S being non void Signature
for X being V6() ManySortedSet of the carrier of S
for s being SortSymbol of S
for b4 being Function of (Union the Sorts of (Free (S,X))),(bool (X . s)) holds
( b4 = (X,s) variables_in iff for t being Element of (Free (S,X)) holds b4 . t = (S variables_in t) . s );
:: deftheorem defines variables_in ABCMIZ_1:def 46 :
for C being initialized ConstructorSignature
for e being expression of C holds variables_in e = (C variables_in e) . (a_Term C);
:: deftheorem defines vars ABCMIZ_1:def 47 :
for C being initialized ConstructorSignature
for e being expression of C holds vars e = varcl (variables_in e);
theorem
theorem
theorem
theorem Th88:
theorem Th89:
theorem
theorem
theorem
theorem Th93:
theorem Th94:
theorem
theorem Th96:
theorem Th97:
theorem
theorem Th99:
theorem
:: deftheorem defines variables_in ABCMIZ_1:def 48 :
for C being initialized ConstructorSignature
for T being quasi-type of C holds variables_in T = (union ((((MSVars C),(a_Term C)) variables_in) .: (adjs T))) \/ (variables_in (the_base_of T));
:: deftheorem defines vars ABCMIZ_1:def 49 :
for C being initialized ConstructorSignature
for T being quasi-type of C holds vars T = varcl (variables_in T);
theorem
theorem Th102:
theorem
theorem Th104:
theorem
theorem Th106:
theorem Th107:
:: deftheorem Def50 defines ground ABCMIZ_1:def 50 :
for C being initialized ConstructorSignature
for T being quasi-type of C holds
( T is ground iff variables_in T = {} );
theorem Th108:
begin
:: deftheorem defines VarPoset ABCMIZ_1:def 51 :
VarPoset = (InclPoset { (varcl A) where A is finite Subset of Vars : verum } ) opp ;
theorem Th109:
theorem Th110:
theorem Th111:
theorem Th112:
theorem
:: deftheorem defines vars-function ABCMIZ_1:def 52 :
for C being initialized ConstructorSignature
for b2 being Function of (QuasiTypes C), the carrier of VarPoset holds
( b2 = vars-function C iff for T being quasi-type of C holds b2 . T = vars T );
:: deftheorem defines smooth ABCMIZ_1:def 53 :
for L being non empty Poset holds
( L is smooth iff ex C being initialized ConstructorSignature ex f being Function of L,VarPoset st
( the carrier of L c= QuasiTypes C & f = (vars-function C) | the carrier of L & ( for x, y being Element of L holds f preserves_sup_of {x,y} ) ) );
begin
:: deftheorem Def54 defines with_an_operation_for_each_sort ABCMIZ_1:def 54 :
for S being ManySortedSign holds
( S is with_an_operation_for_each_sort iff the carrier of S c= rng the ResultSort of S );
:: deftheorem Def55 defines with_missing_variables ABCMIZ_1:def 55 :
for S being ManySortedSign
for X being ManySortedSet of the carrier of S holds
( X is with_missing_variables iff X " {{}} c= rng the ResultSort of S );
theorem Th114:
theorem Th115:
theorem Th116:
theorem Th117:
theorem Th118:
theorem
theorem Th120:
theorem
theorem Th122:
theorem Th123:
theorem Th124:
theorem
theorem
theorem Th127:
theorem Th128:
:: deftheorem Def56 defines term-transformation ABCMIZ_1:def 56 :
for S being non void Signature
for X being ManySortedSet of the carrier of S
for b3 being UnOp of (Union the Sorts of (Free (S,X))) holds
( b3 is term-transformation of S,X iff for s being SortSymbol of S holds b3 .: ( the Sorts of (Free (S,X)) . s) c= the Sorts of (Free (S,X)) . s );
theorem Th129:
theorem Th130:
:: deftheorem defines substitution ABCMIZ_1:def 57 :
for S being non void Signature
for X being ManySortedSet of the carrier of S
for t being term-transformation of S,X holds
( t is substitution iff for o being OperSymbol of S
for p, q being FinSequence of (Free (S,X)) st [o, the carrier of S] -tree p in Union the Sorts of (Free (S,X)) & q = t * p holds
t . ([o, the carrier of S] -tree p) = [o, the carrier of S] -tree q );
begin
:: deftheorem Def58 defines irrelevant ABCMIZ_1:def 58 :
for C being initialized ConstructorSignature
for f being valuation of C holds
( f is irrelevant iff for x being variable st x in dom f holds
ex y being variable st f . x = y -term C );
:: deftheorem defines idval ABCMIZ_1:def 59 :
for C being initialized ConstructorSignature
for X being Subset of Vars holds C idval X = { [x,(x -term C)] where x is variable : x in X } ;
theorem Th131:
definition
let C be
initialized ConstructorSignature;
let f be
valuation of
C;
func f # -> term-transformation of
C,
MSVars C means :
Def60:
( ( for
x being
variable holds
( (
x in dom f implies
it . (x -term C) = f . x ) & ( not
x in dom f implies
it . (x -term C) = x -term C ) ) ) & ( for
c being
constructor OperSymbol of
C for
p,
q being
FinSequence of
QuasiTerms C st
len p = len (the_arity_of c) &
q = it * p holds
it . (c -trm p) = c -trm q ) & ( for
a being
expression of
C,
an_Adj C holds
it . ((non_op C) term a) = (non_op C) term (it . a) ) & ( for
a being
expression of
C,
an_Adj C for
t being
expression of
C,
a_Type C holds
it . ((ast C) term (a,t)) = (ast C) term (
(it . a),
(it . t)) ) );
existence
ex b1 being term-transformation of C, MSVars C st
( ( for x being variable holds
( ( x in dom f implies b1 . (x -term C) = f . x ) & ( not x in dom f implies b1 . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b1 * p holds
b1 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b1 . ((non_op C) term a) = (non_op C) term (b1 . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds b1 . ((ast C) term (a,t)) = (ast C) term ((b1 . a),(b1 . t)) ) )
correctness
uniqueness
for b1, b2 being term-transformation of C, MSVars C st ( for x being variable holds
( ( x in dom f implies b1 . (x -term C) = f . x ) & ( not x in dom f implies b1 . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b1 * p holds
b1 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b1 . ((non_op C) term a) = (non_op C) term (b1 . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds b1 . ((ast C) term (a,t)) = (ast C) term ((b1 . a),(b1 . t)) ) & ( for x being variable holds
( ( x in dom f implies b2 . (x -term C) = f . x ) & ( not x in dom f implies b2 . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b2 * p holds
b2 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b2 . ((non_op C) term a) = (non_op C) term (b2 . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds b2 . ((ast C) term (a,t)) = (ast C) term ((b2 . a),(b2 . t)) ) holds
b1 = b2;
end;
:: deftheorem Def60 defines # ABCMIZ_1:def 60 :
for C being initialized ConstructorSignature
for f being valuation of C
for b3 being term-transformation of C, MSVars C holds
( b3 = f # iff ( ( for x being variable holds
( ( x in dom f implies b3 . (x -term C) = f . x ) & ( not x in dom f implies b3 . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b3 * p holds
b3 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b3 . ((non_op C) term a) = (non_op C) term (b3 . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds b3 . ((ast C) term (a,t)) = (ast C) term ((b3 . a),(b3 . t)) ) ) );
:: deftheorem defines at ABCMIZ_1:def 61 :
for C being initialized ConstructorSignature
for f being valuation of C
for e being expression of C holds e at f = (f #) . e;
:: deftheorem Def62 defines at ABCMIZ_1:def 62 :
for C being initialized ConstructorSignature
for f being valuation of C
for p being FinSequence st rng p c= Union the Sorts of (Free (C,(MSVars C))) holds
p at f = (f #) * p;
:: deftheorem defines at ABCMIZ_1:def 63 :
for C being initialized ConstructorSignature
for f being valuation of C
for p being FinSequence of QuasiTerms C holds p at f = (f #) * p;
theorem
theorem
theorem
theorem
theorem
theorem Th137:
theorem
theorem Th139:
theorem
theorem
theorem
theorem
:: deftheorem defines at ABCMIZ_1:def 64 :
for C being initialized ConstructorSignature
for f being valuation of C
for A being Subset of (QuasiAdjs C) holds A at f = { (a at f) where a is quasi-adjective of C : a in A } ;
theorem Th144:
theorem Th145:
theorem
:: deftheorem defines at ABCMIZ_1:def 65 :
for C being initialized ConstructorSignature
for f being valuation of C
for T being quasi-type of C holds T at f = ((adjs T) at f) ast ((the_base_of T) at f);
theorem
theorem
:: deftheorem Def66 defines at ABCMIZ_1:def 66 :
for C being initialized ConstructorSignature
for f, g, b4 being valuation of C holds
( b4 = f at g iff ( dom b4 = (dom f) \/ (dom g) & ( for x being variable st x in dom b4 holds
b4 . x = ((x -term C) at f) at g ) ) );
theorem Th149:
theorem Th150:
theorem