### Nuprl Lemma : ispair-sqequal

`∀[C:Base]`
`  ∀[A,B,z:Base].`
`    if z is a pair then A z otherwise B z ~ C z `
`    supposing ((z ~ <fst(z), snd(z)>) `` (A <fst(z), snd(z)> ~ C <fst(z), snd(z)>))`
`    ∧ ((∀a,b:Base.  (if z is a pair then a otherwise b ~ b)) `` (B z ~ C z)) `
`  supposing strict(C)`

Proof

Definitions occuring in Statement :  strict: `strict(F)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` pi1: `fst(t)` pi2: `snd(t)` ispair: `if z is a pair then a otherwise b` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` apply: `f a` pair: `<a, b>` base: `Base` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` has-value: `(a)↓` and: `P ∧ Q` cand: `A c∧ B` all: `∀x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` pi1: `fst(t)` pi2: `snd(t)` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` guard: `{T}` strict: `strict(F)`
Lemmas referenced :  strict_wf base_wf all_wf and_wf is-exception_wf has-value_wf_base has-value-implies-dec-ispair-2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalSqle divergentSqle callbyvalueIspair sqequalHypSubstitution hypothesis productElimination thin lemma_by_obid dependent_functionElimination hypothesisEquality independent_functionElimination unionElimination sqequalRule sqleReflexivity isectElimination baseApply closedConclusion baseClosed lambdaFormation because_Cache ispairExceptionCases axiomSqleEquality callbyvalueApply applyExceptionCases sqequalAxiom functionEquality sqequalIntensionalEquality lambdaEquality isect_memberEquality equalityTransitivity equalitySymmetry exceptionSqequal

Latex:
\mforall{}[C:Base]
\mforall{}[A,B,z:Base].
if  z  is  a  pair  then  A  z  otherwise  B  z  \msim{}  C  z
supposing  ((z  \msim{}  <fst(z),  snd(z)>)  {}\mRightarrow{}  (A  <fst(z),  snd(z)>  \msim{}  C  <fst(z),  snd(z)>))
\mwedge{}  ((\mforall{}a,b:Base.    (if  z  is  a  pair  then  a  otherwise  b  \msim{}  b))  {}\mRightarrow{}  (B  z  \msim{}  C  z))
supposing  strict(C)

Date html generated: 2016_05_13-PM-03_24_03
Last ObjectModification: 2016_01_14-PM-06_47_01

Theory : call!by!value_1

Home Index