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 :
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 :
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem
theorem Th34:
theorem Th35:
theorem
begin
:: deftheorem defines a_Type ABCMIZ_1:def 4 :
:: deftheorem defines an_Adj ABCMIZ_1:def 5 :
:: deftheorem defines a_Term ABCMIZ_1:def 6 :
:: deftheorem defines * ABCMIZ_1:def 7 :
:: deftheorem defines non_op ABCMIZ_1:def 8 :
:: deftheorem Def9 defines constructor ABCMIZ_1:def 9 :
:: deftheorem Def10 defines MinConstrSign ABCMIZ_1:def 10 :
:: deftheorem Def11 defines constructor ABCMIZ_1:def 11 :
theorem
:: deftheorem Def12 defines initialized ABCMIZ_1:def 12 :
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 :
:: deftheorem defines an_Adj ABCMIZ_1:def 14 :
:: deftheorem defines a_Term ABCMIZ_1:def 15 :
:: deftheorem defines non_op ABCMIZ_1:def 16 :
:: deftheorem defines ast ABCMIZ_1:def 17 :
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 :
:: deftheorem defines Attrs ABCMIZ_1:def 19 :
:: deftheorem defines Funcs ABCMIZ_1:def 20 :
:: deftheorem defines Constructors ABCMIZ_1:def 21 :
theorem
:: deftheorem defines loci_of ABCMIZ_1:def 22 :
:: deftheorem defines index_of ABCMIZ_1:def 23 :
theorem
:: deftheorem Def24 defines MaxConstrSign ABCMIZ_1:def 24 :
begin
:: deftheorem Def25 defines MSVars ABCMIZ_1:def 25 :
:: deftheorem defines ground ABCMIZ_1:def 26 :
:: deftheorem Def27 defines compound ABCMIZ_1:def 27 :
:: deftheorem Def28 defines expression ABCMIZ_1:def 28 :
theorem Th41:
:: deftheorem defines term ABCMIZ_1:def 29 :
theorem Th42:
:: deftheorem Def30 defines term ABCMIZ_1:def 30 :
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 :
theorem Th46:
theorem
:: deftheorem defines OperSymbol ABCMIZ_1:def 32 :
theorem Th48:
begin
:: deftheorem defines QuasiTerms ABCMIZ_1:def 33 :
theorem
:: deftheorem defines -term ABCMIZ_1:def 34 :
theorem Th50:
theorem Th51:
:: deftheorem Def35 defines -trm ABCMIZ_1:def 35 :
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem
theorem Th57:
theorem Th58:
begin
:: deftheorem Def36 defines Non ABCMIZ_1:def 36 :
:: deftheorem Def37 defines positive ABCMIZ_1:def 37 :
theorem Th59:
:: deftheorem Def38 defines negative ABCMIZ_1:def 38 :
theorem Th60:
theorem Th61:
theorem Th62:
:: deftheorem Def39 defines regular ABCMIZ_1:def 39 :
:: deftheorem defines QuasiAdjs ABCMIZ_1:def 40 :
theorem Th63:
theorem
theorem Th65:
theorem Th66:
theorem Th67:
theorem
theorem
begin
:: deftheorem Def41 defines pure ABCMIZ_1:def 41 :
theorem Th70:
theorem Th71:
:: deftheorem defines QuasiTypes ABCMIZ_1:def 42 :
:: deftheorem Def43 defines quasi-type ABCMIZ_1:def 43 :
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75:
theorem
theorem
theorem
theorem
theorem Th80:
theorem
:: deftheorem defines ast ABCMIZ_1:def 44 :
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 :
:: deftheorem defines variables_in ABCMIZ_1:def 46 :
:: deftheorem defines vars ABCMIZ_1:def 47 :
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 :
:: deftheorem defines vars ABCMIZ_1:def 49 :
theorem
theorem Th102:
theorem
theorem Th104:
theorem
theorem Th106:
theorem Th107:
:: deftheorem Def50 defines ground ABCMIZ_1:def 50 :
theorem Th108:
begin
:: deftheorem defines VarPoset ABCMIZ_1:def 51 :
theorem Th109:
theorem Th110:
theorem Th111:
theorem Th112:
theorem
:: deftheorem defines vars-function ABCMIZ_1:def 52 :
:: deftheorem defines smooth ABCMIZ_1:def 53 :
begin
:: deftheorem Def54 defines with_an_operation_for_each_sort ABCMIZ_1:def 54 :
:: deftheorem Def55 defines with_missing_variables ABCMIZ_1:def 55 :
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 :
theorem Th129:
theorem Th130:
:: deftheorem defines substitution ABCMIZ_1:def 57 :
begin
:: deftheorem Def58 defines irrelevant ABCMIZ_1:def 58 :
:: deftheorem defines idval ABCMIZ_1:def 59 :
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 :
:: deftheorem defines at ABCMIZ_1:def 61 :
:: deftheorem Def62 defines at ABCMIZ_1:def 62 :
:: deftheorem defines at ABCMIZ_1:def 63 :
theorem
theorem
theorem
theorem
theorem
theorem Th137:
theorem
theorem Th139:
theorem
theorem
theorem
theorem
:: deftheorem defines at ABCMIZ_1:def 64 :
theorem Th144:
theorem Th145:
theorem
:: deftheorem defines at ABCMIZ_1:def 65 :
theorem
theorem
:: deftheorem Def66 defines at ABCMIZ_1:def 66 :
theorem Th149:
theorem Th150:
theorem