Nuprl Lemma : ppcc-test4

∀f:ℤ ⟶ ℤ
  ∀[Q,P:ℤ ⟶ ℤ ⟶ ℙ].
    ((∀a,b:ℤ.  (Q[f[a];b] ⇐⇒ P[a;f[b]]))
    ⇒ Trans(ℤ;a,b.P[a;b])
    ⇒ (∀z,w:𝔹.
          ∀a,b,c,d,e:ℤ. ∀x:{z:ℤ| f[(z + 1) - 1] = d ∈ ℤ} .
            ((f[(b + 2) - 2] = if (w ∨bz) ∧b (c =z x) then e + 1 else f[b] fi  ∈ ℤ) c∧ P[a;a + 1])
            ⇒ P[(a + a) - a;c]
            ⇒ (∀x:ℤ × ℤ. Q[fst(x);b] ⇒ P[snd(x);e + 1] supposing x = <d, a> ∈ (ℤ × ℤ)) 
            supposing <<c, a>, e> = <<x, a>, e> ∈ (ℤ × ℤ × ℤ) 
          supposing (↑z) ∧ (¬↑w)))


Proof



Definitions occuring in Statement :  trans: Trans(T;x,y.E[x; y]),  bor: p ∨bq,  band: p ∧b q,  assert: ↑b,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  bool: 𝔹,  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  cand: A c∧ B,  prop: ℙ,  so_apply: x[s1;s2],  so_apply: x[s],  pi1: fst(t),  pi2: snd(t),  all: ∀x:A. B[x],  iff: P ⇐⇒ Q,  not: ¬A,  implies: P ⇒ Q,  and: P ∧ Q,  set: {x:A| B[x]} ,  function: x:A ⟶ B[x],  pair: <a, b>,  product: x:A × B[x],  subtract: n - m,  add: n + m,  natural_number: $n,  int: ℤ,  equal: s = t ∈ T
Definitions unfolded in proof :  all: ∀x:A. B[x],  uall: ∀[x:A]. B[x],  implies: P ⇒ Q,  uimplies: b supposing a,  member: t ∈ T,  and: P ∧ Q,  not: ¬A,  false: False,  so_apply: x[s1;s2],  pi1: fst(t),  subtype_rel: A ⊆r B,  so_lambda: λ2x.t[x],  so_apply: x[s],  cand: A c∧ B,  bool: 𝔹,  unit: Unit,  it: ⋅,  btrue: tt,  uiff: uiff(P;Q),  bor: p ∨bq,  ifthenelse: if b then t else f fi ,  band: p ∧b q,  bfalse: ff,  exists: ∃x:A. B[x],  or: P ∨ Q,  sq_type: SQType(T),  guard: {T},  bnot: ¬bb,  assert: ↑b,  prop: ℙ,  so_lambda: λ2x y.t[x; y],  iff: P ⇐⇒ Q,  rev_implies: P ⇐ Q,  pi2: snd(t),  squash: ↓T,  true: True,  trans: Trans(T;x,y.E[x; y])
Lemmas referenced :  assert_witness,  product_subtype_base,  int_subtype_base,  subtract_wf,  eqtt_to_assert,  eqff_to_assert,  bool_cases_sqequal,  subtype_base_sq,  bool_subtype_base,  assert-bnot,  eq_int_wf,  set_subtype_base,  equal_wf,  istype-int,  assert_wf,  istype-void,  bool_wf,  trans_wf,  add-subtract-cancel,  squash_wf,  true_wf,  istype-universe,  subtype_rel_self,  iff_weakening_equal,  eq_int_eq_true,  btrue_wf,  iff_imp_equal_bool,  bfalse_wf,  istype-assert,  bor_wf,  iff_weakening_uiff,  or_wf,  false_wf,  assert_of_bor,  iff_transitivity,  equal-wf-base,  assert_of_band,  and_functionality_wrt_uiff3,  assert_of_eq_int,  ite_rw_true,  pi2_wf,  pi1_wf,  band_wf,  ifthenelse_wf
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  lambdaFormation_alt,  isect_memberFormation_alt,  cut,  introduction,  sqequalRule,  sqequalHypSubstitution,  productElimination,  thin,  independent_pairEquality,  extract_by_obid,  isectElimination,  hypothesisEquality,  independent_functionElimination,  hypothesis,  lambdaEquality_alt,  dependent_functionElimination,  voidElimination,  functionIsTypeImplies,  inhabitedIsType,  rename,  axiomEquality,  universeIsType,  applyEquality,  because_Cache,  equalityIsType4,  baseApply,  closedConclusion,  baseClosed,  intEquality,  independent_isectElimination,  productIsType,  addEquality,  natural_numberEquality,  unionElimination,  equalityElimination,  equalityTransitivity,  equalitySymmetry,  dependent_pairFormation_alt,  equalityIsType1,  promote_hyp,  instantiate,  setElimination,  setIsType,  functionIsType,  universeEquality,  imageElimination,  imageMemberEquality,  productEquality,  independent_pairFormation,  unionIsType,  inrFormation_alt,  isect_memberEquality_alt,  cumulativity,  hyp_replacement,  dependent_set_memberEquality_alt,  equalityIsType3,  applyLambdaEquality
Latex:
\mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}
    \mforall{}[Q,P:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbP{}].
        ((\mforall{}a,b:\mBbbZ{}.    (Q[f[a];b]  \mLeftarrow{}{}\mRightarrow{}  P[a;f[b]]))
        {}\mRightarrow{}  Trans(\mBbbZ{};a,b.P[a;b])
        {}\mRightarrow{}  (\mforall{}z,w:\mBbbB{}.
                    \mforall{}a,b,c,d,e:\mBbbZ{}.  \mforall{}x:\{z:\mBbbZ{}|  f[(z  +  1)  -  1]  =  d\}  .
                        ((f[(b  +  2)  -  2]  =  if  (w  \mvee{}\msubb{}z)  \mwedge{}\msubb{}  (c  =\msubz{}  x)  then  e  +  1  else  f[b]  fi  )  c\mwedge{}  P[a;a  +  1])
                        {}\mRightarrow{}  P[(a  +  a)  -  a;c]
                        {}\mRightarrow{}  (\mforall{}x:\mBbbZ{}  \mtimes{}  \mBbbZ{}.  Q[fst(x);b]  {}\mRightarrow{}  P[snd(x);e  +  1]  supposing  x  =  <d,  a>) 
                        supposing  <<c,  a>,  e>  =  <<x,  a>,  e> 
                    supposing  (\muparrow{}z)  \mwedge{}  (\mneg{}\muparrow{}w)))


Date html generated: 2019_10_15-AM-11_06_43
Last ObjectModification: 2018_10_12-AM-10_17_24

Theory : general


Home Index