[Rodin-b-sharp-user] General advice on finiteness proofs

SourceForge Headquarters 225 Broadway Suite 1600 San Diego, CA 92101 +1 (858) 454-5900

<html>
  <head>

    <meta http-equiv="content-type" content="text/html; charset=utf-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    Hi,<br>
    <br>
    It seems given `x &lt;: y &amp; finite(y)` Rodin provers cant
    automatically prove `finite(x)`, let alone where we have is a some
    sort of relation, function, restriction/substraction related to x
    where the finiteness of said is obviously implied by finiteness of
    x. Is this right? Is there any general advice available on whats
    going on, why, and how to proceed manually? I know there are some
    threads about related finite() things not discharging when they
    should but I can't read these and understand why, and how to fix in
    general.<br>
    <br>
    As an example, the following machine is a cut down version of the
    situation I have in a more complicated machine I'm trying to write,
    where I noticed the issue. inv6 wont discharge. Note if I change the
    "theorems" to "not theorems" everythin discharges, but that is not
    fixing the issue.<br>
    <br>
        CONTEXT<br>
            ctx     ›<br>
        SETS<br>
        ⚬    FOO    <br>
        ⚬    BAH    <br>
        AXIOMS<br>
        ⚬    axm2:    finite(FOO) not theorem<br>
        ⚬    axm3:    finite(BAH) not theorem<br>
        END<br>
    <br>
    MACHINE<br>
            mchn     ›<br>
        SEES<br>
        ⚬     ctx <br>
        VARIABLES<br>
        ⚬    f    <br>
        ⚬    g    <br>
        ⚬    x    <br>
        INVARIANTS<br>
        ⚬    inv1:    f ⊆ FOO not theorem<br>
        ⚬    inv2:    finite(f) theorem<br>
        ⚬    inv3:    g ⊆ BAH not theorem<br>
        ⚬    inv4:    finite(g) theorem<br>
        ⚬    inv5:    x ∈ f ⇸ g not theorem<br>
        ⚬    inv6:    finite(x) theorem<br>
        EVENTS<br>
        ⚬    INITIALISATION:     not extended ordinary<br>
            THEN<br>
            ⚬    act1:    f ≔ ∅<br>
            ⚬    act2:    g ≔ ∅<br>
            ⚬    act3:    x ≔ ∅<br>
            END<br>
        END<br>
    <br>
    Thanks,<br>
    <br>
    Sam.<br>
     <br>
    <div class="moz-signature">-- <br>
      <p style="color:#CCC; font-size:small"><strong>PGP</strong>:
        0xA53455C1</p>
    </div>
  </body>
</html>