Nuprl Lemma : comparison-seq-zero-simple

[T:Type]. ∀[c1,c2:comparison(T)]. ∀[x,y:T].
uiff((comparison-seq(c1; c2) y) 0 ∈ ℤ;((c1 y) 0 ∈ ℤ) ∧ ((c2 y) 0 ∈ ℤ))

Proof

Definitions occuring in Statement :  comparison-seq: comparison-seq(c1; c2) comparison: comparison(T) uiff: uiff(P;Q) uall: [x:A]. B[x] and: P ∧ Q apply: a natural_number: \$n int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B comparison: comparison(T) prop: uimplies: supposing a all: x:A. B[x]
Lemmas referenced :  comparison-seq-zero subtype_rel_comparison equal-wf-T-base comparison_wf
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality isect_memberEquality applyEquality setEquality cumulativity intEquality setElimination rename baseClosed because_Cache independent_isectElimination lambdaEquality sqequalRule dependent_functionElimination universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[c1,c2:comparison(T)].  \mforall{}[x,y:T].
uiff((comparison-seq(c1;  c2)  x  y)  =  0;((c1  x  y)  =  0)  \mwedge{}  ((c2  x  y)  =  0))

Date html generated: 2017_04_17-AM-08_28_49
Last ObjectModification: 2017_02_27-PM-04_49_22

Theory : list_1

Home Index