[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Extended ASCII in MML
Below you will find the propositions for the revision
of the Mizar Mathematical Library. The aim is to remove
some of extended ASCII characters from vocabularies.
In the text below extended ASCII characters are encoded
according to
http://mizar.org/JFM/ASCII/ExtAscii.html
('#'<decimal_number>)
As of now, 38 ext. ASCII characters are in mml.vct file
(vocabulary for MML) used by 75 symbols. We plan to
eliminate 9 characters from the vocabularies, that is:
#192 #217 #218 #191 #243 #251 #220 #174 #175
3 predicate symbols are not used at all (vocabulary PARSP_2):
#192-, #220, #240#175. They should be removed.
After this revision 59 symbols will still remain.
--------------------
The propositions (pretty long):
1. G#218#191-SemiLattStr change into: /\-SemiLattStr
:: LATTICES
struct(1-sorted) #218#191-SemiLattStr
(# carrier -> set, L_meet -> BinOp of the carrier #);
--------------------------------
2. G#192#217-SemiLattStr change into: \/-SemiLattStr
:: LATTICES
struct(1-sorted) #192#217-SemiLattStr
(# carrier -> set, L_join -> BinOp of the carrier #);
--------------------------------
3. O#192#217 change into: \/
definition let G be non empty #192#217-SemiLattStr,
p, q be Element of the carrier of G;
func p #192#217 q -> Element of the carrier of G equals
:: LATTICES:def 1
(the L_join of G).(p,q);
end;
definition let X be set; let EqR1,EqR2 be Equivalence_Relation of X;
func EqR1 #192#217 EqR2 -> Equivalence_Relation of X means
:: EQREL_1:def 3
EqR1 U EqR2 c= it & for EqR being Equivalence_Relation of X
st EqR1 U EqR2 c= EqR holds it c= EqR;
end;
definition let G be Group; let H1,H2 be Subgroup of G;
func H1 #192#217 H2 -> strict Subgroup of G equals
:: GROUP_4:def 10
gr(carr H1 U carr H2);
end;
definition let A be non empty RelStr such that A is antisymmetric;
let a,b be Element of the carrier of A such that
ex x being Element of A st a <= x & b <= x &
for c being Element of A st a <= c & b <= c holds x <= c;
func a #192#217 b -> Element of A means
:: LATTICE3:def 13
a <= it & b <= it &
for c being Element of A st a <= c & b <= c holds it <= c;
end;
definition let L be Lattice, D1,D2 be non empty Subset of the carrier of L;
func D1 #192#217 D2 -> Subset of the carrier of L equals
:: FILTER_2:def 13
{ p #192#217 q : p #238 D1 & q #238 D2 };
end;
definition let C1, C2 be Coherence_Space;
func C1 #192#217 C2 -> set equals
:: COHSP_1:def 25
{a U+ #237 where a is Element of C1: not contradiction} U
{#237 U+ b where b is Element of C2: not contradiction};
end;
definition
let I be non empty set,
M be ManySortedSet of I;
let EqR1,EqR2 be Equivalence_Relation of M;
func EqR1 #192#217 EqR2 -> Equivalence_Relation of M means
:: MSUALG_5:def 4
ex EqR3 being ManySortedRelation of M st EqR3 = EqR1 U EqR2 &
it = EqCl EqR3;
end;
definition let L be non empty RelStr,
D1, D2 be Subset of the carrier of L;
func D1 #192#217 D2 -> Subset of L equals
:: YELLOW_4:def 3
{ x #192#217 y where x, y is Element of L : x #238 D1 & y #238 D2 };
end;
--------------------------------
4. O#218#191 change into: /\
definition let G be non empty #218#191-SemiLattStr,
p, q be Element of the carrier of G;
func p #218#191 q -> Element of the carrier of G equals
:: LATTICES:def 2
(the L_meet of G).(p,q);
end;
definition let L,D1,D2;
func D1 #218#191 D2 -> Subset of the carrier of L equals
:: FILTER_0:def 9
{ p #218#191 q : p #238 D1 & q #238 D2 };
end;
definition let A be non empty RelStr such that A is antisymmetric;
let a,b be Element of the carrier of A such that
ex x being Element of A st a >= x & b >= x &
for c being Element of A st a >= c & b >= c holds x >= c;
func a #218#191 b -> Element of A means
:: LATTICE3:def 14
it <= a & it <= b &
for c being Element of A st c <= a & c <= b holds c <= it;
end;
definition
let C1, C2 be Coherence_Space;
func C1 #218#191 C2 -> set equals
:: COHSP_1:def 24
{a U+ b where a is Element of C1, b is Element of C2: not contradiction};
end;
definition let S be non empty RelStr; let x be Element of S;
func x #218#191 -> map of S,S means
:: WAYBEL_1:def 18
for s being Element of S holds it.s = x #218#191 s;
end;
definition let L be non empty RelStr,
D1, D2 be Subset of the carrier of L;
func D1 #218#191 D2 -> Subset of L equals
:: YELLOW_4:def 4
{ x #218#191 y where x, y is Element of L : x #238 D1 & y #238 D2 };
end;
definition let L be non empty RelStr,
x be Element of L,
N be non empty NetStr over L;
func x #218#191 N -> strict NetStr over L means
:: WAYBEL_2:def 3
the RelStr of it = the RelStr of N &
for i being Element of the carrier of it ex y being Element of L st
y = (the mapping of N).i & (the mapping of it).i = x #218#191 y;
end;
--------------------------------
5. R#243#243 change into: [=
definition let G be non empty #192#217-SemiLattStr,
p, q be Element of the carrier of G;
pred p #243#243 q means
:: LATTICES:def 3 :: #243
p #192#217 q = q;
end;
--------------------------------
6. R#243` change into: <=`
definition let M,N be Cardinal;
redefine pred M c= N;
:: CARD_1
synonym M #243` N;
end;
--------------------------------
7. K#192 change into: [\
L#217 change into: /]
definition let r be real number;
func #192 r #217 -> Integer means
:: INT_1:def 4
it <= r & r - 1 < it;
end;
--------------------------------
8. K#218 change into: [/
L#191 change into: \]
definition let r be real number;
func #218 r #191 -> Integer means
:: INT_1:def 5
r <= it & it < r + 1;
end;
--------------------------------
9. O#251 change into: sqrt
definition let a be real number;
assume 0 <= a;
func #251 a -> real number means
:: SQUARE_1:def 4
0 <= it & it #253 = a;
end;
O#251 change into: -root
definition let n be Nat; let a be real number;
func n #251 a -> real number equals
:: POWER:def 1
n #251N a if a>=0 & n>=1,
- n #251N (-a) if a<0 & ex m being Nat st n=2 #249 m+1;
end;
--------------------------------
10. O#251N change into: -Root
definition let n; let a be real number;
assume 1 <= n;
func n #251N a -> real number means
:: PREPOWER:def 3
it #N n = a & it > 0 if a>0,
it = 0 if a=0;
end;
--------------------------------
11. #174#240#175 removed as equal to DIRAF:def 4
definition let AFV be WeakAffVect;
let a,b,c,d be Element of the carrier of AFV;
pred a,b #174#240#175 c,d means
:: AFVECT01:def 1
a,b // c,d or a,b // d,c;
end;
--------------------------------
Comments are welcome.
Adam Grabowski
Institute of Mathematics
University of Bialystok
------------
Library Committee of the Association of Mizar Users