### Nuprl Lemma : rel-path-between-append

`∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].`
`  ∀L1,L2:T List. ∀x,y,z:T.`
`    (rel-path-between(T;R;x;y;L1)`
`    `` rel-path-between(T;R;y;z;L2)`
`    `` Refl(T;v1,v2.R v1 v2)`
`    `` rel-path-between(T;R;x;z;L1 @ L2))`

Proof

Definitions occuring in Statement :  rel-path-between: `rel-path-between(T;R;x;y;L)` append: `as @ bs` list: `T List` refl: `Refl(T;x,y.E[x; y])` uall: `∀[x:A]. B[x]` prop: `ℙ` all: `∀x:A. B[x]` implies: `P `` Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` prop: `ℙ` rel-path-between: `rel-path-between(T;R;x;y;L)` and: `P ∧ Q` cand: `A c∧ B` decidable: `Dec(P)` or: `P ∨ Q` less_than: `a < b` squash: `↓T` uimplies: `b supposing a` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` listp: `A List+` subtype_rel: `A ⊆r B` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` less_than': `less_than'(a;b)` cons: `[a / b]` bfalse: `ff` rel-path: `rel-path(R;L)` int_seg: `{i..j-}` lelt: `i ≤ j < k` le: `A ≤ B` guard: `{T}` infix_ap: `x f y` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` uiff: `uiff(P;Q)` ge: `i ≥ j ` sq_type: `SQType(T)` bnot: `¬bb` so_lambda: `λ2x.t[x]` so_apply: `x[s]` last: `last(L)` subtract: `n - m` refl: `Refl(T;x,y.E[x; y])` gt: `i > j`
Lemmas referenced :  refl_wf rel-path-between_wf list_wf istype-universe length-append decidable__lt length_wf full-omega-unsat intformand_wf intformnot_wf intformless_wf itermConstant_wf itermAdd_wf itermVar_wf istype-int int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_wf hd-append-sq subtype_rel_list top_wf istype-less_than last_append list-cases null_nil_lemma length_of_nil_lemma product_subtype_list null_cons_lemma length_of_cons_lemma istype-void int_trichot subtract_wf int_seg_wf append_wf itermSubtract_wf int_term_value_subtract_lemma istype-le int_seg_properties decidable__le intformle_wf int_formula_prop_le_lemma select_append_front subtype_rel_self iff_weakening_equal intformeq_wf int_formula_prop_eq_lemma select_append lt_int_wf eqtt_to_assert assert_of_lt_int non_neg_length length_append eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot iff_weakening_uiff assert_wf less_than_wf set_subtype_base lelt_wf int_subtype_base decidable__equal_int select-as-hd add-associates minus-one-mul add-swap add-mul-special zero-add zero-mul add-member-int_seg2 add-commutes select_wf select_append_back squash_wf le_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt universeIsType cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule lambdaEquality_alt applyEquality inhabitedIsType hypothesis functionIsType because_Cache universeEquality instantiate productElimination independent_pairFormation Error :memTop,  dependent_functionElimination natural_numberEquality addEquality unionElimination imageElimination independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality voidElimination dependent_set_memberEquality_alt promote_hyp hypothesis_subsumption setElimination rename productIsType equalityTransitivity equalitySymmetry equalityElimination equalityIstype cumulativity intEquality multiplyEquality hyp_replacement closedConclusion minusEquality productEquality imageMemberEquality baseClosed

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
\mforall{}L1,L2:T  List.  \mforall{}x,y,z:T.
(rel-path-between(T;R;x;y;L1)
{}\mRightarrow{}  rel-path-between(T;R;y;z;L2)
{}\mRightarrow{}  Refl(T;v1,v2.R  v1  v2)
{}\mRightarrow{}  rel-path-between(T;R;x;z;L1  @  L2))

Date html generated: 2020_05_19-PM-09_52_53
Last ObjectModification: 2020_02_06-PM-09_36_48

Theory : relations2

Home Index