Nuprl Lemma : l-ordered-eq-rels

T:Type. ∀R1,R2:T ⟶ T ⟶ ℙ. ∀L:T List.
  ((∀x∈L.(∀y∈L.R1[x;y] ⇐⇒ R2[x;y]))  l-ordered(T;x,y.R1[x;y];L)  l-ordered(T;x,y.R2[x;y];L))


Proof




Definitions occuring in Statement :  l-ordered: l-ordered(T;x,y.R[x; y];L) l_all: (∀x∈L.P[x]) list: List prop: so_apply: x[s1;s2] all: x:A. B[x] iff: ⇐⇒ Q implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q l-ordered: l-ordered(T;x,y.R[x; y];L) member: t ∈ T uall: [x:A]. B[x] so_lambda: λ2x.t[x] so_apply: x[s1;s2] prop: so_apply: x[s] iff: ⇐⇒ Q and: P ∧ Q so_lambda: λ2y.t[x; y]
Lemmas referenced :  l_all_iff l_all_wf2 iff_wf l_member_wf l_before_member2 l_before_member l_before_wf l-ordered_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution cut hypothesis dependent_functionElimination thin hypothesisEquality independent_functionElimination lemma_by_obid isectElimination because_Cache sqequalRule lambdaEquality applyEquality setElimination rename setEquality productElimination allFunctionality promote_hyp functionEquality cumulativity universeEquality

Latex:
\mforall{}T:Type.  \mforall{}R1,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  \mforall{}L:T  List.
    ((\mforall{}x\mmember{}L.(\mforall{}y\mmember{}L.R1[x;y]  \mLeftarrow{}{}\mRightarrow{}  R2[x;y]))  {}\mRightarrow{}  l-ordered(T;x,y.R1[x;y];L)  {}\mRightarrow{}  l-ordered(T;x,y.R2[x;y];L))



Date html generated: 2016_05_15-PM-04_38_09
Last ObjectModification: 2015_12_27-PM-02_43_32

Theory : general


Home Index