:: Towards the construction of a model of Mizar concepts
:: by Grzegorz Bancerek
::
:: Received April 21, 2008
:: Copyright (c) 2008-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, SUBSET_1, FUNCT_1, TARSKI, CARD_3, RELAT_1,
XBOOLE_0, STRUCT_0, CATALG_1, PBOOLE, MSATERM, FACIRC_1, MSUALG_1,
ZFMISC_1, ZF_MODEL, FUNCOP_1, CARD_1, FINSEQ_1, TREES_3, TREES_4,
MARGREL1, MSAFREE, CLASSES1, SETFAM_1, FINSET_1, QC_LANG3, ARYTM_3,
XXREAL_0, ORDINAL1, MCART_1, FINSEQ_2, ORDINAL4, PARTFUN1, ABCMIZ_0,
FUNCT_2, FUNCT_4, ZF_LANG1, CAT_3, TREES_2, MSUALG_2, MEMBER_1, AOFA_000,
CARD_5, ORDERS_2, YELLOW_1, ARYTM_0, LATTICE3, EQREL_1, LATTICES,
YELLOW_0, ORDINAL2, WAYBEL_0, ASYMPT_0, LANG1, TDGROUP, DTCONSTR,
BINOP_1, MATRIX_7, FUNCT_7, ABCMIZ_1, SETLIM_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, DOMAIN_1,
SETFAM_1, RELAT_1, FUNCT_1, RELSET_1, BINOP_1, PARTFUN1, FACIRC_1,
ENUMSET1, FUNCT_2, PARTIT_2, FUNCT_4, FUNCOP_1, XXREAL_0, ORDINAL1,
XCMPLX_0, NAT_1, MCART_1, FINSET_1, CARD_1, NUMBERS, CARD_3, FINSEQ_1,
FINSEQ_2, TREES_2, TREES_3, TREES_4, FUNCT_7, PBOOLE, MATRIX_7, XXREAL_2,
STRUCT_0, LANG1, CLASSES1, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0,
YELLOW_1, YELLOW_7, DTCONSTR, MSUALG_1, MSUALG_2, MSAFREE, EQUATION,
MSATERM, CATALG_1, MSAFREE3, AOFA_000, PRE_POLY;
constructors DOMAIN_1, MATRIX_7, MSAFREE1, FUNCT_7, EQUATION, YELLOW_1,
CATALG_1, LATTICE3, WAYBEL_0, FACIRC_1, CLASSES1, MSAFREE3, XXREAL_2,
RELSET_1, PRE_POLY, PARTIT_2, XTUPLE_0, XFAMILY;
registrations XBOOLE_0, SUBSET_1, XREAL_0, ORDINAL1, RELSET_1, FUNCT_1,
FINSET_1, STRUCT_0, PBOOLE, MSUALG_1, MSUALG_2, FINSEQ_1, CARD_1,
MSAFREE, FUNCOP_1, TREES_3, MSAFREE1, PARTFUN1, MSATERM, ORDERS_2,
TREES_2, DTCONSTR, WAYBEL_0, YELLOW_1, LATTICE3, MEMBERED, RELAT_1,
INDEX_1, INSTALG1, MSAFREE3, FACIRC_1, XXREAL_2, CLASSES1, FINSEQ_2,
PARTIT_2, XTUPLE_0, NAT_1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
begin :: Variables
reserve i for Nat,
j for Element of NAT,
X,Y,x,y,z for set;
theorem :: ABCMIZ_1:1
for f being Function holds f.x c= Union f;
theorem :: ABCMIZ_1:2
for f being Function st Union f = {} holds f.x = {};
theorem :: ABCMIZ_1:3
for f being Function for x,y being object st f = [x,y] holds x = y;
theorem :: ABCMIZ_1:4
(id X).:Y c= Y;
theorem :: ABCMIZ_1:5
for S being non void Signature
for X being non-empty ManySortedSet of the carrier of S
for t being Term of S, X
holds t is non pair;
registration
let S be non void Signature;
let X be non empty-yielding ManySortedSet of the carrier of S;
cluster -> non pair for Element of Free(S,X);
end;
theorem :: ABCMIZ_1:6
for x,y,z being set st x in {z}* & y in {z}* & card x = card y holds x = y;
definition
let S be non void Signature;
let A be MSAlgebra over S;
mode Subset of A is Subset of Union the Sorts of A;
mode FinSequence of A is FinSequence of Union the Sorts of A;
end;
registration
let S be non void Signature;
let X be non empty-yielding ManySortedSet of S;
cluster -> DTree-yielding for FinSequence of Free(S,X);
end;
theorem :: ABCMIZ_1:7
for S being non void Signature
for X being non empty-yielding ManySortedSet of the carrier of S
for t being Element of Free(S,X) holds
(ex s being SortSymbol of S, v being set st
t = root-tree [v,s] & v in X.s) or
ex o being OperSymbol of S,
p being FinSequence of Free(S,X) st
t = [o,the carrier of S]-tree p & len p = len the_arity_of o &
p is DTree-yielding &
p is ArgumentSeq of Sym(o, X(\/)((the carrier of S)-->{0}));
definition
let A be set;
func varcl A -> set means
:: ABCMIZ_1:def 1
A c= it & (for x,y st [x,y] in it holds x c= it) &
for B being set st A c= B & for x,y st [x,y] in B holds x c= B
holds it c= B;
projectivity;
end;
theorem :: ABCMIZ_1:8
varcl {} = {};
theorem :: ABCMIZ_1:9
for A,B being set st A c= B holds varcl A c= varcl B;
theorem :: ABCMIZ_1:10
for A being set holds
varcl union A = union the set of all varcl a where a is Element of A;
scheme :: ABCMIZ_1:sch 1
Sch14{A() -> set, F(set) -> set, P[set]}:
varcl union {F(z) where z is Element of A(): P[z]}
= union {varcl F(z) where z is Element of A(): P[z]};
theorem :: ABCMIZ_1:11
varcl (X \/ Y) = (varcl X) \/ (varcl Y);
theorem :: ABCMIZ_1:12
for A being non empty set st for a being Element of A holds varcl a = a
holds varcl meet A = meet A;
theorem :: ABCMIZ_1:13
varcl ((varcl X) /\ (varcl Y)) = (varcl X) /\ (varcl Y);
registration
let A be empty set;
cluster varcl A -> empty;
end;
definition
func Vars -> set means
:: ABCMIZ_1:def 2
ex V being ManySortedSet of NAT st it = Union V &
V.0 = the set of all [{}, i] where i is Element of NAT &
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};
end;
theorem :: ABCMIZ_1:14
for V being ManySortedSet of NAT st
V.0 = the set of all [{}, i] where i is Element of NAT &
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}
for i,j being Element of NAT st i <= j holds V.i c= V.j;
theorem :: ABCMIZ_1:15
for V being ManySortedSet of NAT st
V.0 = the set of all [{}, i] where i is Element of NAT &
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}
for A being finite Subset of Vars
ex i being Element of NAT st A c= V.i;
theorem :: ABCMIZ_1:16
the set of all [{}, i] where i is Element of NAT c= Vars;
theorem :: ABCMIZ_1:17
for A being finite Subset of Vars, i being Nat holds [varcl A, i] in Vars;
theorem :: ABCMIZ_1:18
Vars = {[varcl A, j] where A is Subset of Vars, j is Element of NAT:
A is finite};
theorem :: ABCMIZ_1:19
varcl Vars = Vars;
theorem :: ABCMIZ_1:20
for X st the_rank_of X is finite holds X is finite;
theorem :: ABCMIZ_1:21
the_rank_of varcl X = the_rank_of X;
theorem :: ABCMIZ_1:22
for X being finite Subset of Rank omega holds X in Rank omega;
theorem :: ABCMIZ_1:23
Vars c= Rank omega;
theorem :: ABCMIZ_1:24
for A being finite Subset of Vars holds varcl A is finite Subset of Vars;
registration
cluster Vars -> non empty;
end;
definition
mode variable is Element of Vars;
end;
registration
let x be variable;
cluster x`1 -> finite for set;
end;
notation
let x be variable;
synonym vars x for x`1;
end;
definition
let x be variable;
redefine func vars x -> Subset of Vars;
end;
theorem :: ABCMIZ_1:25
[{}, i] in Vars;
theorem :: ABCMIZ_1:26
for A being Subset of Vars holds
varcl {[varcl A, j]} = (varcl A) \/ {[varcl A, j]};
theorem :: ABCMIZ_1:27
for x being variable holds varcl {x} = (vars x) \/ {x};
theorem :: ABCMIZ_1:28
for x being variable holds [(vars x) \/ {x}, i] in Vars;
begin :: Quasi loci
notation
let R be Relation, A be set;
synonym R dom A for R|A;
end;
definition
func QuasiLoci -> FinSequenceSet of Vars means
:: ABCMIZ_1:def 3
for p being FinSequence of Vars holds p in it iff p is one-to-one &
for i st i in dom p holds (p.i)`1 c= rng (p dom i);
end;
theorem :: ABCMIZ_1:29
<*>Vars in QuasiLoci;
registration
cluster QuasiLoci -> non empty;
end;
definition
mode quasi-loci is Element of QuasiLoci;
end;
registration
cluster -> one-to-one for quasi-loci;
end;
theorem :: ABCMIZ_1:30
for l being one-to-one FinSequence of Vars holds l is quasi-loci iff
for i being Nat, x being variable st i in dom l & x = l.i
for y being variable st y in vars x
ex j being Nat st j in dom l & j < i & y = l.j;
theorem :: ABCMIZ_1:31
for l being quasi-loci, x being variable holds
l^<*x*> is quasi-loci iff not x in rng l & vars x c= rng l;
theorem :: ABCMIZ_1:32
for p,q being FinSequence st p^q is quasi-loci
holds p is quasi-loci & q is FinSequence of Vars;
theorem :: ABCMIZ_1:33
for l being quasi-loci holds varcl rng l = rng l;
theorem :: ABCMIZ_1:34
for x being variable holds <*x*> is quasi-loci iff vars x = {};
theorem :: ABCMIZ_1:35
for x,y being variable holds
<*x,y*> is quasi-loci iff vars x = {} & x <> y & vars y c= {x};
theorem :: ABCMIZ_1:36
for x,y,z being variable holds
<*x,y,z*> is quasi-loci iff vars x = {} & x <> y & vars y c= {x} &
x <> z & y <> z & vars z c= {x,y};
definition
let l be quasi-loci;
redefine func l" -> PartFunc of Vars, NAT;
end;
begin :: Mizar Constructor Signature
definition
func a_Type -> set equals
:: ABCMIZ_1:def 4
0;
func an_Adj -> set equals
:: ABCMIZ_1:def 5
1;
func a_Term -> set equals
:: ABCMIZ_1:def 6
2;
func * -> set equals
:: ABCMIZ_1:def 7
0;
func non_op -> set equals
:: ABCMIZ_1:def 8
1;
:: func an_ExReg equals 3; coherence;
:: func a_CondReg equals 4; coherence;
:: func a_FuncReg equals 5; coherence;
end;
definition
let C be Signature;
attr C is constructor means
:: ABCMIZ_1:def 9
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}*;
end;
registration
cluster constructor -> non empty non void for Signature;
end;
definition
func MinConstrSign -> strict Signature means
:: ABCMIZ_1:def 10
it is constructor & the carrier' of it = {*, non_op};
end;
registration
cluster MinConstrSign -> constructor;
end;
registration
cluster constructor strict for Signature;
end;
definition
mode ConstructorSignature is constructor Signature;
end;
:: theorem ::?
:: for C being ConstructorSignature holds the carrier of C = 3
:: by CONSTRSIGN,YELLOW11:1;
definition
let C be ConstructorSignature;
let o be OperSymbol of C;
attr o is constructor means
:: ABCMIZ_1:def 11
o <> * & o <> non_op;
end;
theorem :: ABCMIZ_1:37
for S being ConstructorSignature
for o being OperSymbol of S st o is constructor
holds the_arity_of o = (len the_arity_of o) |-> a_Term;
definition
let C be non empty non void Signature;
attr C is initialized means
:: ABCMIZ_1:def 12
ex m, a being OperSymbol of C st
the_result_sort_of m = a_Type & the_arity_of m = {} & :: set
the_result_sort_of a = an_Adj & the_arity_of a = {}; :: empty
end;
definition
let C be ConstructorSignature;
func a_Type C -> SortSymbol of C equals
:: ABCMIZ_1:def 13
a_Type;
func an_Adj C -> SortSymbol of C equals
:: ABCMIZ_1:def 14
an_Adj;
func a_Term C -> SortSymbol of C equals
:: ABCMIZ_1:def 15
a_Term;
func non_op C -> OperSymbol of C equals
:: ABCMIZ_1:def 16
non_op;
func ast C -> OperSymbol of C equals
:: ABCMIZ_1:def 17
*;
end;
theorem :: ABCMIZ_1:38
for C being ConstructorSignature holds the_arity_of non_op C = <*an_Adj C*> &
the_result_sort_of non_op C = an_Adj C &
the_arity_of ast C = <*an_Adj C, a_Type C*> &
the_result_sort_of ast C = a_Type C;
definition
func Modes -> set equals
:: ABCMIZ_1:def 18
[:{a_Type},[:QuasiLoci,NAT:]:];
func Attrs -> set equals
:: ABCMIZ_1:def 19
[:{an_Adj},[:QuasiLoci,NAT:]:];
func Funcs -> set equals
:: ABCMIZ_1:def 20
[:{a_Term},[:QuasiLoci,NAT:]:];
end;
registration
cluster Modes -> non empty;
cluster Attrs -> non empty;
cluster Funcs -> non empty;
end;
definition
func Constructors -> non empty set equals
:: ABCMIZ_1:def 21
Modes \/ Attrs \/ Funcs;
end;
theorem :: ABCMIZ_1:39
{*, non_op} misses Constructors;
definition
let x be Element of [:QuasiLoci, NAT:];
redefine func x`1 -> quasi-loci;
redefine func x`2 -> Element of NAT;
end;
notation
let c be Element of Constructors;
synonym kind_of c for c`1;
end;
definition
let c be Element of Constructors;
redefine func kind_of c -> Element of {a_Type, an_Adj, a_Term};
redefine func c`2 -> Element of [:QuasiLoci, NAT:];
end;
definition
let c be Element of Constructors;
func loci_of c -> quasi-loci equals
:: ABCMIZ_1:def 22
c`2`1;
func index_of c -> Nat equals
:: ABCMIZ_1:def 23
c`2`2;
end;
theorem :: ABCMIZ_1:40
for c being Element of Constructors holds
(kind_of c = a_Type iff c in Modes) &
(kind_of c = an_Adj iff c in Attrs) &
(kind_of c = a_Term iff c in Funcs);
definition
func MaxConstrSign -> strict ConstructorSignature means
:: ABCMIZ_1:def 24
the carrier' of it = {*, non_op} \/ Constructors &
for o being OperSymbol of it st o is constructor
holds (the ResultSort of it).o = o`1 &
card ((the Arity of it).o) = card o`2`1;
end;
registration
cluster MinConstrSign -> non initialized;
cluster MaxConstrSign -> initialized;
end;
registration
cluster initialized strict for ConstructorSignature;
end;
registration
let C be initialized ConstructorSignature;
cluster constructor for OperSymbol of C;
end;
begin :: Mizar Expressions
definition
let C be ConstructorSignature;
func MSVars C -> ManySortedSet of the carrier of C means
:: ABCMIZ_1:def 25
it.a_Type = {} & it.an_Adj = {} & it.a_Term = Vars;
end;
:: theorem
:: for C being ConstructorSignature
:: for x being variable holds
:: (C variables_in root-tree [x, a_Term]).a_Term C = {x} by MSAFREE3:11;
registration
let C be ConstructorSignature;
cluster MSVars C -> non empty-yielding;
end;
registration
let C be initialized ConstructorSignature;
cluster Free(C, MSVars C) -> non-empty;
end;
definition
let S be non void Signature;
let X be non empty-yielding ManySortedSet of the carrier of S;
let t be Element of Free(S,X);
attr t is ground means
:: ABCMIZ_1:def 26
Union (S variables_in t) = {};
attr t is compound means
:: ABCMIZ_1:def 27
t.{} in [:the carrier' of S, {the carrier of S}:];
end;
reserve C for initialized ConstructorSignature,
s for SortSymbol of C,
o for OperSymbol of C,
c for constructor OperSymbol of C;
definition
let C;
mode expression of C is Element of Free(C, MSVars C);
end;
definition
let C, s;
mode expression of C, s -> expression of C means
:: ABCMIZ_1:def 28
it in (the Sorts of Free(C, MSVars C)).s;
end;
theorem :: ABCMIZ_1:41
z is expression of C, s iff z in (the Sorts of Free(C, MSVars C)).s;
definition
let C;
let c such that
len the_arity_of c = 0;
func c term -> expression of C equals
:: ABCMIZ_1:def 29
[c, the carrier of C]-tree {};
end;
theorem :: ABCMIZ_1:42
for o st len the_arity_of o = 1 for a being expression of C st
ex s st s = (the_arity_of o).1 & a is expression of C, s
holds
[o, the carrier of C]-tree <*a*> is expression of C, the_result_sort_of o;
definition
let C,o such that
len the_arity_of o = 1;
let e be expression of C such that
ex s being SortSymbol of C st
s = (the_arity_of o).1 & e is expression of C, s;
func o term e -> expression of C equals
:: ABCMIZ_1:def 30
[o, the carrier of C]-tree<*e*>;
end;
reserve a,b for expression of C, an_Adj C;
theorem :: ABCMIZ_1:43
(non_op C)term a is expression of C, an_Adj C &
(non_op C)term a = [non_op, the carrier of C]-tree <*a*>;
theorem :: ABCMIZ_1:44
(non_op C)term a = (non_op C)term b implies a = b;
registration
let C,a;
cluster (non_op C)term a -> compound;
end;
registration
let C;
cluster compound for expression of C;
end;
theorem :: ABCMIZ_1:45
for o st len the_arity_of o = 2 for a,b 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 &
a is expression of C, s1 & b is expression of C, s2
holds
[o, the carrier of C]-tree <*a,b*> is expression of C, the_result_sort_of o;
definition
let C,o such that
len the_arity_of o = 2;
let e1,e2 be expression of C such that
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
:: ABCMIZ_1:def 31
[o, the carrier of C]-tree<*e1,e2*>;
end;
reserve t, t1,t2 for expression of C, a_Type C;
theorem :: ABCMIZ_1:46
(ast C)term(a,t) is expression of C, a_Type C &
(ast C)term(a,t) = [ *, the carrier of C]-tree <*a,t*>;
theorem :: ABCMIZ_1:47
(ast C)term(a,t1) = (ast C)term(b,t2) implies a = b & t1 = t2;
registration
let C,a,t;
cluster (ast C)term(a,t) -> compound;
end;
definition
let S be non void Signature;
let s be SortSymbol of S such that
ex o being OperSymbol of S st the_result_sort_of o = s;
mode OperSymbol of s -> OperSymbol of S means
:: ABCMIZ_1:def 32
the_result_sort_of it = s;
end;
definition
let C be ConstructorSignature;
redefine func non_op C -> OperSymbol of an_Adj C;
redefine func ast C -> OperSymbol of a_Type C;
end;
theorem :: ABCMIZ_1:48
for s1,s2 being SortSymbol of C st s1 <> s2 for t1 being expression of C, s1
for t2 being expression of C, s2
holds t1 <> t2;
begin :: Quasi-terms
definition
let C;
func QuasiTerms C -> Subset of Free(C, MSVars C) equals
:: ABCMIZ_1:def 33
(the Sorts of Free(C, MSVars C)).a_Term C;
end;
registration
let C;
cluster QuasiTerms C -> non empty constituted-DTrees;
end;
definition
let C;
mode quasi-term of C is expression of C, a_Term C;
end;
theorem :: ABCMIZ_1:49
z is quasi-term of C iff z in QuasiTerms C;
definition
let x be variable;
let C;
func x-term C -> quasi-term of C equals
:: ABCMIZ_1:def 34
root-tree [x, a_Term];
end;
theorem :: ABCMIZ_1:50
for x1,x2 being variable for C1,C2 being initialized ConstructorSignature
st x1-term C1 = x2-term C2
holds x1 = x2;
registration
let x be variable;
let C;
cluster x-term C -> non compound;
end;
theorem :: ABCMIZ_1:51
for p being DTree-yielding FinSequence holds
[c, the carrier of C]-tree p is expression of C
iff len p = len the_arity_of c & p in (QuasiTerms C)*;
reserve p for FinSequence of QuasiTerms C;
definition
let C,c;
let p such that
len p = len the_arity_of c;
func c-trm p -> compound expression of C equals
:: ABCMIZ_1:def 35
[c, the carrier of C]-tree p;
end;
theorem :: ABCMIZ_1:52
len p = len the_arity_of c implies
c-trm p is expression of C, the_result_sort_of c;
theorem :: ABCMIZ_1:53
for e being expression of C holds (ex x being variable st e = x-term C) or
(ex c being constructor OperSymbol of C st
ex p being FinSequence of QuasiTerms C st
len p = len the_arity_of c & e = c-trm p) or
(ex a being expression of C, an_Adj C st e = (non_op C)term a) or
ex a being expression of C, an_Adj C st
ex t being expression of C, a_Type C st e = (ast C)term(a,t);
theorem :: ABCMIZ_1:54
len p = len the_arity_of c implies c-trm p <> (non_op C)term a;
theorem :: ABCMIZ_1:55
len p = len the_arity_of c implies c-trm p <> (ast C)term(a,t);
theorem :: ABCMIZ_1:56
(non_op C)term a <> (ast C)term(b,t);
reserve e for expression of C;
theorem :: ABCMIZ_1:57
e.{} = [non_op, the carrier of C] implies ex a st e = (non_op C)term a;
theorem :: ABCMIZ_1:58
e.{} = [ *, the carrier of C] implies ex a, t st e = (ast C)term(a,t);
begin :: Quasi-adjectives
reserve a,a9 for expression of C, an_Adj C;
definition
let C,a;
func Non a -> expression of C, an_Adj C equals
:: ABCMIZ_1:def 36
a|<* 0 *> if ex a9 st a = (non_op C)term a9
otherwise (non_op C)term a;
end;
definition
let C,a;
attr a is positive means
:: ABCMIZ_1:def 37
not ex a9 st a = (non_op C)term a9;
end;
registration
let C;
cluster positive for expression of C, an_Adj C;
end;
theorem :: ABCMIZ_1:59
for a being positive expression of C, an_Adj C holds Non a = (non_op C)term a
;
definition
let C,a;
attr a is negative means
:: ABCMIZ_1:def 38
ex a9 st a9 is positive & a = (non_op C)term a9;
end;
registration
let C;
let a be positive expression of C, an_Adj C;
cluster Non a -> negative non positive;
end;
registration
let C;
cluster negative non positive for expression of C, an_Adj C;
end;
theorem :: ABCMIZ_1:60
for a being non positive expression of C, an_Adj C
ex a9 being expression of C, an_Adj C
st a = (non_op C)term a9 & Non a = a9;
theorem :: ABCMIZ_1:61
for a being negative expression of C, an_Adj C
ex a9 being positive expression of C, an_Adj C
st a = (non_op C)term a9 & Non a = a9;
theorem :: ABCMIZ_1:62
for a being non positive expression of C, an_Adj C
holds (non_op C)term (Non a) = a;
registration
let C;
let a be negative expression of C, an_Adj C;
cluster Non a -> positive;
end;
definition
let C,a;
attr a is regular means
:: ABCMIZ_1:def 39
a is positive or a is negative;
end;
registration
let C;
cluster positive -> regular non negative for expression of C, an_Adj C;
cluster negative -> regular non positive for expression of C, an_Adj C;
end;
registration
let C;
cluster regular for expression of C, an_Adj C;
end;
definition
let C;
func QuasiAdjs C -> Subset of Free(C, MSVars C) equals
:: ABCMIZ_1:def 40
{a: a is regular};
end;
registration
let C;
cluster QuasiAdjs C -> non empty constituted-DTrees;
end;
definition
let C;
mode quasi-adjective of C is regular expression of C, an_Adj C;
end;
theorem :: ABCMIZ_1:63
z is quasi-adjective of C iff z in QuasiAdjs C;
theorem :: ABCMIZ_1:64
z is quasi-adjective of C iff z is positive expression of C, an_Adj C or
z is negative expression of C, an_Adj C;
registration
let C;
cluster non positive -> negative for quasi-adjective of C;
cluster non negative -> positive for quasi-adjective of C;
end;
registration
let C;
cluster positive for quasi-adjective of C;
cluster negative for quasi-adjective of C;
end;
theorem :: ABCMIZ_1:65
for a being positive quasi-adjective of C
ex v being constructor OperSymbol of C st the_result_sort_of v = an_Adj C &
ex p st len p = len the_arity_of v & a = v-trm p;
theorem :: ABCMIZ_1:66
for v being constructor OperSymbol of C
st the_result_sort_of v = an_Adj C & len p = len the_arity_of v
holds v-trm p is positive quasi-adjective of C;
registration
let C;
let a be quasi-adjective of C;
cluster Non a -> regular;
end;
theorem :: ABCMIZ_1:67
for a being quasi-adjective of C holds Non Non a = a;
theorem :: ABCMIZ_1:68
for a1,a2 being quasi-adjective of C st Non a1 = Non a2 holds a1 = a2;
theorem :: ABCMIZ_1:69
for a being quasi-adjective of C holds Non a <> a;
begin :: Quasi-types
definition
let C;
let q be expression of C, a_Type C;
attr q is pure means
:: ABCMIZ_1:def 41
not ex a, t st q = (ast C)term(a,t);
end;
theorem :: ABCMIZ_1:70
for m being OperSymbol of C
st the_result_sort_of m = a_Type & the_arity_of m = {}
ex t st t = root-tree [m, the carrier of C] & t is pure;
theorem :: ABCMIZ_1:71
for v being OperSymbol of C
st the_result_sort_of v = an_Adj & the_arity_of v = {}
ex a st a = root-tree [v, the carrier of C] & a is positive;
registration
let C;
cluster pure for expression of C, a_Type C;
end;
reserve q for pure expression of C, a_Type C,
A for finite Subset of QuasiAdjs C;
definition
let C;
func QuasiTypes C -> set equals
:: ABCMIZ_1:def 42
{[A,t]: t is pure};
end;
registration
let C;
cluster QuasiTypes C -> non empty;
end;
definition
let C;
mode quasi-type of C -> set means
:: ABCMIZ_1:def 43
it in QuasiTypes C;
end;
theorem :: ABCMIZ_1:72
z is quasi-type of C iff ex A,q st z = [A,q];
theorem :: ABCMIZ_1:73
[x,y] is quasi-type of C iff
x is finite Subset of QuasiAdjs C & y is pure expression of C, a_Type C;
reserve T for quasi-type of C;
registration
let C;
cluster -> pair for quasi-type of C;
end;
theorem :: ABCMIZ_1:74
ex m being constructor OperSymbol of C st the_result_sort_of m = a_Type C &
ex p st len p = len the_arity_of m & q = m-trm p;
theorem :: ABCMIZ_1:75
for m being constructor OperSymbol of C
st the_result_sort_of m = a_Type C & len p = len the_arity_of m
holds m-trm p is pure expression of C, a_Type C;
theorem :: ABCMIZ_1:76
QuasiTerms C misses QuasiAdjs C & QuasiTerms C misses QuasiTypes C &
QuasiTypes C misses QuasiAdjs C;
theorem :: ABCMIZ_1:77
for e being set holds
(e is quasi-term of C implies e is not quasi-adjective of C) &
(e is quasi-term of C implies e is not quasi-type of C) &
(e is quasi-type of C implies e is not quasi-adjective of C);
notation
let C,A,q;
synonym A ast q for [A,q];
end;
definition
let C,A,q;
redefine func A ast q -> quasi-type of C;
end;
registration
let C,T;
cluster T`1 -> finite for set;
end;
notation
let C,T;
synonym adjs T for T`1;
synonym the_base_of T for T`2;
end;
definition
let C,T;
redefine func adjs T -> Subset of QuasiAdjs C;
redefine func the_base_of T -> pure expression of C, a_Type C;
end;
theorem :: ABCMIZ_1:78
adjs (A ast q) = A & the_base_of (A ast q) = q;
theorem :: ABCMIZ_1:79
for A1,A2 being finite Subset of QuasiAdjs C
for q1,q2 being pure expression of C, a_Type C
st A1 ast q1 = A2 ast q2
holds A1 = A2 & q1 = q2;
theorem :: ABCMIZ_1:80
T = (adjs T) ast the_base_of T;
theorem :: ABCMIZ_1:81
for T1,T2 being quasi-type of C
st adjs T1 = adjs T2 & the_base_of T1 = the_base_of T2
holds T1 = T2;
definition
let C,T;
let a be quasi-adjective of C;
func a ast T -> quasi-type of C equals
:: ABCMIZ_1:def 44
[{a} \/ adjs T, the_base_of T];
end;
theorem :: ABCMIZ_1:82
for a being quasi-adjective of C
holds adjs (a ast T) = {a} \/ adjs T & the_base_of (a ast T) = the_base_of T;
theorem :: ABCMIZ_1:83
for a being quasi-adjective of C holds a ast (a ast T) = a ast T;
theorem :: ABCMIZ_1:84
for a,b being quasi-adjective of C holds a ast (b ast T) = b ast (a ast T);
begin :: Variables in quasi-types
registration
let S be non void Signature;
let s be SortSymbol of S;
let X be non-empty ManySortedSet of the carrier of S;
let t be Term of S,X;
cluster (variables_in t).s -> finite;
end;
registration
let S be non void Signature;
let s be SortSymbol of S;
let X be non empty-yielding ManySortedSet of the carrier of S;
let t be Element of Free(S,X);
cluster (S variables_in t).s -> finite;
end;
definition
let S be non void Signature;
let X be non empty-yielding 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
:: ABCMIZ_1:def 45
for t being Element of Free(S,X) holds it.t = (S variables_in t).s;
end;
definition
let C be initialized ConstructorSignature;
let e be expression of C;
func variables_in e -> Subset of Vars equals
:: ABCMIZ_1:def 46
(C variables_in e).a_Term C;
end;
registration
let C,e;
cluster variables_in e -> finite;
end;
definition
let C,e;
func vars e -> finite Subset of Vars equals
:: ABCMIZ_1:def 47
varcl variables_in e;
end;
theorem :: ABCMIZ_1:85
varcl vars e = vars e;
theorem :: ABCMIZ_1:86
for x being variable holds variables_in (x-term C) = {x};
theorem :: ABCMIZ_1:87
for x being variable holds vars (x-term C) = {x} \/ vars x;
theorem :: ABCMIZ_1:88
for p being DTree-yielding FinSequence st e = [c, the carrier of C]-tree p
holds variables_in e =
union {variables_in t where t is quasi-term of C: t in rng p};
theorem :: ABCMIZ_1:89
for p being DTree-yielding FinSequence st e = [c, the carrier of C]-tree p
holds vars e = union {vars t where t is quasi-term of C: t in rng p};
theorem :: ABCMIZ_1:90
len p = len the_arity_of c implies variables_in (c-trm p) =
union {variables_in t where t is quasi-term of C: t in rng p};
theorem :: ABCMIZ_1:91
len p = len the_arity_of c implies
vars (c-trm p) = union {vars t where t is quasi-term of C: t in rng p};
theorem :: ABCMIZ_1:92
for S being ManySortedSign, o being set holds
S variables_in ([o, the carrier of S]-tree {}) = EmptyMS the carrier of S;
theorem :: ABCMIZ_1:93
for S being ManySortedSign, o being set, t being DecoratedTree holds
S variables_in ([o, the carrier of S]-tree <*t*>) = S variables_in t;
theorem :: ABCMIZ_1:94
variables_in ((non_op C)term a) = variables_in a;
theorem :: ABCMIZ_1:95
vars ((non_op C)term a) = vars a;
theorem :: ABCMIZ_1:96
for S being ManySortedSign, o being set, t1,t2 being DecoratedTree holds
S variables_in ([o, the carrier of S]-tree <*t1,t2*>)
= (S variables_in t1) (\/) (S variables_in t2);
theorem :: ABCMIZ_1:97
variables_in ((ast C)term(a,t)) = (variables_in a)\/(variables_in t);
theorem :: ABCMIZ_1:98
vars ((ast C)term(a,t)) = (vars a)\/(vars t);
theorem :: ABCMIZ_1:99
variables_in Non a = variables_in a;
theorem :: ABCMIZ_1:100
vars Non a = vars a;
definition
let C;
let T be quasi-type of C;
func variables_in T -> Subset of Vars equals
:: ABCMIZ_1:def 48
(union (((MSVars C, a_Term C) variables_in).:adjs T)) \/
variables_in the_base_of T;
end;
registration
let C;
let T be quasi-type of C;
cluster variables_in T -> finite;
end;
definition
let C;
let T be quasi-type of C;
func vars T -> finite Subset of Vars equals
:: ABCMIZ_1:def 49
varcl variables_in T;
end;
theorem :: ABCMIZ_1:101
for T being quasi-type of C holds varcl vars T = vars T;
theorem :: ABCMIZ_1:102
for T being quasi-type of C for a being quasi-adjective of C holds
variables_in (a ast T) = (variables_in a) \/ (variables_in T);
theorem :: ABCMIZ_1:103
for T being quasi-type of C for a being quasi-adjective of C holds
vars (a ast T) = (vars a) \/ (vars T);
theorem :: ABCMIZ_1:104
variables_in (A ast q) =
(union {variables_in a where a is quasi-adjective of C: a in A}) \/
(variables_in q);
theorem :: ABCMIZ_1:105
vars (A ast q) =
(union {vars a where a is quasi-adjective of C: a in A}) \/ (vars q);
theorem :: ABCMIZ_1:106
variables_in (({}QuasiAdjs C) ast q) = variables_in q;
theorem :: ABCMIZ_1:107
e is ground iff variables_in e = {};
definition
let C;
let T be quasi-type of C;
attr T is ground means
:: ABCMIZ_1:def 50
variables_in T = {};
end;
registration
let C;
cluster ground pure for expression of C, a_Type C;
cluster ground for quasi-adjective of C;
end;
theorem :: ABCMIZ_1:108
for t being ground pure expression of C, a_Type C
holds ({} QuasiAdjs C) ast t is ground;
registration
let C;
let t be ground pure expression of C, a_Type C;
cluster ({} QuasiAdjs C) ast t -> ground for quasi-type of C;
end;
registration
let C;
cluster ground for quasi-type of C;
end;
registration
let C;
let T be ground quasi-type of C;
let a be ground quasi-adjective of C;
cluster a ast T -> ground;
end;
begin :: Smooth Type Widening
:: Type widening is smooth iff
:: vars-function is sup-semilattice homomorphism from widening sup-semilattice
:: into VarPoset
definition
func VarPoset -> strict non empty Poset equals
:: ABCMIZ_1:def 51
(InclPoset the set of all varcl A where A is finite Subset of Vars)opp;
end;
theorem :: ABCMIZ_1:109
for x, y being Element of VarPoset holds x <= y iff y c= x;
:: registration
:: let V1,V2 be Element of VarPoset;
:: identify V1 <= V2 with V2 c= V1;
:: compatibility by Th22;
:: end;
theorem :: ABCMIZ_1:110
for x holds
x is Element of VarPoset iff x is finite Subset of Vars & varcl x = x;
registration
cluster VarPoset -> with_infima with_suprema;
end;
theorem :: ABCMIZ_1:111
for V1, V2 being Element of VarPoset holds
V1 "\/" V2 = V1 /\ V2 & V1 "/\" V2 = V1 \/ V2;
registration
let V1,V2 be Element of VarPoset;
identify V1 "\/" V2 with V1 /\ V2;
identify V1 "/\" V2 with V1 \/ V2;
end;
theorem :: ABCMIZ_1:112
for X being non empty Subset of VarPoset holds
ex_sup_of X, VarPoset & sup X = meet X;
registration
cluster VarPoset -> up-complete;
end;
theorem :: ABCMIZ_1:113
Top VarPoset = {};
definition
let C;
func vars-function C -> Function of QuasiTypes C, the carrier of VarPoset
means
:: ABCMIZ_1:def 52
for T being quasi-type of C holds it.T = vars T;
end;
definition
let L be non empty Poset;
attr L is smooth means
:: ABCMIZ_1:def 53
ex C being initialized ConstructorSignature,
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};
end;
registration
let C be initialized ConstructorSignature;
let T be ground quasi-type of C;
cluster RelStr(#{T}, id {T}#) -> smooth;
end;
begin :: Structural induction
scheme :: ABCMIZ_1:sch 2
StructInd
{C() -> initialized ConstructorSignature, P[set], t() -> expression of C()}:
P[t()]
provided
for x being variable holds P[x-term C()] and
for c being constructor OperSymbol of C()
for p being FinSequence of QuasiTerms C()
st len p = len the_arity_of c &
for t being quasi-term of C() st t in rng p holds P[t]
holds P[c-trm p] and
for a being expression of C(), an_Adj C() st P[a]
holds P[(non_op C())term a] and
for a being expression of C(), an_Adj C() st P[a]
for t being expression of C(), a_Type C() st P[t]
holds P[(ast C())term(a,t)];
definition
let S be ManySortedSign;
attr S is with_an_operation_for_each_sort means
:: ABCMIZ_1:def 54
the carrier of S c= rng the ResultSort of S;
let X be ManySortedSet of the carrier of S;
attr X is with_missing_variables means
:: ABCMIZ_1:def 55
X"{{}} c= rng the ResultSort of S;
end;
theorem :: ABCMIZ_1:114
for S being non void Signature for X being ManySortedSet of the carrier of S
holds X is with_missing_variables iff
for s being SortSymbol of S st X.s = {}
ex o being OperSymbol of S st the_result_sort_of o = s;
registration
cluster MaxConstrSign -> with_an_operation_for_each_sort;
let C be ConstructorSignature;
cluster MSVars C -> with_missing_variables;
end;
registration
let S be ManySortedSign;
cluster non-empty -> with_missing_variables
for ManySortedSet of the carrier of S;
end;
registration
let S be ManySortedSign;
cluster with_missing_variables for ManySortedSet of the carrier of S;
end;
registration
cluster initialized with_an_operation_for_each_sort
strict for ConstructorSignature;
end;
registration
let C be with_an_operation_for_each_sort ManySortedSign;
cluster -> with_missing_variables for ManySortedSet of the carrier of C;
end;
definition
let G be non empty DTConstrStr;
redefine func Terminals G -> Subset of G;
redefine func NonTerminals G -> Subset of G;
end;
theorem :: ABCMIZ_1:115
for D1,D2 being non empty DTConstrStr st the Rules of D1 c= the Rules of D2
holds NonTerminals D1 c= NonTerminals D2 &
(the carrier of D1) /\ Terminals D2 c= Terminals D1 &
(Terminals D1 c= Terminals D2 implies the carrier of D1 c= the carrier of D2)
;
theorem :: ABCMIZ_1:116
for D1,D2 being non empty DTConstrStr st Terminals D1 c= Terminals D2 &
the Rules of D1 c= the Rules of D2
holds TS D1 c= TS D2;
theorem :: ABCMIZ_1:117
for S being ManySortedSign
for X,Y being ManySortedSet of the carrier of S st X c= Y
holds X is with_missing_variables implies Y is with_missing_variables;
theorem :: ABCMIZ_1:118
for S being set for X,Y being ManySortedSet of S st X c= Y
holds Union coprod X c= Union coprod Y;
theorem :: ABCMIZ_1:119
for S being non void Signature
for X,Y being ManySortedSet of the carrier of S st X c= Y
holds the carrier of DTConMSA X c= the carrier of DTConMSA Y;
theorem :: ABCMIZ_1:120
for S being non void Signature for X being ManySortedSet of the carrier of S
st X is with_missing_variables
holds
NonTerminals DTConMSA X = [:the carrier' of S,{the carrier of S}:] &
Terminals DTConMSA X = Union coprod X;
theorem :: ABCMIZ_1:121
for S being non void Signature
for X,Y being ManySortedSet of the carrier of S
st X c= Y & X is with_missing_variables
holds
Terminals DTConMSA X c= Terminals DTConMSA Y &
the Rules of DTConMSA X c= the Rules of DTConMSA Y &
TS DTConMSA X c= TS DTConMSA Y;
theorem :: ABCMIZ_1:122
for t being set holds t in Terminals DTConMSA MSVars C iff
ex x being variable st t = [x,a_Term C];
theorem :: ABCMIZ_1:123
for t being set holds t in NonTerminals DTConMSA MSVars C iff
t = [ast C, the carrier of C] or
t = [non_op C, the carrier of C] or
ex c being constructor OperSymbol of C st t = [c, the carrier of C];
theorem :: ABCMIZ_1:124
for S being non void Signature
for X being with_missing_variables ManySortedSet of the carrier of S
for t being set st t in Union the Sorts of Free(S,X)
holds t is Term of S, X (\/) ((the carrier of S)-->{0});
theorem :: ABCMIZ_1:125
for S being non void Signature
for X being with_missing_variables ManySortedSet of the carrier of S
for t being Term of S, X (\/) ((the carrier of S)-->{0})
st t in Union the Sorts of Free(S,X)
holds t in (the Sorts of Free(S,X)).the_sort_of t;
theorem :: ABCMIZ_1:126
for G being non empty DTConstrStr for s being Element of G
for p being FinSequence st s ==> p
holds p is FinSequence of the carrier of G;
theorem :: ABCMIZ_1:127
for S being non void Signature
for X,Y being ManySortedSet of the carrier of S
for g1 being Symbol of DTConMSA X
for g2 being Symbol of DTConMSA Y
for p1 being FinSequence of the carrier of DTConMSA X
for p2 being FinSequence of the carrier of DTConMSA Y
st g1 = g2 & p1 = p2 & g1 ==> p1
holds g2 ==> p2;
theorem :: ABCMIZ_1:128
for S being non void Signature
for X being with_missing_variables ManySortedSet of the carrier of S holds
Union the Sorts of Free(S, X) = TS DTConMSA X;
definition
let S be non void Signature;
let X be ManySortedSet of the carrier of S;
mode term-transformation of S,X -> UnOp of Union the Sorts of Free(S,X) means
:: ABCMIZ_1:def 56
for s being SortSymbol of S holds
it.:((the Sorts of Free(S,X)).s) c= (the Sorts of Free(S,X)).s;
end;
theorem :: ABCMIZ_1:129
for S being non void Signature
for X being non empty ManySortedSet of the carrier of S
for f being UnOp of Union the Sorts of Free(S,X)
holds f is term-transformation of S,X iff
for s being SortSymbol of S
for a being set st a in (the Sorts of Free(S,X)).s
holds f.a in (the Sorts of Free(S,X)).s;
theorem :: ABCMIZ_1:130
for S being non void Signature
for X being non empty ManySortedSet of the carrier of S
for f being term-transformation of S,X
for s being SortSymbol of S
for p being FinSequence of (the Sorts of Free(S,X)).s
holds f*p is FinSequence of (the Sorts of Free(S,X)).s &
card (f*p) = len p;
definition
let S be non void Signature;
let X be ManySortedSet of the carrier of S;
let t be term-transformation of S,X;
attr t is substitution means
:: ABCMIZ_1:def 57
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;
end;
scheme :: ABCMIZ_1:sch 3
StructDef
{C() -> initialized ConstructorSignature,
V,N(set) -> (expression of C()),
F,A(set,set) -> (expression of C())}:
ex f being term-transformation of C(), MSVars C() st
(for x being variable holds f.(x-term C()) = V(x)) &
(for c being constructor OperSymbol of C()
for p,q being FinSequence of QuasiTerms C()
st len p = len the_arity_of c & q = f*p
holds f.(c-trm p) = F(c, q)) &
(for a being expression of C(), an_Adj C()
holds f.((non_op C())term a) = N(f.a)) &
for a being expression of C(), an_Adj C()
for t being expression of C(), a_Type C()
holds f.((ast C())term(a,t)) = A(f.a, f.t)
provided
for x being variable holds V(x) is quasi-term of C() and
for c being constructor OperSymbol of C()
for p being FinSequence of QuasiTerms C()
st len p = len the_arity_of c
holds F(c, p) is expression of C(), the_result_sort_of c and
for a being expression of C(), an_Adj C()
holds N(a) is expression of C(), an_Adj C() and
for a being expression of C(), an_Adj C()
for t being expression of C(), a_Type C()
holds A(a,t) is expression of C(), a_Type C();
begin :: Substitution
definition
let A be set;
let x,y be set;
let a,b be Element of A;
redefine func IFIN(x,y,a,b) -> Element of A;
end;
definition
let C be initialized ConstructorSignature;
mode valuation of C is PartFunc of Vars, QuasiTerms C;
end;
definition
let C be initialized ConstructorSignature;
let f be valuation of C;
attr f is irrelevant means
:: ABCMIZ_1:def 58
for x being variable st x in dom f
ex y being variable st f.x = y-term C;
end;
notation
let C be initialized ConstructorSignature;
let f be valuation of C;
antonym f is relevant for f is irrelevant;
end;
registration
let C be initialized ConstructorSignature;
cluster empty -> irrelevant for valuation of C;
end;
registration
let C be initialized ConstructorSignature;
cluster empty for valuation of C;
end;
definition
let C be initialized ConstructorSignature;
let X be Subset of Vars;
func C idval X -> valuation of C equals
:: ABCMIZ_1:def 59
{[x, x-term C] where x is variable: x in X};
end;
theorem :: ABCMIZ_1:131
for X being Subset of Vars holds dom (C idval X) = X &
for x being variable st x in X holds (C idval X).x = x-term C;
registration
let C be initialized ConstructorSignature;
let X be Subset of Vars;
cluster C idval X -> irrelevant one-to-one;
end;
registration
let C be initialized ConstructorSignature;
let X be empty Subset of Vars;
cluster C idval X -> empty;
end;
definition
let C;
let f be valuation of C;
func f# -> term-transformation of C, MSVars C means
:: ABCMIZ_1:def 60
(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);
end;
registration
let C;
let f be valuation of C;
cluster f# -> substitution;
end;
reserve f for valuation of C;
definition
let C,f,e;
func e at f -> expression of C equals
:: ABCMIZ_1:def 61
f#.e;
end;
definition
let C,f;
let p be FinSequence such that
rng p c= Union the Sorts of Free(C, MSVars C);
func p at f -> FinSequence equals
:: ABCMIZ_1:def 62
f# * p;
end;
definition
let C,f;
let p be FinSequence of QuasiTerms C;
redefine func p at f -> FinSequence of QuasiTerms C equals
:: ABCMIZ_1:def 63
f# * p;
end;
reserve x for variable;
theorem :: ABCMIZ_1:132
not x in dom f implies (x-term C)at f = x-term C;
theorem :: ABCMIZ_1:133
x in dom f implies (x-term C)at f = f.x;
theorem :: ABCMIZ_1:134
len p = len the_arity_of c implies (c-trm p)at f = c-trm p at f;
theorem :: ABCMIZ_1:135
((non_op C)term a)at f = (non_op C)term(a at f);
theorem :: ABCMIZ_1:136
((ast C)term(a,t))at f = (ast C)term(a at f,t at f);
theorem :: ABCMIZ_1:137
for X being Subset of Vars holds e at (C idval X) = e;
theorem :: ABCMIZ_1:138
for X being Subset of Vars
holds (C idval X)# = id Union the Sorts of Free(C, MSVars C);
theorem :: ABCMIZ_1:139
for f being empty valuation of C holds e at f = e;
theorem :: ABCMIZ_1:140
for f being empty valuation of C
holds f# = id Union the Sorts of Free(C, MSVars C);
definition
let C,f;
let t be quasi-term of C;
redefine func t at f -> quasi-term of C;
end;
definition
let C,f;
let a be expression of C, an_Adj C;
redefine func a at f -> expression of C, an_Adj C;
end;
registration
let C,f;
let a be positive expression of C, an_Adj C;
cluster a at f -> positive for expression of C, an_Adj C;
end;
registration
let C,f;
let a be negative expression of C, an_Adj C;
cluster a at f -> negative for expression of C, an_Adj C;
end;
definition
let C,f;
let a be quasi-adjective of C;
redefine func a at f -> quasi-adjective of C;
end;
theorem :: ABCMIZ_1:141
(Non a) at f = Non (a at f);
definition
let C,f;
let t be expression of C, a_Type C;
redefine func t at f -> expression of C, a_Type C;
end;
registration
let C,f;
let t be pure expression of C, a_Type C;
cluster t at f -> pure for expression of C, a_Type C;
end;
theorem :: ABCMIZ_1:142
for f being irrelevant one-to-one valuation of C
ex g being irrelevant one-to-one valuation of C
st for x,y being variable holds
x in dom f & f.x = y-term C iff y in dom g & g.y = x-term C;
theorem :: ABCMIZ_1:143
for f,g being irrelevant one-to-one valuation of C
st for x,y being variable holds
x in dom f & f.x = y-term C implies y in dom g & g.y = x-term C
for e st variables_in e c= dom f
holds e at f at g = e;
definition
let C,f;
let A be Subset of QuasiAdjs C;
func A at f -> Subset of QuasiAdjs C equals
:: ABCMIZ_1:def 64
{a at f where a is quasi-adjective of C: a in A};
end;
theorem :: ABCMIZ_1:144
for A being Subset of QuasiAdjs C for a being quasi-adjective of C st A = {a}
holds A at f = {a at f};
theorem :: ABCMIZ_1:145
for A,B being Subset of QuasiAdjs C
holds (A \/ B) at f = (A at f) \/ (B at f);
theorem :: ABCMIZ_1:146
for A,B being Subset of QuasiAdjs C st A c= B holds A at f c= B at f;
registration
let C be initialized ConstructorSignature;
let f be valuation of C;
let A be finite Subset of QuasiAdjs C;
cluster A at f -> finite;
end;
definition
let C be initialized ConstructorSignature;
let f be valuation of C;
let T be quasi-type of C;
func T at f -> quasi-type of C equals
:: ABCMIZ_1:def 65
((adjs T) at f)ast((the_base_of T) at f);
end;
theorem :: ABCMIZ_1:147
for T being quasi-type of C holds adjs(T at f) = (adjs T) at f &
the_base_of (T at f) = (the_base_of T) at f;
theorem :: ABCMIZ_1:148
for T being quasi-type of C for a being quasi-adjective of C
holds (a ast T) at f = (a at f) ast (T at f);
definition
let C be initialized ConstructorSignature;
let f,g be valuation of C;
func f at g -> valuation of C means
:: ABCMIZ_1:def 66
dom it = (dom f) \/ dom g & for x being variable st x in dom it
holds it.x = ((x-term C) at f) at g;
end;
registration
let C be initialized ConstructorSignature;
let f,g be irrelevant valuation of C;
cluster f at g -> irrelevant;
end;
theorem :: ABCMIZ_1:149
for f1,f2 being valuation of C holds (e at f1) at f2 = e at (f1 at f2);
theorem :: ABCMIZ_1:150
for A being Subset of QuasiAdjs C for f1,f2 being valuation of C
holds (A at f1) at f2 = A at (f1 at f2);
theorem :: ABCMIZ_1:151
for T being quasi-type of C for f1,f2 being valuation of C
holds (T at f1) at f2 = T at (f1 at f2);