Nuprl Rule : callbyvalueTry

This rule proved as lemma rule_can_test_exception_cases_true in file rules/rules_cft_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a = b ∈ T

  BY callbyvalueTry m u x y t n v c ()

  H  ⊢ (t?n:v.c)↓
  H x:(t)↓, y:(t?n:v.c ~ if n=2 n then t else ⊥) ⊢ a = b ∈ T

  H m:Base, u:Base, x:(t ~ exception(m; u)), y:(t?n:v.c ~ if n=2 m then c[u/v] else (exception(m; u))) ⊢ a = b ∈ T

  H  ⊢ t ∈ Base
  H  ⊢ n ∈ Base
  H v:Base ⊢ c ∈ Base

Definitions occuring in rule : has-value: (a)↓, bottom: ⊥, sqequal: s ~ t, atom_eq: atomeqn def, equal: s = t ∈ T, member: t ∈ T, base: Base, axiom: Ax

Latex:
H \mvdash{} a = b BY callbyvalueTry m u x y t n v c () H \mvdash{} (t?n:v.c)\mdownarrow{} H x:(t)\mdownarrow{}, y:(t?n:v.c \msim{} if n=2 n then t else \mbot{}) \mvdash{} a = b H m:Base, u:Base, x:(t \msim{} exception(m; u)), y:(t?n:v.c \msim{} if n=2 m then c[u/v] else (exception(m; u))) \mvdash{} a = b H \mvdash{} t \mmember{} Base H \mvdash{} n \mmember{} Base H v:Base \mvdash{} c \mmember{} Base Date html generated: 2019_06_20-PM-04_12_26 Last ObjectModification: 2017_01_24-PM-04_22_21 Theory : rules Home Index