<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=utf-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    <p>Bedaŭrinde, tio maltrafas.  Agda ne vidas la malkreskanton de la
      listo malgraŭ la ampleksa ordono eĉ ĝis 15 !<br>
    </p>
    <span id="result_box" class="" lang="en"><span class="">Unfortunately
        this fails, Agda doesn't see the descent of the list despite the
        command even up to 15 !</span></span><span id="result_box"
      class="" lang="en"><span class=""><br>
        <br>
        Sincere,<br>
        <br>
      </span></span>
    <div class="moz-cite-prefix">On 2017-08-16 22:53, Sergei Meshveliani
      wrote:<br>
    </div>
    <blockquote type="cite"
      cite="mid:1502916835.4258.5.camel@one.mechvel.pereslavl.ru">
      <pre wrap="">I would try to call  
               agda --termination-depth=2 Foo.agda  

Maybe, this will help Agda to see that  (x ∷ xs)  is less than 
(n ∷ (x ∷ xs)).

------
Sergei


On Wed, 2017-08-16 at 22:23 +0200, Serge Leblanc wrote:
</pre>
      <blockquote type="cite">
        <pre wrap="">Thank you for your help. 

Why Agda refuses the following  structurally decreasing function? 


foldl″ : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A
foldl″ c (n ∷ []) = n
foldl″ c (n ∷ (x ∷ xs)) = foldl″ c (c n x ∷ xs)

/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)

On 2017-08-14 20:55, Ulf Norell wrote:

</pre>
        <blockquote type="cite">
          <pre wrap="">The fact that foldr₁ is using a private recursive helper function
will likely make it impossible to prove your theorem. 


/ Ulf

On Mon, Aug 14, 2017 at 6:47 PM, Jesper Cockx <a class="moz-txt-link-rfc2396E" href="mailto:Jesper@sikanda.be"><Jesper@sikanda.be></a>
wrote:
        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.
        
        
        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.
        
        
        Best regards,
        
        Jesper
        
        
        2017-08-14 18:33 GMT+02:00 Serge Leblanc
        <a class="moz-txt-link-rfc2396E" href="mailto:33dbqnxpy7if@gmail.com"><33dbqnxpy7if@gmail.com></a>:
        
                Saluton, neniu bonvolas helpi min?
                
                
                Hi, nobody wants to help me?
                
                
                
                On 2017-08-06 18:23, Serge Leblanc wrote:
                
                > Dear All,
                > I need help to finish these lemmas.
                > They have the same meaning, I am right?
                > All helpers are welcome!
                > 
                > Estimata ĉiuj, 
                > Mi bezonas helpon por daŭrigi ci-tiuj pruvojn!
                > Ĉu ili havas je la saman signifon! Ĉu mi pravas?
                > Ĉiuj helpantoj estas bonvenaj!
                > 
                > Sincere.
                > -- 
                > Serge Leblanc 
                > __________________________________________________
                > gpg --search-keys 0x67B17A3F 
                > Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C
                > F631 67B1 7A3F
                
                -- 
                Serge Leblanc 
                ____________________________________________________
                gpg --search-keys 0x67B17A3F 
                Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C
                F631 67B1 7A3F
                
                
                _______________________________________________
                Agda mailing list
                <a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
                <a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
                
        
        
        
        _______________________________________________
        Agda mailing list
        <a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
        <a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
        


</pre>
        </blockquote>
        <pre wrap="">
-- 
Serge Leblanc 
______________________________________________________________________
gpg --search-keys 0x67B17A3F 
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
      </blockquote>
      <pre wrap="">

</pre>
    </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>