mailing-list for TeXmacs Users

["Yin Wang" <address@hidden>]

Hi,

Why is \overline's appear so thick and ugly in my PDF files? I
attached an example. I wonder if there is a way to tune this?


--
Yin Wang
<TeXmacs|1.0.6.6>

<style|generic>

<\body>
  <section|Problem 1>

  First we formulate the two programs into KAT.

  <\code>
    while <with|mode|math|b> do {

    \ \ \ <with|mode|math|p>;\ 

    \ \ \ while <with|mode|math|c> do <with|mode|math|q>

    }
  </code>

  can be expressed as

  <\equation>
    (b p (c q)<rsup|\<ast\>><overline|c> )<rsup|\<ast\>> <overline|b><rsup|*>
    \ \ \ \ <label|while>
  </equation>

  and

  <\code>
    if <with|mode|math|b> then {

    \ \ \ \ <with|mode|math|p>;

    \ \ \ \ while <with|mode|math|b\<vee\>c> do {

    \ \ \ \ \ \ \ \ if <with|mode|math|c> then <with|mode|math|q> else
    <with|mode|math|p>

    \ \ \ \ }

    }
  </code>

  can be expressed as

  <\equation>
    b p ((b+c) (c q+<overline|c> p))<rsup|\<ast\>>
    <overline|b+c>+<overline|b> \ \ \ <label|trans>
  </equation>

  Because <with|mode|math|<overline|b+c>=<overline|c> <overline|b>> and

  <\eqnarray*>
    <tformat|<table|<row|<cell|(b+c) (c q+<overline|c> p)>|<cell|=>|<cell|b c
    q+b <overline|c> p+c c q + c <overline|c>
    p>>|<row|<cell|>|<cell|=>|<cell|b c q+b <overline|c> p+c
    q>>|<row|<cell|>|<cell|=>|<cell|(b+1) c q+b <overline|c>
    p>>|<row|<cell|>|<cell|=>|<cell|c q+ <overline|c> b p,>>>>
  </eqnarray*>

  (<reference|trans>) can be transformed into

  <\equation>
    b p (c q+ <overline|c> b p)<rsup|\<ast\>> <overline|c>
    <overline|b>+<overline|b> \ <label|final1>
  </equation>

  Then we use the rule <math|1+p p<rsup|\<ast\>>=p<rsup|\<ast\>>> on
  (<reference|while>). We get

  <\eqnarray*>
    <tformat|<table|<row|<cell|(b p (c q)<rsup|\<ast\>><overline|c>
    )<rsup|\<ast\>> <overline|b><rsup|*> >|<cell|=>|<cell|(1+(b p (c
    q)<rsup|\<ast\>><overline|c> ) (b p (c q)<rsup|\<ast\>><overline|c>
    )<rsup|\<ast\>>) <overline|b><rsup|*> \ >>|<row|<cell|>|<cell|=>|<cell|b
    p (c q)<rsup|\<ast\>><with|color|red|<overline|c> \ (b p (c
    q)<rsup|\<ast\>><overline|c> )<rsup|\<ast\>>> <overline|b><rsup|*>
    \ +<overline|b><rsup|*> <label|slide><eq-number>>>>>
  </eqnarray*>

  This transformation correspond to loop unwinding operation, which turns the
  original program into

  <\code>
    if <with|mode|math|b> then {<with|mode|math|p>; while <with|mode|math|c>
    do <with|mode|math|q>;

    \ \ \ \ \ \ \ \ \ \ \ \ while <with|mode|math|b> do {

    \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ <with|mode|math|p>;\ 

    \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ while <with|mode|math|c> do
    <with|mode|math|q>

    \ \ \ \ \ \ \ \ \ \ \ \ }

    }
  </code>

  Now we can see that <with|mode|math|p (q \ p)<rsup|\<ast\>>=(p
  q)<rsup|\<ast\>> p> may be applied on part in red in (4). We apply it and
  get

  <\equation*>
    b p <with|color|red|(c q)<rsup|\<ast\>>(<overline|c> \ b p (c
    q)<rsup|\<ast\>>)<rsup|\<ast\>>><overline|c> \ <overline|b><rsup|*>
    \ +<overline|b><rsup|*>\ 
  </equation*>

  We see that we can apply this rule once more and get

  <\equation*>
    b p<with|color|red| ((c q)<rsup|\<ast\>><overline|c> \ b p)<rsup|\<ast\>>
    (c q)<rsup|\<ast\>>><overline|c> \ <overline|b><rsup|*>
    \ +<overline|b><rsup|*>\ 
  </equation*>

  Now we can see the rule <with|mode|math|(p<rsup|*\<ast\>>q)<rsup|\<ast\>>p<rsup|\<ast\>>=(p+q)<rsup|\<ast\>>>
  can be applied to the red part with substitutions <with|mode|math|p=c q>
  and <with|mode|math|q=><with|mode|math|<overline|c> \ b p>. Apply it and we
  get

  <\equation*>
    b p<with|color|red| (c q+<overline|c> \ b p)<rsup|\<ast\>>> <overline|c>
    \ <overline|b><rsup|*> \ +<overline|b><rsup|*>\ 
  </equation*>

  which equals (<reference|final1>). This proves the programs are equal.
</body>

<\references>
  <\collection>
    <associate|auto-1|<tuple|1|?>>
    <associate|final1|<tuple|3|?>>
    <associate|slide|<tuple|3|?>>
    <associate|trans|<tuple|2|?>>
    <associate|while|<tuple|1|?>>
  </collection>
</references>

<\auxiliary>
  <\collection>
    <\associate|toc>
      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|Problem
      1> <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
      <no-break><pageref|auto-1><vspace|0.5fn>
    </associate>
  </collection>
</auxiliary>

Attachment: over.pdf
Description: Adobe PDF document