### Nuprl Lemma : rel_exp-iff-path

[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
∀n:ℕ. ∀x,y:T.  (x R^n ⇐⇒ ∃L:T List. ((||L|| (n 1) ∈ ℤ) ∧ rel-path-between(T;R;x;y;L)))

Proof

Definitions occuring in Statement :  rel-path-between: rel-path-between(T;R;x;y;L) length: ||as|| list: List rel_exp: R^n nat: uall: [x:A]. B[x] prop: infix_ap: y all: x:A. B[x] exists: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q function: x:A ⟶ B[x] add: m natural_number: \$n int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] rel_exp: R^n eq_int: (i =z j) subtract: m ifthenelse: if then else fi  btrue: tt infix_ap: y implies:  Q member: t ∈ T iff: ⇐⇒ Q and: P ∧ Q nat: decidable: Dec(P) or: P ∨ Q uimplies: supposing a not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top prop: subtype_rel: A ⊆B rev_implies:  Q so_lambda: λ2x.t[x] so_apply: x[s] cand: c∧ B true: True less_than': less_than'(a;b) squash: T less_than: a < b cons: [a b] select: L[n] last: last(L) rel-path-between: rel-path-between(T;R;x;y;L) lelt: i ≤ j < k int_seg: {i..j-} guard: {T} rel-path: rel-path(R;L) le: A ≤ B ge: i ≥  sq_type: SQType(T) bool: 𝔹 unit: Unit it: uiff: uiff(P;Q) bfalse: ff assert: b
Lemmas referenced :  infix_ap_wf rel_exp_wf subtract_wf decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_subtract_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf le_wf list_wf length_wf int_subtype_base rel-path-between_wf less_than_wf primrec-wf2 all_wf iff_wf exists_wf equal_wf nat_wf equal-wf-T-base length-singleton nil_wf cons_wf reduce_hd_cons_lemma length_of_nil_lemma length_of_cons_lemma int_seg_wf satisfiable-full-omega-tt int_seg_properties int_term_value_add_lemma int_formula_prop_eq_lemma itermAdd_wf intformeq_wf non_neg_length product_subtype_list false_wf subtype_base_sq list-cases eq_int_wf equal-wf-base bool_wf assert_wf bnot_wf not_wf uiff_transitivity eqtt_to_assert assert_of_eq_int iff_transitivity iff_weakening_uiff eqff_to_assert assert_of_bnot subtype_rel_self subtract-add-cancel decidable__equal_int null_wf iff_weakening_equal squash_wf true_wf rel-path-between-cons null_nil_lemma null_cons_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  cut thin sqequalRule rename setElimination Error :functionIsType,  Error :universeIsType,  hypothesisEquality Error :inhabitedIsType,  Error :productIsType,  instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination cumulativity because_Cache universeEquality Error :dependent_set_memberEquality_alt,  natural_numberEquality hypothesis dependent_functionElimination unionElimination independent_isectElimination approximateComputation independent_functionElimination Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  int_eqEquality Error :isect_memberEquality_alt,  voidElimination independent_pairFormation functionExtensionality applyEquality Error :equalityIsType3,  baseApply closedConclusion baseClosed Error :setIsType,  productEquality intEquality addEquality lambdaEquality productElimination lambdaFormation voidEquality isect_memberEquality dependent_pairFormation equalitySymmetry imageMemberEquality computeAll hypothesis_subsumption promote_hyp levelHypothesis equalityTransitivity addLevel Error :equalityIsType4,  equalityElimination Error :equalityIsType1,  hyp_replacement applyLambdaEquality imageElimination

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
\mforall{}n:\mBbbN{}.  \mforall{}x,y:T.    (x  R\^{}n  y  \mLeftarrow{}{}\mRightarrow{}  \mexists{}L:T  List.  ((||L||  =  (n  +  1))  \mwedge{}  rel-path-between(T;R;x;y;L)))

Date html generated: 2019_06_20-PM-02_02_08
Last ObjectModification: 2018_09_30-PM-02_47_37

Theory : relations2

Home Index