### Nuprl Lemma : transitive-closure-symmetric

`∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  (Sym(A;x,y.R x y) `` Sym(A;x,y.x TC(R) y))`

Proof

Definitions occuring in Statement :  transitive-closure: `TC(R)` sym: `Sym(T;x,y.E[x; y])` uall: `∀[x:A]. B[x]` prop: `ℙ` infix_ap: `x f y` implies: `P `` Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` sym: `Sym(T;x,y.E[x; y])` all: `∀x:A. B[x]` infix_ap: `x f y` transitive-closure: `TC(R)` member: `t ∈ T` subtype_rel: `A ⊆r B` prop: `ℙ` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` spreadn: spread3 and: `P ∧ Q` uimplies: `b supposing a` cand: `A c∧ B` top: `Top` so_lambda: `λ2x.t[x]` so_apply: `x[s]` rel_path: `rel_path(A;L;x;y)` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` pi1: `fst(t)` pi2: `snd(t)` squash: `↓T` true: `True` guard: `{T}`
Lemmas referenced :  transitive-closure_wf subtype_rel_self istype-universe sym_wf subtype_rel_function map_wf reverse_wf map-length istype-void length-reverse rel_path_wf less_than_wf length_wf list_induction all_wf list_wf list_ind_nil_lemma reverse_nil_lemma map_nil_lemma list_ind_cons_lemma reverse-cons map_append_sq map_cons_lemma cons_wf squash_wf true_wf nil_wf append_wf rel_path-append subtype_rel-equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  sqequalHypSubstitution rename sqequalRule Error :universeIsType,  cut applyEquality introduction extract_by_obid isectElimination thin hypothesisEquality hypothesis instantiate universeEquality Error :inhabitedIsType,  Error :lambdaEquality_alt,  Error :functionIsType,  setElimination productElimination Error :dependent_pairEquality_alt,  functionExtensionality because_Cache functionEquality independent_isectElimination Error :productIsType,  Error :dependent_set_memberEquality_alt,  productEquality promote_hyp independent_pairFormation Error :isect_memberEquality_alt,  voidElimination natural_numberEquality independent_functionElimination dependent_functionElimination equalitySymmetry Error :equalityIsType1,  equalityTransitivity imageElimination imageMemberEquality baseClosed applyLambdaEquality

Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].    (Sym(A;x,y.R  x  y)  {}\mRightarrow{}  Sym(A;x,y.x  TC(R)  y))

Date html generated: 2019_06_20-PM-02_01_25
Last ObjectModification: 2018_10_07-AM-00_13_27

Theory : relations2

Home Index