Nuprl Lemma : pcw-path-copathAgree

∀[A:𝕌']. ∀[B:A ⟶ Type].
  ∀w:coW(A;a.B[a]). ∀path:Path.
    (StepAgree(path 0;⋅;w)
    ⇒ (∀i:ℕ
          ((copath-length(pcw-path-coPath(i + 1;path)) = (i + 1) ∈ ℤ)
          ⇒ (copath-length(pcw-path-coPath(i;path)) = i ∈ ℤ)
          ⇒ copathAgree(a.B[a];w;pcw-path-coPath(i;path);pcw-path-coPath(i + 1;path)))))


Proof



Definitions occuring in Statement :  pcw-path-coPath: pcw-path-coPath(n;p),  copathAgree: copathAgree(a.B[a];w;x;y),  copath-length: copath-length(p),  coW: coW(A;a.B[a]),  pcw-path: Path,  pcw-step-agree: StepAgree(s;p1;w),  nat: ℕ,  it: ⋅,  uall: ∀[x:A]. B[x],  so_apply: x[s],  all: ∀x:A. B[x],  implies: P ⇒ Q,  unit: Unit,  apply: f a,  function: x:A ⟶ B[x],  add: n + m,  natural_number: $n,  int: ℤ,  universe: Type,  equal: s = t ∈ T
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  implies: P ⇒ Q,  member: t ∈ T,  uimplies: b supposing a,  and: P ∧ Q,  nat: ℕ,  decidable: Dec(P),  or: P ∨ Q,  iff: P ⇐⇒ Q,  not: ¬A,  rev_implies: P ⇐ Q,  false: False,  prop: ℙ,  uiff: uiff(P;Q),  sq_stable: SqStable(P),  squash: ↓T,  subtract: n - m,  subtype_rel: A ⊆r B,  top: Top,  le: A ≤ B,  less_than': less_than'(a;b),  true: True,  so_lambda: λ2x.t[x],  so_apply: x[s],  so_lambda: λ2x y.t[x; y],  so_apply: x[s1;s2],  so_lambda: so_lambda(x,y,z.t[x; y; z]),  so_apply: x[s1;s2;s3],  pcw-path: Path,  coW: coW(A;a.B[a]),  cand: A c∧ B,  pcw-path-coPath: pcw-path-coPath(n;p),  bool: 𝔹,  unit: Unit,  it: ⋅,  btrue: tt,  ifthenelse: if b then t else f fi ,  bfalse: ff,  guard: {T},  let: let,  pcw-step: pcw-step(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b]),  spreadn: spread3,  copath: copath(a.B[a];w),  copathAgree: copathAgree(a.B[a];w;x;y),  copath-extend: copath-extend(q;t),  less_than: a < b,  eq_int: (i =z j),  coPath-extend: coPath-extend(n;p;t),  coPath: coPath(a.B[a];w;n),  coPathAgree: coPathAgree(a.B[a];n;w;p;q),  ge: i ≥ j ,  exposed-it: exposed-it
Lemmas referenced :  pcw-path-coPath_wf,  decidable__le,  false_wf,  not-le-2,  sq_stable__le,  condition-implies-le,  minus-add,  minus-one-mul,  zero-add,  minus-one-mul-top,  add-associates,  add-swap,  add-commutes,  add_functionality_wrt_le,  add-zero,  le-add-cancel,  le_wf,  nat_wf,  pcw-step-agree_wf,  unit_wf2,  it_wf,  pcw-path_wf,  coW_wf,  sq_stable__copathAgree,  equal_wf,  copath-length_wf,  eq_int_wf,  bool_wf,  equal-wf-T-base,  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,  le_antisymmetry_iff,  add-subtract-cancel,  pcw-step_wf,  copath-nil-Agree,  copath_wf,  top_wf,  squash_wf,  member_wf,  equal-wf-base,  decidable__lt,  not-lt-2,  add-mul-special,  zero-mul,  coPath_wf,  le_weakening,  int_subtype_base,  minus-minus,  less-iff-le,  not-ge-2,  subtract_wf,  true_wf,  less_than_wf,  ge_wf,  less_than_irreflexivity,  less_than_transitivity1,  nat_properties,  coW-dom_wf,  coW-item_wf
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation,  lambdaFormation,  cut,  introduction,  extract_by_obid,  sqequalHypSubstitution,  isectElimination,  thin,  hypothesisEquality,  independent_isectElimination,  hypothesis,  productElimination,  dependent_set_memberEquality,  addEquality,  setElimination,  rename,  natural_numberEquality,  dependent_functionElimination,  unionElimination,  independent_pairFormation,  voidElimination,  independent_functionElimination,  sqequalRule,  imageMemberEquality,  baseClosed,  imageElimination,  applyEquality,  lambdaEquality,  isect_memberEquality,  voidEquality,  intEquality,  because_Cache,  minusEquality,  instantiate,  cumulativity,  functionEquality,  universeEquality,  equalityTransitivity,  equalitySymmetry,  equalityElimination,  impliesFunctionality,  lessCases,  axiomSqEquality,  productEquality,  multiplyEquality,  closedConclusion,  baseApply,  functionExtensionality,  independent_pairEquality,  axiomEquality,  intWeakElimination
Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].
    \mforall{}w:coW(A;a.B[a]).  \mforall{}path:Path.
        (StepAgree(path  0;\mcdot{};w)
        {}\mRightarrow{}  (\mforall{}i:\mBbbN{}
                    ((copath-length(pcw-path-coPath(i  +  1;path))  =  (i  +  1))
                    {}\mRightarrow{}  (copath-length(pcw-path-coPath(i;path))  =  i)
                    {}\mRightarrow{}  copathAgree(a.B[a];w;pcw-path-coPath(i;path);pcw-path-coPath(i  +  1;path)))))


Date html generated: 2019_06_20-PM-00_57_13
Last ObjectModification: 2019_01_02-PM-01_34_12

Theory : co-recursion-2


Home Index