Nuprl Lemma : sqeq-copath3

∀[a,b,c,f:Top]. ∀[n,m:ℤ].
  (λx.if (x) < (m)  then f if x=n then a[x] else b[x]  else c[x] ~ λx.if (x) < (m)
                                                                         then if x=n then f a[x] else (f b[x])
                                                                         else c[x])


Proof



Definitions occuring in Statement :  uall: ∀[x:A]. B[x],  top: Top,  so_apply: x[s],  less: if (a) < (b)  then c  else d,  int_eq: if a=b then c else d,  apply: f a,  lambda: λx.A[x],  int: ℤ,  sqequal: s ~ t
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  subtype_rel: A ⊆r B,  has-value: (a)↓,  and: P ∧ Q,  all: ∀x:A. B[x],  implies: P ⇒ Q,  bool: 𝔹,  unit: Unit,  it: ⋅,  btrue: tt,  uiff: uiff(P;Q),  uimplies: b supposing a,  less_than: a < b,  less_than': less_than'(a;b),  top: Top,  true: True,  squash: ↓T,  not: ¬A,  false: False,  bfalse: ff,  exists: ∃x:A. B[x],  or: P ∨ Q,  sq_type: SQType(T),  guard: {T},  bnot: ¬bb,  ifthenelse: if b then t else f fi ,  assert: ↑b,  nequal: a ≠ b ∈ T ,  rev_implies: P ⇐ Q,  iff: P ⇐⇒ Q,  prop: ℙ
Lemmas referenced :  has-value_wf_base,  int_subtype_base,  is-exception_wf,  istype-int,  istype-top,  lt_int_wf,  eqtt_to_assert,  assert_of_lt_int,  istype-void,  eq_int_wf,  assert_of_eq_int,  eqff_to_assert,  bool_subtype_base,  bool_cases_sqequal,  subtype_base_sq,  bool_wf,  assert-bnot,  neg_assert_of_eq_int,  iff_weakening_uiff,  assert_wf,  less_than_wf,  istype-less_than,  exception-not-value_1,  value-type-has-value,  int-value-type
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  Error :isect_memberFormation_alt,  introduction,  cut,  sqequalRule,  sqequalSqle,  sqleRule,  thin,  divergentSqle,  extract_by_obid,  sqequalHypSubstitution,  isectElimination,  baseApply,  closedConclusion,  baseClosed,  hypothesisEquality,  applyEquality,  hypothesis,  because_Cache,  sqleReflexivity,  axiomSqEquality,  Error :inhabitedIsType,  Error :isect_memberEquality_alt,  Error :isectIsTypeImplies,  callbyvalueLess,  productElimination,  Error :lambdaFormation_alt,  unionElimination,  equalityElimination,  equalityTransitivity,  equalitySymmetry,  independent_isectElimination,  lessCases,  independent_pairFormation,  voidElimination,  natural_numberEquality,  imageMemberEquality,  imageElimination,  independent_functionElimination,  int_eqReduceTrueSq,  Error :dependent_pairFormation_alt,  Error :equalityIsType4,  promote_hyp,  dependent_functionElimination,  instantiate,  cumulativity,  int_eqReduceFalseSq,  Error :equalityIsType1,  Error :universeIsType,  lessExceptionCases,  axiomSqleEquality,  exceptionSqequal,  intEquality
Latex:
\mforall{}[a,b,c,f:Top].  \mforall{}[n,m:\mBbbZ{}].
    (\mlambda{}x.if  (x)  <  (m)    then  f  if  x=n  then  a[x]  else  b[x]    else  c[x]  \msim{}  \mlambda{}x.if  (x)  <  (m)
                                                                                                                                                  then  if  x=n
                                                                                                                                                            then  f  a[x]
                                                                                                                                                            else  (f  b[x])
                                                                                                                                                  else  c[x])


Date html generated: 2019_06_20-PM-01_12_05
Last ObjectModification: 2019_01_02-PM-01_35_36

Theory : co-recursion-2


Home Index