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