% mathematical symbols by Anthony Phan.
% file: mathsymb.mf (various mathematical symbols)
% last modification: May 16, 2005.
% Only known charcodes will be generated.

def horizontal_rules_list=math_axis,
  -body_depth,-desc_depth,x_height,cap_height,asc_height,body_height
enddef;

%%% !!! marked signs are to be revised

use_rule1;

%
% Usual binary relations.
%

beginchar(negation_sign,12u#+2appr#,v_center(spread1#+rth#));
  "Negation sign";
  pickup tiny.nib;
  pos1(rth,90); pos3(rth,0);
  y2r=y1r; y2l=y1l; x2l=x3l; x2r=x3r;
  y1=math_axis+0.5spread1; y1l-y3=spread1;
  lft x1=Appr; rt x3r=w-Appr;
  filldraw stroke z1e--z2e--z3e;
  penlabels(1,2,3);
endchar;

beginchar(not_sign,12u#+2appr#,asc_height#,asc_depth#);
  "Not sign";
  pickup tiny.nib;
  pos1(rth,0); pos2(rth,0);
  top y1=h+eps; 0.5[bot y2,top y1]=math_axis;
  lft x1l=lft x2l=hround 0.5(w-rth);
  filldraw stroke z1e..z2e; penlabels(1,2);
  charwd:=0; w:=0;
endchar;

beginchar(varnot_sign,12u#+2appr#,asc_height#,asc_depth#);
  "Variant not sign";
  pickup tiny.nib;
  lft x2l=w-rt x1r=appr+hround 1.75u;
  top y1r=h+eps; 0.5[bot y2l,top y1r]=math_axis;
  adjust_slanted_bar(2l,1r,2r,1l)(rth-tiny,-1);
  filldraw stroke z1e..z2e; penlabels(1,2);
  charwd:=0; w:=0;
endchar;

%
% equality signs and related things (relations).
%

beginchar(colon_sign,3u#+2appr#,x_height#,0);
  "Colon";
  pickup null.nib;
  adjust_dot1((0.5w,h-0.5dtsz),dtsz,false,false);
  adjust_dot2((0.5w,0.5dtsz),dtsz,false,false);
  dot(1,1'); dot(2,2');
endchar;

beginchar(colon_equal_sign,15u#+2appr#,v_center(spread1#+rth#));
  "Colon-equal sign";
  pickup tiny.nib;
  pos1(rth,90); pos2(rth,90); pos3(rth,90); pos4(rth,90);
  lft x1=lft x3=Appr+hround 3u; rt x2=rt x4=w-Appr;
  y1=y2; y3=y4; y1-y3=spread1; .5[y1,y3]=math_axis;
  filldraw stroke z1e..z2e; filldraw stroke z3e..z4e;
  penlabels(1,2,3,4); pickup null.nib;
  adjust_dot5((appr+1.5u,math_axis
      +0.5max(0.5[x_height-dtsz,spread1],spread1)),
    dtsz,false,false); dot(5,5');
  adjust_dot6((appr+1.5u,math_axis
      -0.5max(0.5[x_height-dtsz,spread1],spread1)),
    dtsz,false,false); dot(6,6');
endchar;

beginchar(equal_colon_sign,15u#+2appr#,v_center(spread1#+rth#));
  "Equal-colon sign";
  pickup tiny.nib;
  pos1(rth,90); pos2(rth,90); pos3(rth,90); pos4(rth,90);
  lft x1=lft x3=Appr; rt x2=rt x4=w-Appr-hround 3u;
  y1=y2; y3=y4; y1-y3=spread1; .5[y1,y3]=math_axis;
  filldraw stroke z1e..z2e; filldraw stroke z3e..z4e;
  penlabels(1,2,3,4); pickup null.nib;
  adjust_dot5((w-appr-1.5u,math_axis
      +0.5max(0.5[x_height-dtsz,spread1],spread1)),
    dtsz,false,false);
  adjust_dot6((w-appr-1.5u,math_axis
      -0.5max(0.5[x_height-dtsz,spread1],spread1)),
    dtsz,false,false);
  dot(5,5'); dot(6,6');
  penlabels(1,2,3,4);
endchar;

beginchar(top_dot_equal_sign,arithmetic_bounds);
  "Top dot equal sign";
  pickup tiny.nib;
  pos1(rth,90); pos2(rth,90); pos3(rth,90); pos4(rth,90);
  lft x1=lft x3=Appr; rt x2=rt x4=w-Appr;
  y1=y2; y3=y4; y1-y3=spread1; .5[y1,y3]=math_axis;
  filldraw stroke z1e..z2e; filldraw stroke z3e..z4e;
  penlabels(1,2,3,4); pickup null.nib;
  adjust_dot5((0.5[x1,x2],
      min(y1+math_spread[0.5x_height,0.6x_height],h-0.5dtsz)),
    dtsz,true,false); dot(5,5');
endchar;

beginchar(bot_dot_equal_sign,arithmetic_bounds);
  "Bot dot equal sign";
  pickup tiny.nib;
  pos1(rth,90); pos2(rth,90); pos3(rth,90); pos4(rth,90);
  lft x1=lft x3=Appr; rt x2=rt x4=w-Appr;
  y1=y2; y3=y4; y1-y3=spread1; .5[y1,y3]=math_axis;
  filldraw stroke z1e..z2e; filldraw stroke z3e..z4e;
  penlabels(1,2,3,4); pickup null.nib;
  adjust_dot5((0.5[x1,x2],
      max(y3-math_spread[0.5x_height,0.6x_height],-d+0.5dtsz)),
    dtsz,true,false); dot(5,5');
endchar;

beginchar(top_bot_dot_equal_sign,arithmetic_bounds);
  "Top bot dot equal sign";
  pickup tiny.nib;
  pos1(rth,90); pos2(rth,90); pos3(rth,90); pos4(rth,90);
  lft x1=lft x3=Appr; rt x2=rt x4=w-Appr;
  y1=y2; y3=y4; y1-y3=spread1; .5[y1,y3]=math_axis;
  filldraw stroke z1e..z2e; filldraw stroke z3e..z4e;
  penlabels(1,2,3,4); pickup null.nib;
  adjust_dot5((0.5[x1,x2],
      min(y1+math_spread[0.5x_height,0.6x_height],h-0.5dtsz)),
    dtsz,true,false); dot(5,5');
  adjust_dot6((0.5[x1,x2],
      max(y3-math_spread[0.5x_height,0.6x_height],-d+0.5dtsz)),
    dtsz,true,false); dot(6,6');
endchar;

beginchar(rising_dots_equal_sign,arithmetic_bounds);
  "Rising dots equal sign";
  pickup tiny.nib;
  pos1(rth,90); pos2(rth,90); pos3(rth,90); pos4(rth,90);
  lft x1=lft x3=Appr; rt x2=rt x4=w-Appr;
  y1=y2; y3=y4; y1-y3=spread1; .5[y1,y3]=math_axis;
  filldraw stroke z1e..z2e; filldraw stroke z3e..z4e;
  penlabels(1,2,3,4); pickup null.nib;
  adjust_dot5((w-appr-0.5dtsz,
      min(y1+math_spread[0.5x_height,0.6x_height],h-0.5dtsz)),
    dtsz,false,false); dot(5,5');
  adjust_dot6((appr+0.5dtsz,
      max(y3-math_spread[0.5x_height,0.6x_height],-d+0.5dtsz)),
    dtsz,false,false); dot(6,6');
endchar;

beginchar(falling_dots_equal_sign,arithmetic_bounds);
  "Falling dots equal sign";
  pickup tiny.nib;
  pos1(rth,90); pos2(rth,90); pos3(rth,90); pos4(rth,90);
  lft x1=lft x3=Appr; rt x2=rt x4=w-Appr;
  y1=y2; y3=y4; y1-y3=spread1; .5[y1,y3]=math_axis;
  filldraw stroke z1e..z2e; filldraw stroke z3e..z4e;
  penlabels(1,2,3,4); pickup null.nib;
  adjust_dot5((appr+0.5dtsz,
      min(y1+math_spread[0.5x_height,0.6x_height],h-0.5dtsz)),
    dtsz,false,false); dot(5,5');
  adjust_dot6((w-appr-0.5dtsz,
      max(y3-math_spread[0.5x_height,0.6x_height],-d+0.5dtsz)),
    dtsz,false,false); dot(6,6');
endchar;

beginchar(bump_equal,12u#+2appr#,v_center(spread1#+rth#));
  "bumped equal sign";
  numeric t[];
  pickup tiny.nib;
  pos1(rth,90); pos2(rth,90); pos3(rth,90); pos4(rth,90);
  pos5(rth,180); pos6(rth,90); pos7(rth,0);
  lft x1=lft x3=appr; rt x2=rt x4=w-appr;
  y1=y2; y3=y4; y1-y3=spread1; .5[y1,y3]=math_axis;
  rt x5l=hround 1/3[lft x1,rt x2]; x5l-x1=x2-x7l;
  y5=y7=y1l; x6=0.5[x5,x7]; y6l-y1l=vround 0.5(x7l-x5l);
  tmp_path:=z7r up_to_left z6r left_to_down z5r;
  t1=xpart(tmp_path intersectiontimes (z2r..0.5[z1r,z2r]));
  t2=xpart(tmp_path intersectiontimes (z1r..0.5[z1r,z2r]));
  filldraw z1l--z5l up_to_right z6l right_to_down z7l--z2l--
  z2r--subpath(t1,t2) of tmp_path--z1r--cycle;
  filldraw stroke z3e..z4e; penlabels(1,2,3,4,5,6,7);
endchar;

beginchar(pump_equal,12u#+2appr#,v_center(spread1#+rth#));
  "pumped equal sign";
  numeric t[];
  pickup tiny.nib;
  pos1(rth,90); pos2(rth,90); pos3(rth,90); pos4(rth,90);
  pos8(rth,0); pos9(rth,90); pos10(rth,180);
  lft x1=lft x3=appr; rt x2=rt x4=w-appr;
  y1=y2; y3=y4; y1-y3=spread1; .5[y1,y3]=math_axis;
  rt x8r=hround 1/3[lft x1,rt x2]; x8r-x3=x4-x10r;
  y8=y10=y3r; x9=0.5[x8,x10]; y3r-y9r=vround 0.5(x10r-x8r);
  tmp_path:=z8l down_to_right z9l right_to_up z10l;
  t1=xpart(tmp_path intersectiontimes (z3l..0.5[z3l,z4l]));
  t2=xpart(tmp_path intersectiontimes (z4l..0.5[z3l,z4l]));
  filldraw z3l--subpath(t1,t2) of tmp_path--z4l
  --z4r--z10r up_to_left z9r left_to_down z8r--z3r--cycle;
  filldraw stroke z1e..z2e; penlabels(1,2,3,4,8,9,10);
endchar;

beginchar(Bump_equal,12u#+2appr#,v_center(spread1#+rth#));
  "Bumped equal";
  numeric t[];
  pickup tiny.nib;
  pos1(rth,90); pos2(rth,90); pos3(rth,90); pos4(rth,90);
  pos5(rth,180); pos6(rth,90); pos7(rth,0); pos8(rth,0);
  pos9(rth,90); pos10(rth,180);
  lft x1=lft x3=appr; rt x2=rt x4=w-appr;
  y1=y2; y3=y4; y1-y3=spread1; .5[y1,y3]=math_axis;
  rt x5l=rt x8r=hround 1/3[lft x1,rt x2]; x5l-x1=x2-x7l; x10r=x7l;
  y5=y7=y1l; y8=y10=y3r; x6=x9=0.5[x5,x7];
  y6l-y1l=y3r-y9r=vround 0.5(x7l-x5l);
  tmp_path:=z7r up_to_left z6r left_to_down z5r;
  tmpp_path:=z8l down_to_right z9l right_to_up z10l;
  t1=xpart(tmp_path intersectiontimes (z2r..0.5[z1r,z2r]));
  t2=xpart(tmp_path intersectiontimes (z1r..0.5[z1r,z2r]));
  t3=xpart(tmpp_path intersectiontimes (z3l..0.5[z3l,z4l]));
  t4=xpart(tmpp_path intersectiontimes (z4l..0.5[z3l,z4l]));
  filldraw z1l--z5l up_to_right z6l right_to_down z7l--z2l--
  z2r--subpath(t1,t2) of tmp_path--z1r--cycle;
  filldraw z3l--subpath(t3,t4) of tmpp_path--z4l
  --z4r--z10r up_to_left z9r left_to_down z8r--z3r--cycle;
  penlabels(1,2,3,4,5,6,7,8,9,10);
endchar;

%%% !!!
beginchar(circ_equal_sign,arithmetic_bounds);
  "Circle-equal sign";
  pickup tiny.nib;
  pos1(rth,90); pos2(rth,90); pos3(rth,90); pos4(rth,90);
  lft x1=lft x3=Appr; rt x2=rt x4=w-Appr;
  y1=y2; y3=y4; y1-y3=spread1; .5[y1,y3]=math_axis;
  filldraw stroke z1e..z2e; % upper bar
  filldraw stroke z3e..z4e; % lower bar
  pickup rule.nib0;
  a:=min(max(7u,dtsz+rth0),spread1+rth);
  adjust_dot5((0.5[x1,x2],max(vround(1/6[top y1,h])+0.5a,h-0.5a)+o),
    a,true,false);
  full_dot:=false; dot(5,5');
  penlabels(1,2);
endchar;

beginchar(equal_circ_sign,12u#+2appr#,v_center(spread1#+rth#));
  "Equal-circle sign";
  pickup tiny.nib;
  pos1(rth,90); pos2(rth,90); pos3(rth,90); pos4(rth,90);
  lft x1=lft x3=Appr; rt x2=rt x4=w-Appr;
  y1=y2; y3=y4; y1-y3=spread1; .5[y1,y3]=math_axis;
  filldraw stroke z1e..z2e; % upper bar
  filldraw stroke z3e..z4e; % lower bar
  pickup rule.nib0;
  a:=min(max(7u,dtsz+rth0),spread1+rth);
  adjust_dot5(0.5[z3,z2],a,true,false);
  full_dot:=false; dot(5,5');
  penlabels(1,2);
endchar;

%%% !!!
beginchar(triangle_equal_sign,arithmetic_bounds);
  "Triangle-equal sign";
  pickup tiny.nib;
  pos1(rth,90); pos2(rth,90); pos3(rth,90); pos4(rth,90);
  lft x1=lft x3=Appr; rt x2=rt x4=w-Appr;
  y1=y2; y3=y4; y1-y3=spread1; .5[y1,y3]=math_axis;
  filldraw stroke z1e..z2e; % upper bar
  filldraw stroke z3e..z4e; % lower bar
  triangle_foot:=vround 1/6[top y1r,h];
  a:=min(2max(h+o-triangle_foot,spread1+rth+o)/sqrt 3,7u);
  set_triangle'(up,a,rth0,false,false);
  filldraw stroke z1'e--z2'e--z3'e--z1'e;
endchar;

%%% !!!
beginchar(correspondance_sign,arithmetic_bounds);
  "Correspondance sign";
  pickup tiny.nib;
  pos1(rth,90); pos2(rth,90); pos3(rth,90); pos4(rth,90);
  lft x1=lft x3=Appr; rt x2=rt x4=w-Appr;
  y1=y2; y3=y4; y1-y3=spread1; .5[y1,y3]=math_axis;
  filldraw stroke z1e..z2e; % upper bar
  filldraw stroke z3e..z4e; % lower bar
%
  top y6r=h+o; bot y5r=vround(1/6[top y1r,h]);
  y5r=y5l=y7r=y7l;
  x6r=0.5[x1,x2]; x5r-x1=x2-x7r=hround 0.5u;
  x5l-x5r=diag_width(rth-tiny,z6r-z5r);
  x7r-x7l=diag_width(rth-tiny,z6r-z7r);
  z6l-z5l=whatever*(z6r-z5r); z6l-z7l=whatever*(z6r-z7r);
  filldraw stroke z5e--z6e--z7e;
  penlabels(1,2,3,4,5,6,7);
endchar;

beginchar(hash_sign,arithmetic_bounds);
  "Hash sign";
  pickup tiny.nib;
  pos1(rth,90); pos2(rth,90); pos3(rth,90); pos4(rth,90);
  pos5(rth,0); pos6(rth,0); pos7(rth,0); pos8(rth,0);
  lft x1=lft x3=Appr;
  lft x5l=lft x6l=hround 0.5(w+Appr-Appr-spread1-rth);
  x7-x5=x8-x6=spread1; x2-x7r=x4-x7r=x5l-x1;
  y1=y2; y3=y4; y1-y3=spread1; .5[y1,y3]=math_axis;
  top y5=top y7=h; y5-y1=y3-y6; y8=y6;
  filldraw stroke z1e..z2e; filldraw stroke z3e..z4e;
  filldraw stroke z5e..z6e; filldraw stroke z7e..z8e;
  penlabels(1,2,3,4,5,6,7,8);
endchar;

beginchar(var_hash_sign,arithmetic_bounds);
  "Variant hash sign";
  pickup tiny.nib;
  pos1(rth,90); pos2(rth,90); pos3(rth,90); pos4(rth,90);
  lft x1=lft x3=Appr; rt x2=rt x4=w-Appr;
  y1=y2; y3=y4; y1-y3=spread1; .5[y1,y3]=math_axis;
  bot y6l=-d; top y7r=h; lft x6l=w-rt x7r=Appr+hround 1.25u;
  adjust_slanted_bar(6l,7r,8r,5l)(spread1+rth-tiny,-1);
  numeric a; a=(rth-tiny)/sind angle(z5l-z6l);
  penpos5(a,0); penpos6(a,0); penpos7(a,0); penpos8(a,0);
% I'm not sure that it's a good idea, but wel, that's
% school works.
  filldraw stroke z1e..z2e; filldraw stroke z3e..z4e;
  filldraw stroke diag_stroke.e(5,6,r,y1r,y1l,y3r,y3l);
  filldraw stroke diag_stroke.e(7,8,r,y1r,y1l,y3r,y3l);
%  filldraw stroke z5e..z6e; filldraw stroke z7e..z8e;
  penlabels(1,2,3,4,5,6,7,8);
endchar;

beginchar(vdash_sign,12u#+2appr#,v_center(12u#));
  "vdash sign";
  pickup tiny.nib;
  pos1(rth,0); pos2(rth,0); pos3(rth,90); pos4(rth,90);
  lft x1l=lft x2l=Appr; rt x4=w-Appr; x3=x1;
  top y1=h; 0.5[y1,y2]=math_axis=y3=y4;
  filldraw stroke z1e..z2e; filldraw stroke z3e..z4e;
  penlabels(1,2,3,4); tmp_picture:=currentpicture;
endchar;

beginchar(vdash_not,12u#+2appr#,asc_height#,asc_depth#);
  "Not vdash sign";
  currentpicture:=tmp_picture;
  pickup tiny.nib;
  lft x2l=w-rt x1r=appr+hround 1.75u;
  top y1r=h+eps; 0.5[bot y2l,top y1r]=math_axis;
  adjust_slanted_bar(2l,1r,2r,1l)(rth-tiny,-1);
  filldraw stroke z1e..z2e; penlabels(1,2);
endchar;

beginchar(dashv_sign,12u#+2appr#,v_center(12u#));
  "dashv sign";
  pickup tiny.nib;
  pos1(rth,0); pos2(rth,0); pos3(rth,90); pos4(rth,90);
  rt x1r=rt x2r=w-Appr; lft x3=Appr; x4=x1;
  top y1=h; 0.5[y1,y2]=math_axis=y3=y4;
  filldraw stroke z1e..z2e; filldraw stroke z3e..z4e;
  penlabels(1,2,3,4); tmp_picture:=currentpicture;
endchar;

beginchar(dashv_not,12u#+2appr#,asc_height#,asc_depth#);
  "Not dashv sign";
  currentpicture:=tmp_picture;
  pickup tiny.nib;
  lft x2l=w-rt x1r=appr+hround 1.75u;
  top y1r=h+eps; 0.5[bot y2l,top y1r]=math_axis;
  adjust_slanted_bar(2l,1r,2r,1l)(rth-tiny,-1);
  filldraw stroke z1e..z2e; penlabels(1,2);
endchar;

beginchar(vDash_sign,12u#+2appr#,v_center(12u#));
  "vDash sign";
  pickup tiny.nib;
  pos1(rth,0); pos2(rth,0); pos3(rth,90); pos4(rth,90);
  pos5(rth,90); pos6(rth,90);
  lft x1l=lft x2l=Appr; rt x4=rt x6=w-Appr; x3=x5=x1;
  top y1=h; y3-y5=spread1; 0.5[y1,y2]=math_axis=0.5[y3,y5];
  y4=y3; y6=y5; filldraw stroke z1e..z2e; filldraw stroke z3e..z4e;
  filldraw stroke z5e..z6e; penlabels(1,2,3,4,5,6);
  tmp_picture:=currentpicture;
endchar;

beginchar(vDash_not,12u#+2appr#,asc_height#,asc_depth#);
  "Not vDash sign";
  currentpicture:=tmp_picture;
  pickup tiny.nib;
  lft x2l=w-rt x1r=appr+hround 1.75u;
  top y1r=h+eps; 0.5[bot y2l,top y1r]=math_axis;
  adjust_slanted_bar(2l,1r,2r,1l)(rth-tiny,-1);
  filldraw stroke z1e..z2e; penlabels(1,2);
endchar;

beginchar(Dashv_sign,12u#+2appr#,v_center(12u#));
  "Dashv sign";
  pickup tiny.nib;
  pos1(rth,0); pos2(rth,0); pos3(rth,90); pos4(rth,90);
  pos5(rth,90); pos6(rth,90);
  rt x1r=rt x2r=w-Appr; lft x3=lft x5=Appr; x4=x6=x1;
  top y1=h; y3-y5=spread1; 0.5[y1,y2]=math_axis=0.5[y3,y5];
  y4=y3; y6=y5; filldraw stroke z1e..z2e; filldraw stroke z3e..z4e;
  filldraw stroke z5e..z6e; penlabels(1,2,3,4,5,6);
  tmp_picture:=currentpicture;
endchar;

beginchar(Dashv_not,12u#+2appr#,asc_height#,asc_depth#);
  "Not Dashv sign";
  currentpicture:=tmp_picture;
  pickup tiny.nib;
  lft x2l=w-rt x1r=appr+hround 1.75u;
  top y1r=h+eps; 0.5[bot y2l,top y1r]=math_axis;
  adjust_slanted_bar(2l,1r,2r,1l)(rth-tiny,-1);
  filldraw stroke z1e..z2e; penlabels(1,2);
endchar;

beginchar(Vdash_sign,12u#+2appr#,v_center(12u#));
  "Vdash sign";
  pickup tiny.nib;
  pos1(rth,0); pos2(rth,0); pos3(rth,0); pos4(rth,0);
  pos5(rth,90); pos6(rth,90);
  lft x1l=lft x2l=Appr; x3=x4=x1+spread1;
  rt x6=w-appr; x5=x3;
  top y1=h; 0.5[y1,y2]=math_axis=y5=y6; y1=y3; y2=y4;
  filldraw stroke z1e..z2e; filldraw stroke z3e..z4e;
  filldraw stroke z5e..z6e; penlabels(1,2,3,4,5,6);
  tmp_picture:=currentpicture;
endchar;

beginchar(Vdash_not,12u#+2appr#,asc_height#,asc_depth#);
  "Not Vdash sign";
  currentpicture:=tmp_picture;
  pickup tiny.nib;
  lft x2l=w-rt x1r=appr+hround 1.75u;
  top y1r=h+eps; 0.5[bot y2l,top y1r]=math_axis;
  adjust_slanted_bar(2l,1r,2r,1l)(rth-tiny,-1);
  filldraw stroke z1e..z2e; penlabels(1,2);
endchar;

beginchar(dashV_sign,12u#+2appr#,v_center(12u#));
  "dashV sign";
  pickup tiny.nib;
  pos1(rth,0); pos2(rth,0); pos3(rth,0); pos4(rth,0);
  pos5(rth,90); pos6(rth,90);
  rt x1r=rt x2r=w-Appr; x3=x4=x1-spread1;
  lft x5=appr; x6=x3;
  top y1=h; 0.5[y1,y2]=math_axis=y5=y6; y1=y3; y2=y4;
  filldraw stroke z1e..z2e; filldraw stroke z3e..z4e;
  filldraw stroke z5e..z6e; penlabels(1,2,3,4,5,6);
  tmp_picture:=currentpicture;
endchar;

beginchar(dashV_not,12u#+2appr#,asc_height#,asc_depth#);
  "Not dashV sign";
  currentpicture:=tmp_picture;
  pickup tiny.nib;
  lft x2l=w-rt x1r=appr+hround 1.75u;
  top y1r=h+eps; 0.5[bot y2l,top y1r]=math_axis;
  adjust_slanted_bar(2l,1r,2r,1l)(rth-tiny,-1);
  filldraw stroke z1e..z2e; penlabels(1,2);
endchar;

beginchar(VDash_sign,12u#+2appr#,v_center(12u#));
  "VDash sign";
  pickup tiny.nib;
  pos1(rth,0); pos2(rth,0); pos3(rth,0); pos4(rth,0);
  pos5(rth,90); pos6(rth,90); pos7(rth,90); pos8(rth,90);
  lft x1l=lft x2l=Appr; x3=x4=x1+spread1;
  rt x6=rt x8=w-appr; x5=x7=x3;
  top y1=h; y5-y7=spread1;
  0.5[y1,y2]=0.5[y5,y7]=math_axis;
  y1=y3; y2=y4; y5=y6; y7=y8;
  filldraw stroke z1e..z2e; filldraw stroke z3e..z4e;
  filldraw stroke z5e..z6e; filldraw stroke z7e..z8e;
  penlabels(1,2,3,4,5,6,7,8); tmp_picture:=currentpicture;
endchar;

beginchar(VDash_not,12u#+2appr#,asc_height#,asc_depth#);
  "Not Vdash sign";
  currentpicture:=tmp_picture;
  pickup tiny.nib;
  lft x2l=w-rt x1r=appr+hround 1.75u;
  top y1r=h+eps; 0.5[bot y2l,top y1r]=math_axis;
  adjust_slanted_bar(2l,1r,2r,1l)(rth-tiny,-1);
  filldraw stroke z1e..z2e; penlabels(1,2);
endchar;

beginchar(DashV_sign,12u#+2appr#,v_center(12u#));
  "DashV sign";
  pickup tiny.nib;
  pos1(rth,0); pos2(rth,0); pos3(rth,0); pos4(rth,0);
  pos5(rth,90); pos6(rth,90); pos7(rth,90); pos8(rth,90);
  rt x1r=rt x2r=w-Appr; x3=x4=x1-spread1;
  lft x5=lft x7=appr; x6=x8=x3;
  top y1=h; y5-y7=spread1;
  0.5[y1,y2]=0.5[y5,y7]=math_axis;
  y1=y3; y2=y4; y5=y6; y7=y8;
  filldraw stroke z1e..z2e; filldraw stroke z3e..z4e;
  filldraw stroke z5e..z6e; filldraw stroke z7e..z8e;
  penlabels(1,2,3,4,5,6,7,8); tmp_picture:=currentpicture;
endchar;

beginchar(DashV_not,12u#+2appr#,asc_height#,asc_depth#);
  "Not DashV sign";
  currentpicture:=tmp_picture;
  pickup tiny.nib;
  lft x2l=w-rt x1r=appr+hround 1.75u;
  top y1r=h+eps; 0.5[bot y2l,top y1r]=math_axis;
  adjust_slanted_bar(2l,1r,2r,1l)(rth-tiny,-1);
  filldraw stroke z1e..z2e; penlabels(1,2);
endchar;

beginchar(Vvdash_sign,12u#+2appr#,v_center(12u#));
  "Vvdash sign";
  pickup tiny.nib;
  pos1(rth,0); pos2(rth,0); pos3(rth,0); pos4(rth,0);
  pos5(rth,0); pos6(rth,0); pos7(rth,90); pos8(rth,90);
  lft x1l=lft x2l=Appr; x3=x4=x1+spread1; x5=x6=x3+spread1;
  rt x8=w-appr; x7=x5;
  top y1=h; 0.5[y1,y2]=math_axis=y7=y8; y1=y3=y5; y2=y4=y6;
  filldraw stroke z1e..z2e; filldraw stroke z3e..z4e;
  filldraw stroke z5e..z6e; filldraw stroke z7e..z8e;
  penlabels(1,2,3,4,5,6,7,8); tmp_picture:=currentpicture;
endchar;

beginchar(Vvdash_not,12u#+2appr#,asc_height#,asc_depth#);
  "Not Vvdash sign";
  currentpicture:=tmp_picture;
  pickup tiny.nib;
  lft x2l=w-rt x1r=appr+hround 1.75u;
  top y1r=h+eps; 0.5[bot y2l,top y1r]=math_axis;
  adjust_slanted_bar(2l,1r,2r,1l)(rth-tiny,-1);
  filldraw stroke z1e..z2e; penlabels(1,2);
endchar;

beginchar(dashVv_sign,12u#+2appr#,v_center(12u#));
  "dashVv sign";
  pickup tiny.nib;
  pos1(rth,0); pos2(rth,0); pos3(rth,0); pos4(rth,0);
  pos5(rth,0); pos6(rth,0); pos7(rth,90); pos8(rth,90);
  rt x1r=rt x2r=w-Appr; x3=x4=x1-spread1; x5=x6=x3-spread1;
  lft x7=appr; x8=x5;
  top y1=h; 0.5[y1,y2]=math_axis=y7=y8; y1=y3=y5; y2=y4=y6;
  filldraw stroke z1e..z2e; filldraw stroke z3e..z4e;
  filldraw stroke z5e..z6e; filldraw stroke z7e..z8e;
  penlabels(1,2,3,4,5,6,7,8); tmp_picture:=currentpicture;
endchar;

beginchar(dashVv_not,12u#+2appr#,asc_height#,asc_depth#);
  "Not dashVv sign";
  currentpicture:=tmp_picture;
  pickup tiny.nib;
  lft x2l=w-rt x1r=appr+hround 1.75u;
  top y1r=h+eps; 0.5[bot y2l,top y1r]=math_axis;
  adjust_slanted_bar(2l,1r,2r,1l)(rth-tiny,-1);
  filldraw stroke z1e..z2e; penlabels(1,2);
endchar;

beginchar(therefore_sign,arithmetic_bounds);
  "Therefore sign";
  pickup null.nib;
  a:=(12u-dtsz)/sqrt 12;
  x0=0.5w; y0=math_axis;
  adjust_dot1((x0,y0+2a),dtsz,false,false);
  adjust_dot2((appr+0.5dtsz,y0-a),dtsz,false,false);
  adjust_dot3((w-appr-0.5dtsz,y0-a),dtsz,false,false);
  dot(1,1'); dot(2,2'); dot(3,3');
endchar;

beginchar(because_sign,arithmetic_bounds);
  "Because sign";
  pickup null.nib;
  a:=(12u-dtsz)/sqrt 12;
  x0=0.5w; y0=math_axis;
  adjust_dot1((x0,y0-2a),dtsz,false,false);
  adjust_dot2((appr+0.5dtsz,y0+a),dtsz,false,false);
  adjust_dot3((w-appr-0.5dtsz,y0+a),dtsz,false,false);
  dot(1,1'); dot(2,2'); dot(3,3');
endchar;

beginchar(bowtie_sign,arithmetic_bounds);
  "Bowtie sign";
  pickup tiny.nib;
  a:=(11u+rth-tiny)/sqrt 2;% see times_sign
  y1r=y3l=good.y(math_axis+0.5a); y2l=y4r=y1r-vround a;
  lft x1r=lft x4r=Appr; rt x2l=rt x3l=w-Appr;
  adjust_slanted_bar(1r,2l,1,2)(rth-tiny,-1);
  adjust_slanted_bar(4r,3l,4,3)(rth-tiny,1);
  rth-tiny=x1l-x1r=x2l-x2r=x3l-x3r=x4l-x4r;
  z1l=whatever[z1,z2l]; z2r=whatever[z2,z1r];
  z3r=whatever[z3,z4r]; z4l=whatever[z4,z3l];
  filldraw stroke z1e--z2e--z3e--z4e--z1e;
  penlabels(1,2,3,4);
endchar;

%
% domination signs and related things (relations).
%

beginchar(dominated,12u#+2appr#,v_center(spread4#+rth#));
  "dominated by sign";
  pickup tiny.nib;
  top y1r=top y4r=h; y2l=y5l=good.y math_axis;
  y1r-y2l=y2l-y3r; y6r=y3r;
  lft x2l=Appr; rt x4r=w-Appr;
  x1r-x2l=x3r-x2l=x4r-x5l=x6r-x5l=hround(6.5u-tiny);
  adjust_slanted_bar(2l,1r,2a,1l)(rth-tiny,-1);
  adjust_slanted_bar(2l,3r,2b,3l)(rth-tiny,1);
  z2r=whatever[z1r,z2a]; z2r=whatever[z3r,z2b];
  z4r-z4l=z1r-z1l; z5r-z5l=z2r-z2l; z6r-z6l=z3r-z3l;
  filldraw stroke z1e--z2e--z3e; filldraw stroke z4e--z5e--z6e;
  penlabels(1,2,3,4,5,6); labels(2a,2b);
endchar;

beginchar(dominating,12u#+2appr#,v_center(spread4#+rth#));
  "dominating sign";
  pickup tiny.nib;
  top y1r=top y4r=h; y2l=y5l=good.y math_axis;
  y1r-y2l=y2l-y3r; y6r=y3r;
  lft x4r=Appr; rt x2l=w-Appr;
  x1r-x2l=x3r-x2l=x4r-x5l=x6r-x5l=-hround(6.5u-tiny);
  adjust_slanted_bar(2l,1r,2a,1l)(rth-tiny,1);
  adjust_slanted_bar(2l,3r,2b,3l)(rth-tiny,-1);
  z2r=whatever[z1r,z2a]; z2r=whatever[z3r,z2b];
  z4r-z4l=z1r-z1l; z5r-z5l=z2r-z2l; z6r-z6l=z3r-z3l;
  filldraw stroke z3e--z2e--z1e; filldraw stroke z6e--z5e--z4e;
  penlabels(1,2,3,4,5,6); labels(2a,2b);
endchar;

beginchar(Dominated,12u#+2appr#,v_center(spread4#+spread1#+rth#));
  "Dominated by sign";
  pickup tiny.nib;
  y2r=0.5[y1,y3]=0.5[y4,y6]=good.y math_axis;
  y1-y3=2(y4-y6)=spread1+spread4;
  rt x1=w-Appr; lft x2r=Appr; x1=x1r=x3=x3r=x4=x6;
  adjust_slanted_bar(2r,1,2a,1a)(0.5(rth-tiny),-1);
  adjust_slanted_bar(2r,3,2b,3b)(0.5(rth-tiny),1);
  z1r=whatever[z2r,z1a]; z3r=whatever[z2r,z3b];
  z1r-z1=z1-z1l=z4r-z4=z4-z4l; z3r-z3=z3-z3l=z6r-z6=z6-z6l;
  z2l-z1l=whatever*(z2r-z1r); z2l-z3l=whatever*(z2r-z3r);
  z5r-z4r=whatever*(z2r-z1r); z5r-z6r=whatever*(z2r-z3r);
  z5l-z4l=whatever*(z2r-z1r); z5l-z6l=whatever*(z2r-z3r);
  filldraw stroke z3e--z2e--z1e; filldraw stroke z6e--z5e--z4e;
  penlabels(1,2,3,4,5,6); labels(1a,3b,2a,2b);
endchar;

beginchar(Dominating,12u#+2appr#,v_center(spread4#+spread1#+rth#));
  "Dominated by sign";
  pickup tiny.nib;
  y2r=0.5[y1,y3]=0.5[y4,y6]=good.y math_axis;
  y1-y3=2(y4-y6)=spread1+spread4;
  lft x1=Appr; rt x2r=w-Appr; x1=x1r=x3=x3r=x4=x6;
  adjust_slanted_bar(2r,1,2a,1a)(0.5(rth-tiny),1);
  adjust_slanted_bar(2r,3,2b,3b)(0.5(rth-tiny),-1);
  z1r=whatever[z2r,z1a]; z3r=whatever[z2r,z3b];
  z1r-z1=z1-z1l=z4r-z4=z4-z4l; z3r-z3=z3-z3l=z6r-z6=z6-z6l;
  z2l-z1l=whatever*(z2r-z1r); z2l-z3l=whatever*(z2r-z3r);
  z5r-z4r=whatever*(z2r-z1r); z5r-z6r=whatever*(z2r-z3r);
  z5l-z4l=whatever*(z2r-z1r); z5l-z6l=whatever*(z2r-z3r);
  filldraw stroke z1e--z2e--z3e; filldraw stroke z4e--z5e--z6e;
  penlabels(1,2,3,4,5,6); labels(1a,3b,2a,2b);
endchar;

%
% TO BE REVISED
%

beginchar(Dominated_curly,14u#+2appr#,v_center(spread4#+spread1#+rth#));
  "Curly dominated by sign";
  pickup tiny.nib;
  pos2(rth,-90); pos4(rth,-90);
  top y1r=top y5r=h; y2=math_axis=0.5[y1r,y3l]=0.5[y5r,y8r];
  lft x2=appr; rt x5r=rt x8r=w-appr; x5r-x1r=x8r-x3l=hround 2.5u;
  x4r=2/3[x2r,x1r]; y4r=y2r; a:=diag_width(rth,z1r-z4r);
  pos1(a,0); pos5(a,0); pos3(a,180); pos8(a,0);
  filldraw stroke z1e{z4r-z1r}...z2e{left};
  filldraw stroke z3e{z4l-z3l}...z2e{left};
%
  rt x6l=rt x7l=hround(0.5w+0.5u); y6l=y7l=good.y math_axis;
  tmp_path:=z5l{z4r-z1r}...z6l;
  z0=direction 1 of tmp_path; a:=angle z0;
  pos6(rth,a+90); pos7(rth,-90-a);
  tmp_path:=z8r{z4l-z3l}...z7r{z0 yscaled -1};
  t:=xpart(tmp_path intersectiontimes (z6l..(x5r,y6l))); 
  filldraw z5l{z4r-z1r}...z6l& z7l...z8l{z3l-z4l}
  --subpath (0,t-eps) of tmp_path
  --reverse subpath (0,t-eps) of (z5r{z4r-z1r}...z6r{z0})--cycle;
  penlabels(0,1,2,3,4,5,6,7,8);
endchar;

beginchar(Dominating_curly,14u#+2appr#,v_center(spread4#+spread1#+rth#));
  "Curly dominating sign";
  pickup tiny.nib;
  pos2(rth,90); pos4(rth,90);
  top y1l=top y5l=h; y2=math_axis=0.5[y1l,y3r]=0.5[y5l,y8l];
  rt x2=w-appr; lft x5l=lft x8l=appr; x5l-x1l=x8l-x3r=-hround 2.5u;
  x4l=2/3[x2l,x1l]; y4l=y2l; a:=diag_width(rth,z1l-z4l);
  pos1(a,0); pos5(a,0); pos3(a,180); pos8(a,0);
  filldraw stroke z1e{z4l-z1l}...z2e{right};
  filldraw stroke z3e{z4r-z3r}...z2e{right};
%
  lft x6r=lft x7r=hround(0.5w-0.5u); y6r=y7r=good.y math_axis;
  tmp_path:=z5r{z4l-z1l}...z6r;
  z0=direction 1 of tmp_path; a:=angle z0;
  pos6(rth,a+90); pos7(rth,-90-a);
  tmp_path:=z8l{z4r-z3r}...z7l{z0 yscaled -1};
  t:=xpart(tmp_path intersectiontimes (z6r..(x5l,y6r))); 
  filldraw z5r{z4l-z1l}...z6r& z7r...z8r{z3r-z4r}
  --subpath (0,t-eps) of tmp_path
  --reverse subpath (0,t-eps) of (z5l{z4l-z1l}...z6l{z0})--cycle;
  penlabels(0,1,2,3,4,5,6,7,8);
endchar;

beginpicture(tmp,12u#+2appr#,v_center(spread2#+rth#));
pickup tiny.nib;
rt x1=rt x1r=rt x3=rt x3r=w-Appr; lft x2r=appr-hround u;
x1r-x1l=x3r-x3l=rth-tiny;
y2r=y2a=y2b=good.y math_axis; y1-y2r=y2r-y3=0.5(h+d-rth);
adjust_slanted_bar(1,2r,1a,2a)(0.5(rth-tiny),-1);
adjust_slanted_bar(3,2r,3b,2b)(0.5(rth-tiny),1);
z1r=whatever[z1a,z2r]; z3r=whatever[z3b,z2r];
z1l-2z1+z1r=whatever*(z2a-z1);
z3l-2z3+z3r=whatever*(z2b-z3);
z2l-z1l=whatever*(z2b-z1);
z2l-z3l=whatever*(z2b-z3);
filldraw stroke z1e--z3e--z2e--z1e;
%  penlabels(1,2,3); labels(1a,2a,2b,3b);
numeric a; pair u_; u_=z2r-z3r; a=1/abs cosd angle u_;
endpicture;

beginchar(triangle_left,12u#+2appr#,
    v_center(spread2#+rth#));
  "Triangle left";
  currentpicture:=tmp_picture;
endchar;

beginchar(not_triangle_left,12u#+2appr#,asc_height#,asc_depth#);
  "Not triangle left";
  currentpicture:=tmp_picture;
  pickup tiny.nib;
  pos1(rth,0); pos2(rth,0);
  top y2l=h; 0.5[bot y2l,top y1l]=good.y math_axis;
  lft x1l=lft x2l=hround 0.5(w-rth);
  filldraw stroke z2e..z1e; penlabels(1,2);
endchar;

beginchar(triangle_left_eq,12u#+2appr#,
    v_center(if true_size: spread2#+rth#+a*spread1#
      else: spread2#+rth#+spread1#
      fi));
  "Triangle left equal";
  currentpicture:=tmp_picture
  shifted(0,vround(a*0.5spread1));
  pickup tiny.nib;
  penpos1((rth-tiny)*a,90);
  penpos2((rth-tiny)*a,90);
  rt x2=w-Appr; lft x1=appr-hround u; y2=-d+0.5rth; z1-z2=whatever*u_;
  filldraw stroke z1e..z2e; penlabels(1,2);
  tmp_picture:=currentpicture;
endchar;

beginchar(not_triangle_left_eq,12u#+2appr#,asc_height#,asc_depth#);
  "Not triangle left equal";
  currentpicture:=tmp_picture;
  pickup tiny.nib;
  pos1(rth,0); pos2(rth,0); bot y1l=-d; top y2l=h;
  lft x1l=lft x2l=hround 0.5(w-rth);
  filldraw stroke z2e..z1e; penlabels(1,2);
endchar;

beginpicture(tmp,12u#+2appr#,v_center(spread2#+rth#));
pickup tiny.nib;
lft x1=lft x1r=lft x3=lft x3r=Appr; rt x2r=w-appr+hround u;
x1l-x1r=x3l-x3r=rth-tiny;
y2r=y2a=y2b=good.y math_axis; y1-y2r=y2r-y3=0.5(h+d-rth);
adjust_slanted_bar(1,2r,1a,2a)(0.5(rth-tiny),1);
adjust_slanted_bar(3,2r,3b,2b)(0.5(rth-tiny),-1);
z1r=whatever[z1a,z2r]; z3r=whatever[z3b,z2r];
z1l-2z1+z1r=whatever*(z2a-z1);
z3l-2z3+z3r=whatever*(z2b-z3);
z2l-z1l=whatever*(z2b-z1);
z2l-z3l=whatever*(z2b-z3);
filldraw stroke z1e--z2e--z3e--z1e;
%  penlabels(1,2,3); labels(1a,2a,2b,3b);
numeric a; pair u_; u_=z2r-z3r; a=1/abs cosd angle u_;
endpicture;

beginchar(triangle_right,12u#+2appr#,v_center(spread2#+rth#));
  "Triangle right";
  currentpicture:=tmp_picture;
endchar;

beginchar(not_triangle_right,12u#+2appr#,asc_height#,asc_depth#);
  "Not triangle right";
  currentpicture:=tmp_picture;
  pickup tiny.nib;
  pos1(rth,0); pos2(rth,0);
  top y2l=h; 0.5[bot y2l,top y1l]=good.y math_axis;
  lft x1l=lft x2l=hround 0.5(w-rth);
  filldraw stroke z2e..z1e; penlabels(1,2);
endchar;

beginchar(triangle_right_eq,12u#+2appr#,
    v_center(if true_size:
	spread2#+rth#+a*spread1#
      else: spread2#+rth#+spread1#
      fi));
  "Triangle right equal";
  currentpicture:=tmp_picture
  shifted(0,vround(a*0.5spread1));
  pickup tiny.nib;
  penpos1((rth-tiny)*a,90);
  penpos2((rth-tiny)*a,90);
  lft x2=Appr; rt x1=w-appr+hround u; y2=-d+0.5rth; z1-z2=whatever*u_;
  filldraw stroke z2e..z1e; penlabels(1,2);
  tmp_picture:=currentpicture;
endchar;

beginchar(not_triangle_right_eq,12u#+2appr#,asc_height#,asc_depth#);
  "Not triangle right equal";
  currentpicture:=tmp_picture;
  pickup tiny.nib;
  pos1(rth,0); pos2(rth,0); bot y1l=-d; top y2l=h;
  lft x1l=lft x2l=hround 0.5(w-rth);
  filldraw stroke z2e..z1e; penlabels(1,2);
  tmp_picture:=currentpicture;
endchar;

vardef d_problem(expr origin,top_lim,side_lim,breadth)=
  save a,b,c;
  a=abs((side_lim-xpart origin)/(top_lim-ypart origin));
  b=abs(breadth/(top_lim-ypart origin));
  begingroup
    vardef f(expr c)=
      (1+a**2-2a*b*c+(b*c)**2)*(c**2)<1
    enddef;
    c=solve f(0,breadth);
  endgroup;
  breadth*(c,1+-+c)
enddef;

%%% !!!
beginchar(angle_sign,12u#+2appr#,asc_height#,0);
  "Angle sign";
  pickup tiny.nib;
  rt x1l=w-appr; lft x2l=appr; rt x3r=w-appr-hround 1.5u;
  bot y1l=bot y2l=0; top y3l=h+eps; pos1(rth,90);
  (x3r-x3l,y3l-y3r)=d_problem(z2l,y3l,x3r,rth-tiny);
  y2r=y1r; z2r-z3r=whatever*(z2l-z3l);
  filldraw stroke z1e--z2e--z3e;
  penlabels(1,2,3);
endchar;

%%% !!!
beginchar(measured_angle,12u#+2appr#,asc_height#,asc_depth#);
  "Measured angle sign";
  pickup tiny.nib;
  rt x1l=w-appr; lft x2l=appr; rt x3r=w-appr-hround 1.5u;
  bot y1l=bot y2l=0; top y3l=h+eps; pos1(rth,90);
  (x3r-x3l,y3l-y3r)=d_problem(z2l,y3l,x3r,rth-tiny);
  y2r=y1r; z2r-z3r=whatever*(z2l-z3l);
  filldraw stroke z1e--z2e--z3e;
  %
  numeric a;
  y2l=y5r; rt x5r=hround max(0.6[Appr,w-Appr]+0.5rth,x2l+0.5(h+d))+eps;
  pos5(rth,0);
  a=x5r-x2l; 0.5 y4=-d+eps; 0.5(x4-x2l)=a+-+min((0.5(y4-y2l)),a);
  0.5(z6-z2l)=a*dir min((angle(z3l-z2l)-angle(z4-z2l)),90);
  numeric t[];
  tmp_path:=halfcircle rotated -90 scaled 2(x5r-x2r) shifted z2r;
  tmpp_path:=reverse(halfcircle rotated -90 scaled 2(x5l-x2r) shifted z2r);
  t1=xpart(tmp_path intersectiontimes (z2l..z4));
  t2=xpart(tmp_path intersectiontimes (z2l..z6));
  z4r=point t1 of tmp_path; z6r=point t2 of tmp_path;
  t3=xpart(tmpp_path intersectiontimes (z2l..z6));
  t4=xpart(tmpp_path intersectiontimes (z2l..z4));
  z4l=point t4 of tmpp_path; z6l=point t3 of tmpp_path;
  filldraw subpath (t1,t2) of tmp_path
  --subpath (t3,t4) of tmpp_path--cycle;
  penlabels(1,2,3,4,5,6);
endchar;

%%% !!!
beginchar(spherical_angle,arithmetic_bounds);
  "Spherical angle sign";
  pickup tiny.nib;
  % < part
  y2r=0.5[y1,y3]=good.y math_axis; y1-y3=spread4;
  rt x1=w-Appr; lft x2r=Appr; x1=x1r=x3=x3r;
  adjust_slanted_bar(2r,1,2a,1a)(0.5(rth-tiny),-1);
  adjust_slanted_bar(2r,3,2b,3b)(0.5(rth-tiny),1);
  z1r=whatever[z2r,z1a]; z3r=whatever[z2r,z3b];
  z1r-z1=z1-z1l; z3r-z3=z3-z3l;
  z2l-z1l=whatever*(z2r-z1r); z2l-z3l=whatever*(z2r-z3r);
  filldraw stroke z3e--z2e--z1e;
  % ) part
  y2r=y5r; rt x5r=hround max(0.6[Appr,w-Appr]+0.5rth,x2r+0.5(h+d))+eps;
  top y6=h+eps; y6-y2r=y2r-y4; pos5(rth,0);
  numeric t[];
  tmp_path:=halfcircle rotated -90 scaled 2(x5r-x2r) shifted z2r;
  tmpp_path:=reverse(halfcircle rotated -90 scaled 2(x5l-x2r) shifted z2r);
  t1=xpart(tmp_path intersectiontimes ((0,y4)..(w,y4)));
  t2=xpart(tmp_path intersectiontimes ((0,y6)..(w,y6)));
  z4r=point t1 of tmp_path; z6r=point t2 of tmp_path;
  t3=xpart(tmpp_path intersectiontimes (z2r..z6r));
  t4=xpart(tmpp_path intersectiontimes (z2r..z4r));
  z4l=point t4 of tmpp_path; z6l=point t3 of tmpp_path;
  filldraw subpath (t1,t2) of tmp_path
  --subpath (t3,t4) of tmpp_path--cycle;
  penlabels(1,2,3,4,5,6);
endchar;

beginchar(between_sign,7u#+2appr#,body_height#,paren_depth#);
  "Between sign";
  pickup tiny.nib;
  pos2(hround 0.75[hair,stem],0); pos5(hround 0.75[hair,stem],0);
  top y1l=top y4r=h+eps; bot y3l=bot y6r=-d-eps;
  y0r=y0l=y2=y5=math_axis;
  rt x1r=rt x3r=rt x5r+hround 0.75u=w-appr;
  lft x4l=lft x6l=lft x2l-hround 0.75u=appr;
  x2l-x0l=x0r-x5r=x5r-x2l;
  (x1r-x1l,y1l-y1r)=(x3r-x3l,y3r-y3l)
  =(x4r-x4l,y4r-y4l)=(x6r-x6l,y6l-y6r)
  =d_problem(z0l,y1l,x1r,max(0,vair-tiny));
  filldraw stroke z1e{z0l-z1l}..z2e..z3e{z3l-z0l};
  filldraw stroke z4e{z0r-z4r}..z5e..z6e{z6r-z0r};
  penlabels(1,2,3,4,5,6);
endchar;

%%% !!!
beginchar(times_left_three,arithmetic_bounds);
  "Left three times sign";
  pickup tiny.nib;
  top y1l=top y3r=h; bot y2r=bot y4l=-d;
  lft x1l=lft x4l=appr; rt x2r=rt x3r=w-appr;
  adjust_slanted_bar(1l,2r,1r,2l)(rth-tiny,1);
  adjust_slanted_bar(3r,4l,3l,4r)(rth-tiny,-1);
  z1=0.5[z1l,z1r]; z2=0.5[z2l,z2r];
  forsuffixes $=r,l: z5$=whatever[z1,z2];
    z5$=whatever[z3$,z4$]; endfor;
  filldraw stroke z1e..z2e; filldraw stroke z5e..z4e;
  penlabels(1,2,3,4,5);
endchar;

%%% !!!
beginchar(times_right_three,arithmetic_bounds);
  "Right three times sign";
  pickup tiny.nib;
  top y1l=top y3r=h; bot y2r=bot y4l=-d;
  lft x1l=lft x4l=appr; rt x2r=rt x3r=w-appr;
  adjust_slanted_bar(1l,2r,1r,2l)(rth-tiny,1);
  adjust_slanted_bar(3r,4l,3l,4r)(rth-tiny,-1);
  z3=0.5[z3l,z3r]; z4=0.5[z4l,z4r];
  forsuffixes $=r,l: z5$=whatever[z3,z4];
    z5$=whatever[z1$,z2$]; endfor;
  filldraw stroke z3e..z4e; filldraw stroke z5e..z2e;
  penlabels(1,2,3,4,5);
endchar;

beginchar(pitchfork_sign,12u#+2appr#,asc_height#,0);
  "Small cap sign";
  ensure_centering_of(rth);
  pickup tiny.nib;
  pos1(rth,180); pos2(rth,180);
  pos4(rth,0); pos5(rth,0); pos6(rth,0); pos7(rth,0);
  y3+0.5rth=x_height+o; bot y1r=bot y5r=bot y7+o=-d;
  top y6=h; y2=y4=2/3[y3,y1r];
  lft x1r=w-rt x5r=appr+hround 0.8u;
  x1=x2; x4=x5; x3=x6=x7=0.5w;
  filldraw stroke z1e..z2e; filldraw stroke z4e..z5e;
  filldraw stroke z6e..z7e;
  pickup rule.nib; autorounded;
  draw z2 up_to_right z3 right_to_down z4;
  penlabels(1,2,3,4,5,6,7);
endchar;

beginchar(smile_sign,16u#+2appr#,v_center(0.5x_height#));
  "Smile sign";
  pickup tiny.nib;
  a:=vround 0.5[vair,stem]; pos2(a,90);
  y2-0.5a=vround(-d-0.5a); y1l=y3l=good.y h;
  lft x1l=appr; rt x3l=w-appr; x2=0.5[x1l,x3l];
  z1'-z1l=(z2l-z1l) xscaled 1/3;
  z3'-z3l=(z2l-z3l) xscaled 1/3;
  pos1(hair,angle(z1'-z1l)+90);
  pos3(hair,angle(z3'-z3l)-90);
  filldraw stroke z1e{z1'-z1l}...z2e{right}...z3e{z3l-z3'};
  penlabels(1,2,3); labels(1',3');
endchar;

beginchar(frown_sign,16u#+2appr#,v_center(0.5x_height#));
  "Frown sign";
  pickup tiny.nib;
  a:=vround 0.5[vair,stem]; pos2(a,90);
  y2+0.5a=vround(h+0.5a); y1r=y3r=good.y -d;
  lft x1r=appr; rt x3r=w-appr; x2=0.5[x1r,x3r];
  z1'-z1r=(z2r-z1r) xscaled 1/3;
  z3'-z3r=(z2r-z3r) xscaled 1/3;
  pos1(hair,angle(z1'-z1r)+90);
  pos3(hair,angle(z3'-z3r)-90);
  filldraw stroke z1e{z1'-z1r}...z2e{right}...z3e{z3r-z3'};
  penlabels(1,2,3); labels(1',3');
endchar;