Nuprl Lemma : isaxiom-sqequal

`∀[C:Base]`
`  ∀[A,B,z:Base].`
`    if z = Ax then A z otherwise B z ~ C z `
`    supposing (A Ax ~ C Ax) ∧ ((∀a,b:Base.  (if z = Ax 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]` isaxiom: `if z = Ax then a otherwise b` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` apply: `f a` base: `Base` sqequal: `s ~ t` axiom: `Ax`
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` 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-isaxiom-2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalSqle divergentSqle callbyvalueIsaxiom sqequalHypSubstitution hypothesis productElimination thin lemma_by_obid dependent_functionElimination hypothesisEquality independent_functionElimination unionElimination sqequalRule sqleReflexivity baseApply closedConclusion baseClosed lambdaFormation because_Cache isaxiomExceptionCases axiomSqleEquality isectElimination callbyvalueApply applyExceptionCases sqequalAxiom sqequalIntensionalEquality functionEquality lambdaEquality isect_memberEquality equalityTransitivity equalitySymmetry exceptionSqequal

Latex:
\mforall{}[C:Base]
\mforall{}[A,B,z:Base].
if  z  =  Ax  then  A  z  otherwise  B  z  \msim{}  C  z
supposing  (A  Ax  \msim{}  C  Ax)  \mwedge{}  ((\mforall{}a,b:Base.    (if  z  =  Ax  then  a  otherwise  b  \msim{}  b))  {}\mRightarrow{}  (B  z  \msim{}  C  z))
supposing  strict(C)

Date html generated: 2016_05_13-PM-03_24_08
Last ObjectModification: 2016_01_14-PM-06_46_29

Theory : call!by!value_1

Home Index