Nuprl Lemma : copathAgree-extend

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])].
∀p:copath(a.B[a];w). ∀b:coW-dom(a.B[a];copath-at(w;p)). copathAgree(a.B[a];w;p;copath-extend(p;b))

Proof

Definitions occuring in Statement : copathAgree: copathAgree(a.B[a];w;x;y), copath-extend: copath-extend(q;t), copath-at: copath-at(w;p), copath: copath(a.B[a];w), coW-dom: coW-dom(a.B[a];w), coW: coW(A;a.B[a]), uall: ∀[x:A]. B[x], so_apply: x[s], all: ∀x:A. B[x], function: x:A ⟶ B[x], universe: Type
Definitions unfolded in proof : cand: A c∧ B, assert: ↑b, bnot: ¬_bb, exists: ∃x:A. B[x], it: ⋅, unit: Unit, bool: 𝔹, bfalse: ff, sq_type: SQType(T), coPath-at: coPath-at(n;w;p), coPath: coPath(a.B[a];w;n), btrue: tt, ifthenelse: if b then t else f fi , coPath-extend: coPath-extend(n;p;t), eq_int: (i =_z j), coPathAgree: coPathAgree(a.B[a];n;w;p;q), rev_implies: P ⇐ Q, iff: P ⇐⇒ Q, or: P ∨ Q, decidable: Dec(P), guard: {T}, true: True, le: A ≤ B, subtype_rel: A ⊆r B, subtract: n - m, uimplies: b supposing a, uiff: uiff(P;Q), prop: ℙ, and: P ∧ Q, false: False, squash: ↓T, not: ¬A, less_than: a < b, less_than': less_than'(a;b), copath-at: copath-at(w;p), top: Top, nat: ℕ, copathAgree: copathAgree(a.B[a];w;x;y), copath-extend: copath-extend(q;t), copath: copath(a.B[a];w), implies: P ⇒ Q, sq_stable: SqStable(P), so_apply: x[s], so_lambda: λ₂x.t[x], member: t ∈ T, all: ∀x:A. B[x], uall: ∀[x:A]. B[x]
Lemmas referenced : coW-item_wf, neg_assert_of_eq_int, assert-bnot, bool_cases_sqequal, equal_wf, assert_of_bnot, iff_weakening_uiff, iff_transitivity, eqff_to_assert, assert_of_eq_int, eqtt_to_assert, bool_subtype_base, bool_wf, subtype_base_sq, bool_cases, int_subtype_base, not_wf, bnot_wf, assert_wf, less_than_irreflexivity, le_weakening, less_than_transitivity1, eq_int_wf, sq_stable__le, primrec-wf2, less_than_wf, set_wf, le-add-cancel2, coPath_subtype, coPath-extend_wf, coPathAgree_wf, add_functionality_wrt_le, minus-minus, zero-add, less-iff-le, not-le-2, decidable__le, subtract_wf, all_wf, le_weakening2, coPath_wf, le_wf, coPath-at_wf, coW_wf, copath_wf, copath-at_wf, coW-dom_wf, le-add-cancel, add-commutes, add-associates, add-zero, zero-mul, add-mul-special, minus-one-mul-top, add-swap, minus-one-mul, nat_wf, minus-add, condition-implies-le, not-lt-2, equal-wf-base, member_wf, false_wf, squash_wf, top_wf, copath-extend_wf, sq_stable__copathAgree
Rules used in proof : promote_hyp, dependent_pairFormation, equalityElimination, impliesFunctionality, equalitySymmetry, equalityTransitivity, unionElimination, independent_pairFormation, dependent_set_memberEquality, functionExtensionality, universeEquality, functionEquality, cumulativity, instantiate, baseClosed, imageMemberEquality, multiplyEquality, minusEquality, independent_isectElimination, intEquality, productEquality, imageElimination, voidEquality, voidElimination, isect_memberEquality, sqequalAxiom, natural_numberEquality, because_Cache, addEquality, rename, setElimination, lessCases, productElimination, independent_functionElimination, hypothesis, dependent_functionElimination, applyEquality, lambdaEquality, sqequalRule, hypothesisEquality, thin, isectElimination, sqequalHypSubstitution, extract_by_obid, introduction, cut, lambdaFormation, isect_memberFormation, sqequalReflexivity, computationStep, sqequalTransitivity, sqequalSubstitution

Latex:
\mforall{}[A:\mBbbU{}']. \mforall{}[B:A {}\mrightarrow{} Type]. \mforall{}[w:coW(A;a.B[a])]. \mforall{}p:copath(a.B[a];w). \mforall{}b:coW-dom(a.B[a];copath-at(w;p)). copathAgree(a.B[a];w;p;copath-extend(p;b)) Date html generated: 2018_07_25-PM-01_41_29 Last ObjectModification: 2018_07_24-PM-05_49_18 Theory : co-recursion Home Index