### Nuprl Lemma : termination-equality-base

`∀[T:Type]. ∀[x,y:Base].  x = y ∈ T supposing (x)↓ ∧ (x = y ∈ partial(T)) supposing value-type(T)`

Proof

Definitions occuring in Statement :  partial: `partial(T)` value-type: `value-type(T)` has-value: `(a)↓` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` and: `P ∧ Q` base: `Base` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` and: `P ∧ Q` partial: `partial(T)` quotient: `x,y:A//B[x; y]` cand: `A c∧ B` label: `...\$L... t` guard: `{T}` member: `t ∈ T` prop: `ℙ` per-partial: `per-partial(T;x;y)`
Lemmas referenced :  base-partial_wf per-partial_wf has-value_wf_base partial_wf istype-base value-type_wf istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  sqequalHypSubstitution productElimination thin sqequalRule cut hypothesis pertypeElimination promote_hyp Error :productIsType,  Error :equalityIstype,  Error :universeIsType,  introduction extract_by_obid isectElimination hypothesisEquality sqequalBase equalitySymmetry because_Cache instantiate universeEquality independent_isectElimination

Latex:
\mforall{}[T:Type].  \mforall{}[x,y:Base].    x  =  y  supposing  (x)\mdownarrow{}  \mwedge{}  (x  =  y)  supposing  value-type(T)

Date html generated: 2019_06_20-PM-00_33_53
Last ObjectModification: 2018_12_22-PM-01_07_43

Theory : partial_1

Home Index