<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=utf-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    Thank you for your help.
    <p>Why Agda refuses the following  structurally decreasing function?
      <br>
    </p>
    foldl″ : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A<br>
    foldl″ c (n ∷ []) = n<br>
    foldl″ c (n ∷ (x ∷ xs)) = foldl″ c (c n x ∷ xs)<br>
    <br>
    <span style="color: rgb(157, 165, 180); font-family: inconsolata, Menlo, Consolas, "DejaVu Sans Mono", "Liberation Mono", Monaco, "Lucida Console", monospace; font-size: 15px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; line-height: 30px; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: pre-wrap; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; display: inline !important; float: none; background-color: rgb(33, 37, 43);">/home/serge/agda/Maximal.agda:47,1-49,50
Termination checking failed for the following functions:
  foldl″
Problematic calls:
  foldl″ c (c n x ∷ xs)
    (at /home/serge/agda/Maximal.agda:49,27-33)</span><br>
    <br>
    <div class="moz-cite-prefix">On 2017-08-14 20:55, Ulf Norell wrote:<br>
    </div>
    <blockquote type="cite"
cite="mid:CAJjNqYF=GadEsT3zEjseAc7ChhqkVF_MZBkjUphtBZB6yzmK3g@mail.gmail.com">
      <div dir="ltr">The fact that <span style="font-size:12.8px">foldr₁</span> is
        using a private recursive helper function will likely make it
        impossible to prove your theorem.
        <div><br>
        </div>
        <div>/ Ulf</div>
      </div>
      <div class="gmail_extra"><br>
        <div class="gmail_quote">On Mon, Aug 14, 2017 at 6:47 PM, Jesper
          Cockx <span dir="ltr"><<a href="mailto:Jesper@sikanda.be"
              target="_blank" moz-do-not-send="true">Jesper@sikanda.be</a>></span>
          wrote:<br>
          <blockquote class="gmail_quote" style="margin:0 0 0
            .8ex;border-left:1px #ccc solid;padding-left:1ex">
            <div dir="ltr">
              <div>
                <div>
                  <div>Maybe you can explain what approaches you have
                    already tried and why you got stuck? I think people
                    would be more inclined to help that way.<br>
                    <br>
                  </div>
                  To get you started on proof1, here's a hint: since you
                  are proving something about the functions foldr₁ and
                  _⊔_, you can take a look at their definitions and
                  follow the same structure for your proof. For example,
                  since foldr₁ is defined in terms of the helper
                  function foldr, you probably also need to define a
                  helper lemma that proves a similar statement about
                  foldr.<br>
                  <br>
                </div>
                Best regards,<br>
              </div>
              Jesper<br>
            </div>
            <div class="gmail_extra"><br>
              <div class="gmail_quote">
                <div>
                  <div class="h5">2017-08-14 18:33 GMT+02:00 Serge
                    Leblanc <span dir="ltr"><<a
                        href="mailto:33dbqnxpy7if@gmail.com"
                        target="_blank" moz-do-not-send="true">33dbqnxpy7if@gmail.com</a>></span>:<br>
                  </div>
                </div>
                <blockquote class="gmail_quote" style="margin:0 0 0
                  .8ex;border-left:1px #ccc solid;padding-left:1ex">
                  <div>
                    <div class="h5">
                      <div text="#000000" bgcolor="#FFFFFF">
                        <p>Saluton, neniu bonvolas helpi min?<br>
                        </p>
                        <p>Hi, nobody wants to help me?<br>
                        </p>
                        <div>
                          <div class="m_-5624432948826885329h5"> <br>
                            <div
                              class="m_-5624432948826885329m_-5308586550852440085moz-cite-prefix">On
                              2017-08-06 18:23, Serge Leblanc wrote:<br>
                            </div>
                            <blockquote type="cite"> <span
                                id="m_-5624432948826885329m_-5308586550852440085result_box"
                                lang="en"><span>Dear All,</span><br>
                                <span>I need help to finish these
                                  lemmas.</span><br>
                                <span>They have the same meaning, I am
                                  right?</span><br>
                                <span>All helpers are welcome!</span></span><br>
                              <br>
                              Estimata ĉiuj, <br>
                              Mi bezonas helpon por daŭrigi ci-tiuj
                              pruvojn!<br>
                              <div
                                class="m_-5624432948826885329m_-5308586550852440085moz-signature">Ĉu
                                ili havas je la saman signifon! Ĉu mi
                                pravas?<br>
                                Ĉiuj helpantoj estas bonvenaj!<br>
                                <br>
                                Sincere.<br>
                                -- <br>
                                Serge Leblanc
                                <hr> gpg --search-keys 0x67B17A3F <br>
                                Fingerprint = 2B2D AC93 8620 43D3 D2C2
                                C2D3 B67C F631 67B1 7A3F</div>
                            </blockquote>
                            <br>
                            <div
                              class="m_-5624432948826885329m_-5308586550852440085moz-signature">--
                              <br>
                              Serge Leblanc
                              <hr> gpg --search-keys 0x67B17A3F <br>
                              Fingerprint = 2B2D AC93 8620 43D3 D2C2
                              C2D3 B67C F631 67B1 7A3F</div>
                          </div>
                        </div>
                      </div>
                      <br>
                    </div>
                  </div>
                  ______________________________<wbr>_________________<br>
                  Agda mailing list<br>
                  <a href="mailto:Agda@lists.chalmers.se"
                    target="_blank" moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
                  <a
                    href="https://lists.chalmers.se/mailman/listinfo/agda"
                    rel="noreferrer" target="_blank"
                    moz-do-not-send="true">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
                  <br>
                </blockquote>
              </div>
              <br>
            </div>
            <br>
            ______________________________<wbr>_________________<br>
            Agda mailing list<br>
            <a href="mailto:Agda@lists.chalmers.se"
              moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
            <a href="https://lists.chalmers.se/mailman/listinfo/agda"
              rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
            <br>
          </blockquote>
        </div>
        <br>
      </div>
    </blockquote>
    <br>
    <div class="moz-signature">-- <br>
      Serge Leblanc
      <hr>
      gpg --search-keys 0x67B17A3F
      <br>
      Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F</div>
  </body>
</html>