Nuprl Lemma : coW-equiv-iff3

∀[A:𝕌']
  ∀B:A ⟶ Type. ∀w,w':coW(A;a.B[a]).
    (coW-equiv(a.B[a];w;w')
    ⇐⇒ ∀p:maximal-copath(a.B[a];w')
          ∃q:maximal-copath(a.B[a];w)
           ∀n:ℕ
             ((∀i:ℕn. (copath-length(p i) = i ∈ ℤ))
             ⇒ (∀i:ℕn. ((copath-length(q i) = i ∈ ℤ) ∧ coW-equiv(a.B[a];copath-at(w;q i);copath-at(w';p i))))))

Proof

Definitions occuring in Statement : maximal-copath: maximal-copath(a.B[a];w), coW-equiv: coW-equiv(a.B[a];w;w'), copath-length: copath-length(p), copath-at: copath-at(w;p), coW: coW(A;a.B[a]), int_seg: {i..j^-}, nat: ℕ, uall: ∀[x:A]. B[x], so_apply: x[s], all: ∀x:A. B[x], exists: ∃x:A. B[x], iff: P ⇐⇒ Q, implies: P ⇒ Q, and: P ∧ Q, apply: f a, function: x:A ⟶ B[x], natural_number: $n, int: ℤ, universe: Type, equal: s = t ∈ T
Definitions unfolded in proof : copath-length: copath-length(p), copath: copath(a.B[a];w), btrue: tt, eq_int: (i =_z j), ifthenelse: if b then t else f fi , coPath-at: coPath-at(n;w;p), copath-nil: (), copath-at: copath-at(w;p), less_than: a < b, cand: A c∧ B, coWmem: coWmem(a.B[a];z;w), exists: ∃x:A. B[x], guard: {T}, sq_type: SQType(T), so_apply: x[s1;s2;s3], true: True, top: Top, subtract: n - m, squash: ↓T, sq_stable: SqStable(P), uiff: uiff(P;Q), or: P ∨ Q, decidable: Dec(P), not: ¬A, false: False, less_than': less_than'(a;b), le: A ≤ B, uimplies: b supposing a, pi1: fst(t), so_lambda: so_lambda(x,y,z.t[x; y; z]), subtype_rel: A ⊆r B, lelt: i ≤ j < k, int_seg: {i..j^-}, maximal-copath: maximal-copath(a.B[a];w), nat: ℕ, rev_implies: P ⇐ Q, so_apply: x[s], so_lambda: λ₂x.t[x], prop: ℙ, member: t ∈ T, implies: P ⇒ Q, and: P ∧ Q, iff: P ⇐⇒ Q, all: ∀x:A. B[x], uall: ∀[x:A]. B[x]
Lemmas referenced : minus-zero, not-equal-2, equal-wf-base-T, copathAgree_refl, pi1_wf, copath-nil-Agree, top_wf, it_wf, coW-equiv_transitivity, coW-equiv_inversion, copath-at-extend, length-copath-extend, copathAgree-extend, copath-extend_wf, coW-equiv_weakening, less_than_wf, coW-item_wf, copath-last_wf, coW-dom_wf, pi2_wf, add_functionality_wrt_eq, copathAgree-last, coW-equiv-iff, sq_stable__copathAgree, sq_stable__all, minus-minus, zero-mul, add-mul-special, subtract_wf, iff_weakening_equal, subtype_rel_self, lelt_wf, le-add-cancel2, less-iff-le, not-lt-2, decidable__lt, true_wf, squash_wf, decidable__int_equal, decidable__all_int_seg, int_subtype_base, subtype_base_sq, equal-wf-T-base, copath_length_nil_lemma, copath-nil_wf, le-add-cancel, add-zero, add_functionality_wrt_le, add-commutes, add-swap, add-associates, minus-one-mul-top, zero-add, minus-one-mul, minus-add, condition-implies-le, sq_stable__le, not-le-2, decidable__le, false_wf, int_seg_subtype_nat, copathAgree_wf, copath_wf, dependent-choice, coW_wf, copath-at_wf, le_wf, copath-length_wf, equal_wf, int_seg_wf, nat_wf, exists_wf, maximal-copath_wf, all_wf, coW-equiv_wf
Rules used in proof : hyp_replacement, levelHypothesis, equalityUniverse, multiplyEquality, dependent_pairFormation, axiomEquality, independent_pairEquality, dependent_pairEquality, minusEquality, voidEquality, isect_memberEquality, imageElimination, baseClosed, imageMemberEquality, independent_functionElimination, voidElimination, unionElimination, equalitySymmetry, equalityTransitivity, independent_isectElimination, functionExtensionality, addEquality, universeEquality, cumulativity, instantiate, productEquality, because_Cache, productElimination, dependent_set_memberEquality, intEquality, rename, setElimination, natural_numberEquality, functionEquality, dependent_functionElimination, hypothesis, applyEquality, lambdaEquality, sqequalRule, hypothesisEquality, thin, isectElimination, sqequalHypSubstitution, extract_by_obid, introduction, cut, independent_pairFormation, lambdaFormation, isect_memberFormation, sqequalReflexivity, computationStep, sqequalTransitivity, sqequalSubstitution

Latex:
\mforall{}[A:\mBbbU{}'] \mforall{}B:A {}\mrightarrow{} Type. \mforall{}w,w':coW(A;a.B[a]). (coW-equiv(a.B[a];w;w') \mLeftarrow{}{}\mRightarrow{} \mforall{}p:maximal-copath(a.B[a];w') \mexists{}q:maximal-copath(a.B[a];w) \mforall{}n:\mBbbN{} ((\mforall{}i:\mBbbN{}n. (copath-length(p i) = i)) {}\mRightarrow{} (\mforall{}i:\mBbbN{}n ((copath-length(q i) = i) \mwedge{} coW-equiv(a.B[a];copath-at(w;q i);copath-at(w';p i)))))) Date html generated: 2018_07_29-AM-09_21_45 Last ObjectModification: 2018_07_25-PM-03_17_39 Theory : co-recursion Home Index