[Generalised some results.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20090106183321] hunk ./StatusLemmas.agda 50
--- However, the other direction is not valid, not even in a total
--- setting with a non-exceptional end result.
+-- However, the other direction is not valid.
hunk ./StatusLemmas.agda 52
-¬UtoB : ¬ (∀ (x : Expr total) {n} → x ⇓[ U ] nat n → x ⇓[ B ] nat n)
-¬UtoB UtoB with UtoB (⌜ nat 0 ⌝ catch ⌜ nat 1 ⌝) (Catch₂ Int Val)
-... | Catch₁ ()
-... | Catch₂ () _
+¬UtoB : ∀ t v → ∃ λ (x : Expr t) → x ⇓[ U ] v × ¬ (x ⇓[ B ] v)
+¬UtoB t v = (x , Catch₂ Int Val , helper)
+  where
+  v′ : Value
+  v′ with v
+  ... | nat 0 = nat 1
+  ... | _     = nat 0
hunk ./StatusLemmas.agda 60
--- Furthermore, in a partial setting the following even more limited
--- variant is also invalid.
+  x : Expr t
+  x = ⌜ v′ ⌝ catch ⌜ v ⌝
hunk ./StatusLemmas.agda 63
-¬UtoB' : ¬ (∀ (x : Expr partial) → x ↡[ U ] → x ↡[ B ])
-¬UtoB' UtoB'
-  with UtoB' (loop ⌜ nat 0 ⌝ catch ⌜ nat 0 ⌝) (0 , Catch₂ Int Val)
-... | (n , Catch₁ ⇓)                    = loop-¬⇓ nat-¬↯ (nat n , ⇓)
-... | (n , Catch₂ (Loop (Seqn₁ _ ↯)) _) = loop-¬⇓ nat-¬↯ (throw , ↯)
-... | (n , Catch₂ (Loop (Seqn₂ ())) _)
+  helper : ¬ (x ⇓[ B ] v)
+  helper x⇓ with v
+  helper (Catch₁ ())   | nat zero
+  helper (Catch₁ ())   | nat (suc n)
+  helper (Catch₂ () _) | nat zero
+  helper (Catch₂ () _) | nat (suc n)
+  helper (Catch₂ () _) | throw
hunk ./StatusLemmas.agda 71
--- In a total setting the more limited variant is provable, though.
+-- In a total setting the following more limited variant is
+-- provable...
hunk ./StatusLemmas.agda 88
+-- ...but not in a partial setting.
+
+¬UtoB′ : ∃ λ (x : Expr partial) → x ↡[ U ] × ¬ (x ↡[ B ])
+¬UtoB′ = (x , (0 , Catch₂ Int Val) , helper)
+  where
+  x = loop ⌜ nat 0 ⌝ catch ⌜ nat 0 ⌝
+
+  helper : ¬ (x ↡[ B ])
+  helper (n , Catch₁ ⇓)                    = loop-¬⇓ nat-¬↯ (nat n , ⇓)
+  helper (n , Catch₂ (Loop (Seqn₁ _ ↯)) _) = loop-¬⇓ nat-¬↯ (throw , ↯)
+  helper (n , Catch₂ (Loop (Seqn₂ ())) _)
+
hunk ./StatusLemmas.agda 108
-block-unblockʳ : ¬ (∀ t (x : Expr t) → block (unblock x) ⊑ x)
-block-unblockʳ bux⊑x
-  with _⊑_.⇓ (bux⊑x total ⌜ nat 0 ⌝) {i = B} (Block (Unblock Int))
-... | ()
+block-unblockʳ : ∀ t → ∃ λ (x : Expr t) → block (unblock x) ⋢ x
+block-unblockʳ _ =
+  (⌜ nat 0 ⌝ , λ bu⊑ → nat-¬↯ (_⊑_.⇓ bu⊑ {i = B} (Block (Unblock Int))))
hunk ./StatusLemmas.agda 112
-unblock-blockˡ : ¬ (∀ t (x : Expr t) → x ⊑ unblock (block x))
-unblock-blockˡ x⊑ubx
-  with _⊑_.⇓ (x⊑ubx total (⌜ nat 0 ⌝ catch ⌜ nat 1 ⌝)) (Catch₂ Int Val)
-... | Unblock (Block (Catch₁ ()))
-... | Unblock (Block (Catch₂ () _))
+unblock-blockˡ : ∀ t → ∃ λ (x : Expr t) → x ⋢ unblock (block x)
+unblock-blockˡ t =
+  (⌜ nat 0 ⌝ catch ⌜ nat 1 ⌝ , λ ⊑ub →
+     helper (_⊑_.⇓ ⊑ub (Catch₂ Int Val)))
+  where
+  helper : ¬ (unblock {t} (block (⌜ nat 0 ⌝ catch ⌜ nat 1 ⌝))
+                ⇓[ U ] nat 1)
+  helper (Unblock (Block (Catch₁ ())))
+  helper (Unblock (Block (Catch₂ () _)))
hunk ./StatusLemmas.agda 122
-unblock-blockʳ : ¬ (∀ t (x : Expr t) → unblock (block x) ⊑ x)
-unblock-blockʳ ubx⊑x
-  with _⊑_.⇓ (ubx⊑x total ⌜ nat 0 ⌝) {i = B} (Unblock Int)
-... | ()
+unblock-blockʳ : ∀ t → ∃ λ (x : Expr t) → unblock (block x) ⋢ x
+unblock-blockʳ _ =
+  (⌜ nat 0 ⌝ , λ ub⊑ → nat-¬↯ (_⊑_.⇓ ub⊑ {i = B} (Unblock Int)))
hunk ./Totality.agda 34
-¬defined : ¬ (∀ (x : Expr partial) i → x ⇓[ i ])
-¬defined ⇓ = loop-¬⇓ nat-¬↯ (⇓ (loop ⌜ nat 0 ⌝) B)
+¬defined : ∃₂ λ (x : Expr partial) i → ¬ x ⇓[ i ]
+¬defined = (loop ⌜ nat 0 ⌝ , B , loop-¬⇓ nat-¬↯)