Nuprl Lemma : normalize-decide-right

[a,F,G:Top].  (case of inl(x) => F[x] inr(x) => G[x] case of inl(x) => F[x] inr(x) => G[x] (inr ))


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] top: Top so_apply: x[s] apply: a decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T has-value: (a)↓ all: x:A. B[x] or: P ∨ Q uimplies: supposing a sq_type: SQType(T) implies:  Q guard: {T} uiff: uiff(P;Q) and: P ∧ Q ifthenelse: if then else fi  btrue: tt bfalse: ff
Lemmas referenced :  assert_of_bnot eqff_to_assert is-exception_wf has-value_wf_base eqtt_to_assert bool_subtype_base bool_wf subtype_base_sq bool_cases top_wf isl_wf injection-eta
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalSqle sqleRule thin divergentSqle callbyvalueDecide sqequalHypSubstitution hypothesis lemma_by_obid dependent_functionElimination equalityTransitivity equalitySymmetry isectElimination because_Cache unionElimination instantiate cumulativity independent_isectElimination independent_functionElimination productElimination sqequalRule sqleReflexivity baseApply closedConclusion baseClosed hypothesisEquality decideExceptionCases axiomSqleEquality exceptionSqequal sqequalAxiom isect_memberEquality

Latex:
\mforall{}[a,F,G:Top].
    (case  a  of  inl(x)  =>  F[x]  |  inr(x)  =>  G[x]  a  \msim{}  case  a  of  inl(x)  =>  F[x]  |  inr(x)  =>  G[x]  (inr  x  ))



Date html generated: 2016_05_13-PM-03_43_19
Last ObjectModification: 2016_01_14-PM-07_08_09

Theory : computation


Home Index