<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=utf-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    <p><span id="result_box" class="" lang="en"><span class="">Dear, I
          succeeded completing the proof1: ∀ xs → All (_≥_ (max "xs))
          (toList xs)" using "tabulate".</span> <span class=""></span></span><span
        id="result_box" class="" lang="en"><span class=""></span></span><span
        id="result_box" class="" lang="en"><span class=""></span></span><span
        id="result_box" class="" lang="en"><span class="">Can anyone
          show me a simple method?</span></span></p>
    <p><span id="result_box" class="short_text" lang="en"><span class="">Sincerely
          thank you,</span></span><br>
    </p>
    <p>Estimata, mi sukcesis plenumi pruvon "proof₁′ : ∀ xs → All (_≥_
      (max″ xs)) (toList xs)" per uzado de 'tabulate'. Ĉu ekzistas pli
      simpla metodo ?<br>
    </p>
    Sinceran dankon,<br>
    <br>
    <font color="#000099">proof₁′ : ∀ xs → All (_≥_ (max″ xs)) (toList
      xs)<br>
      proof₁′ (h ∷ t) = tabulate helper   <br>
        where<br>
          helper′ : ∀ {x xs}  → x ∈ xs → (∀ x₀ → max″ (x₀ ∷ xs) ≥ x) <br>
          helper′ {x} (here {x′} {xs′} px) x₀ = begin<br>
            x ≤⟨ lemma₄ (x₀ ∷ xs′)  x ⟩<br>
            Data.List.foldl _⊔_ (x ⊔ x₀) xs′ ≡⟨ cong (λ s →
      Data.List.foldl _⊔_ s xs′) (⊔-comm x x₀) ⟩<br>
            Data.List.foldl _⊔_ (x₀ ⊔ x) xs′ ≡⟨ cong (λ s →
      Data.List.foldl _⊔_ (x₀ ⊔ s) xs′) px ⟩<br>
            Data.List.foldl _⊔_ (x₀ ⊔ x′) xs′<br>
            ∎<br>
            where open Data.Nat.≤-Reasoning<br>
          helper′ {x} (there {x′} {xs′} pxs) x₀ = helper′ pxs (x₀ ⊔ x′)<br>
      <br>
          helper : {x : ℕ} → x ∈ (h ∷ t) → max″ (h ∷ t) ≥ x<br>
          helper {x} (here px) = begin<br>
            x ≡⟨ px ⟩<br>
            h ≤⟨ lemma₄ t h ⟩<br>
            max″ (h ∷ t)<br>
            ∎<br>
            where open Data.Nat.≤-Reasoning<br>
          helper {x} (there pxs) = (helper′ pxs h)</font><br>
    <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>