1:- encoding(utf8).
    2
    3atom_st(X, Y):- dcg_st(X0, Y0, []),  X0 =[_|X1],
    4	maplist(atom_codes, [X, Y], [X1, Y0]).
    5%%
    6ts_atom(in, '∈').
    7ts_atom(subseteq, '⊆').
    8ts_atom(neg, '¬').
    9ts_atom(ne, '≠').
   10ts_atom(not, '¬').
   11ts_atom(alpha, 'α').
   12ts_atom(beta, 'β').
   13ts_atom(sigma, 'σ').
   14ts_atom('Sigma', 'Σ').
   15ts_atom(cup, '∪').
   16ts_atom(cap, '∩').
   17ts_atom('Gamma', 'Γ').
   18ts_atom(gamma, 'γ').
   19ts_atom('Psi', 'Ψ').
   20ts_atom(psi, 'ψ').
   21ts_atom('Omega', 'Ω').
   22ts_atom(omega, 'ω').
   23ts_atom('Delta', 'Δ').
   24ts_atom(delta, 'δ').
   25ts_atom(varepsilon, 'ε').
   26ts_atom(emptyset, 'φ').
   27ts_atom('Phi', 'Φ').
   28ts_atom(phi, φ).
   29ts_atom('Lambda', 'Λ').
   30ts_atom(lambda, 'λ').
   31ts_atom('Pi', 'Π').
   32ts_atom(pi, 'π').
   33ts_atom(iota, 'ι').
   34ts_atom(eta, 'η').
   35ts_atom(kappa, 'κ').
   36ts_atom(sim, '〜').
   37ts_atom(times, '×').
   38ts_atom('To', '⇒').
   39ts_atom(to, '→').
   40ts_atom(to, (-->)).
   41ts_atom(to, (->)).
   42ts_atom(forall, '∀').
   43ts_atom(exists, '∃').
   44ts_atom(land, '∧').
   45ts_atom(lor, '∨').
   46ts_atom(iff, '⇔').
   47ts_atom(equiv, '≡').
   48ts_atom(vdash, '|-').
   49ts_atom(mid, ('|')).
   50ts_atom(bot, '⊥').
   51ts_atom(xi, 'ξ').
   52ts_atom('Xi', 'Ξ').
   53ts_atom(because, '∵').
   54ts_atom(therefore, '∴').
   55ts_atom(aleph, 'ℵ').
   56ts_atom(otimes, '⊗').
   57ts_atom(oplus, '⊕').
   58ts_atom(infty, '∞').
   59ts_atom(cong, '≅').
   60ts_atom(simeq, '≃').
   61ts_atom(partial, '∂').
   62
   63
   64%%%%%
   65punct(`．`) --> `。`.
   66punct(`，`) --> `、`.
   67punct(` `) --> `　`.
   68
   69%%%%%%
   70punct_opp(`。`) --> `．`.
   71punct_opp(`、`) --> `，`.
   72
   73%%%%%%
   74dcg_st(`\\in`) --> `∈`.
   75dcg_st(`\\subseteq`) --> `⊆`.
   76dcg_st(`\\neg`) --> `¬`.
   77dcg_st(`\\neg`) --> `¬`.
   78dcg_st(`\\ne`) --> `≠`.
   79dcg_st(`\\alpha`) --> `α`.
   80dcg_st(`\\beta`) --> `β`.
   81dcg_st(`\\sigma`) --> `σ`.
   82dcg_st(`\\Sigma`) --> `Σ`.
   83dcg_st(`\\cup`) --> `∪`.
   84dcg_st(`\\cap`) --> `∩`.
   85dcg_st(`\\Gamma`) --> `Γ`.
   86dcg_st(`\\gamma`) --> `γ`.
   87dcg_st(`\\Psi`) --> `Ψ`.
   88dcg_st(`\\psi`) --> `ψ`.
   89dcg_st(`\\Omega`) --> `Ω`.
   90dcg_st(`\\omega`) --> `ω`.
   91dcg_st(`\\Delta`) --> `Δ`.
   92dcg_st(`\\delta`) --> `δ`.
   93dcg_st(`\\varepsilon`) --> `ε`.
   94dcg_st(`\\emptyset`) --> `φ`.
   95dcg_st(`\\Phi`) --> `Φ`.
   96dcg_st(`\\phi`) --> `φ`.
   97dcg_st(`\\Lambda`) --> `Λ`.
   98dcg_st(`\\lambda`) --> `λ`.
   99dcg_st(`\\Pi`) --> `Π`.
  100dcg_st(`\\pi`) --> `π`.
  101dcg_st(`\\iota`) --> `ι`.
  102dcg_st(`\\eta`) --> `η`.
  103dcg_st(`\\kappa`) --> `κ`.
  104dcg_st(`\\sim`) --> `〜`.
  105dcg_st(`\\times`) --> `×`.
  106dcg_st(`\\To`) --> `⇒`.
  107dcg_st(`\\to`) --> `→`.
  108dcg_st(`\\to`) --> `-->`.
  109dcg_st(`\\to`) --> `->`.
  110dcg_st(`\\forall`) --> `∀`.
  111dcg_st(`\\exists`) --> `∃`.
  112dcg_st(`\\land`) --> `∧`.
  113dcg_st(`\\lor`) --> `∨`.
  114dcg_st(`\\iff`) --> `⇔`.
  115dcg_st(`\\equiv`) --> `≡`.
  116dcg_st(`\\vdash`) --> `|-`.
  117dcg_st(`\\mid`) --> `|`.
  118dcg_st(`\\bot`) --> `⊥`.
  119dcg_st(`\\because`) --> `∵`.
  120dcg_st(`\\aleph`) --> `ℵ`.
  121dcg_st(`\\partial`) --> `∂`.
  122dcg_st(`\\xi`) --> `ξ`.
  123dcg_st(`\\Xi`) --> `Ξ`.
  124
  125%%%%%%%%%% TeX ==> Japanese Kanji
  126dcg_ts(`∵`) --> `\\because`.
  127dcg_ts(`∈`) --> `\\in`.
  128dcg_ts(`⊆`) --> `\\subseteq`.
  129dcg_ts(`¬`) --> `\\neg`.
  130dcg_ts(`¬`) --> `\\not`.
  131dcg_ts(`≠`) --> `\\ne`.
  132dcg_ts(`α`) --> `\\alpha`.
  133dcg_ts(`β`) --> `\\beta`.
  134dcg_ts(`σ`) --> `\\sigma`.
  135dcg_ts(`Σ`) --> `\\Sigma`.
  136dcg_ts(`∪`) --> `\\cup`.
  137dcg_ts(`∩`) --> `\\cap`.
  138dcg_ts(`Γ`) --> `\\Gamma`.
  139dcg_ts(`γ`) --> `\\gamma`.
  140dcg_ts(`Ψ`) --> `\\Psi`.
  141dcg_ts(`ψ`) --> `\\psi`.
  142dcg_ts(`Ω`) --> `\\Omega`.
  143dcg_ts(`ω`) --> `\\omega`.
  144dcg_ts(`Δ`) --> `\\Delta`.
  145dcg_ts(`δ`) --> `\\delta`.
  146dcg_ts(`ε`) --> `\\varepsilon`.
  147dcg_ts(`φ`) --> `\\emptyset`.
  148dcg_ts(`Φ`) --> `\\Phi`.
  149dcg_ts(`φ`) --> `\\phi`.
  150dcg_ts(`Λ`) --> `\\Lambda`.
  151dcg_ts(`λ`) --> `\\lambda`.
  152dcg_ts(`Π`) --> `\\Pi`.
  153dcg_ts(`π`) --> `\\pi`.
  154dcg_ts(`ι`) --> `\\iota`.
  155dcg_ts(`η`) --> `\\eta`.
  156dcg_ts(`κ`) --> `\\kappa`.
  157dcg_ts(`〜`) --> `\\sim`.
  158dcg_ts(`×`) --> `\\times`.
  159dcg_ts(`→`) --> `\\to`.
  160dcg_ts(`-->`) --> `\\to`.
  161dcg_ts(`->`) --> `\\to`.
  162dcg_ts(`∀`) --> `\\forall`.
  163dcg_ts(`∃`) --> `\\exists`.
  164dcg_ts(`∧`) --> `\\land`.
  165dcg_ts(`∨`) --> `\\lor`.
  166dcg_ts(`⇔`) --> `\\iff`.
  167dcg_ts(`⇒`) --> `\\To`.
  168dcg_ts(`≡`) --> `\\equiv`.
  169dcg_ts(`|-`) --> `\\vdash`.
  170dcg_ts(`|`) --> `\\mid`.
  171dcg_ts(`⊥`) --> `\\bot`.
  172dcg_ts(`ℵ`) --> `\\aleph`.
  173dcg_ts(`∂`) --> `\\partial`.
  174dcg_ts(`≃`) --> `\\simeq`.
  175dcg_ts(`≅`) --> `\\cong`.
  176dcg_ts(`ξ`)--> `\\xi`. 
  177dcg_ts(`Ξ`)--> `\\Xi`