Nuprl Lemma : app_permf_comp

m,n:ℕ. ∀p,p':ℕm ⟶ ℕm. ∀q,q':ℕn ⟶ ℕn.
  ((app_permf(m;n;p;q) app_permf(m;n;p';q')) app_permf(m;n;p p';q q') ∈ (ℕn ⟶ ℕn))


Proof




Definitions occuring in Statement :  app_permf: app_permf(m;n;p;q) compose: g int_seg: {i..j-} nat: all: x:A. B[x] function: x:A ⟶ B[x] add: m natural_number: $n equal: t ∈ T
Definitions unfolded in proof :  compose: g app_permf: app_permf(m;n;p;q) all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] nat: int_seg: {i..j-} subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a ifthenelse: if then else fi  btrue: tt bfalse: ff implies:  Q bool: 𝔹 unit: Unit it: uiff: uiff(P;Q) and: P ∧ Q guard: {T} lelt: i ≤ j < k ge: i ≥  decidable: Dec(P) or: P ∨ Q not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top prop: less_than: a < b squash: T le: A ≤ B iff: ⇐⇒ Q rev_implies:  Q subtract: m less_than': less_than'(a;b) true: True
Lemmas referenced :  int_seg_wf nat_wf lt_int_wf equal-wf-base bool_wf set_subtype_base le_wf istype-int int_subtype_base lelt_wf assert_wf less_than_wf le_int_wf bnot_wf uiff_transitivity eqtt_to_assert assert_of_lt_int eqff_to_assert assert_functionality_wrt_uiff bnot_of_lt_int assert_of_le_int int_seg_properties nat_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf equal-wf-T-base add_nat_wf intformless_wf int_formula_prop_less_lemma add-is-int-iff itermAdd_wf intformeq_wf int_term_value_add_lemma int_formula_prop_eq_lemma false_wf decidable__lt decidable__equal_int subtract_wf itermSubtract_wf int_term_value_subtract_lemma add-subtract-cancel add-member-int_seg2 int_seg_subtype istype-false not-le-2 condition-implies-le minus-add minus-one-mul add-swap minus-one-mul-top add-mul-special zero-mul add-zero add-associates minus-minus add-commutes zero-add le-add-cancel
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lambdaFormation_alt cut lambdaEquality_alt universeIsType introduction extract_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality addEquality setElimination rename hypothesisEquality hypothesis inhabitedIsType functionIsType baseApply closedConclusion baseClosed applyEquality intEquality independent_isectElimination because_Cache unionElimination equalityElimination independent_functionElimination productElimination equalityIsType1 equalityTransitivity equalitySymmetry dependent_functionElimination dependent_set_memberEquality_alt independent_pairFormation approximateComputation dependent_pairFormation_alt int_eqEquality isect_memberEquality_alt voidElimination productIsType applyLambdaEquality imageElimination pointwiseFunctionality promote_hyp minusEquality multiplyEquality

Latex:
\mforall{}m,n:\mBbbN{}.  \mforall{}p,p':\mBbbN{}m  {}\mrightarrow{}  \mBbbN{}m.  \mforall{}q,q':\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n.
    ((app\_permf(m;n;p;q)  o  app\_permf(m;n;p';q'))  =  app\_permf(m;n;p  o  p';q  o  q'))



Date html generated: 2019_10_16-PM-00_59_42
Last ObjectModification: 2018_10_08-AM-09_20_29

Theory : perms_1


Home Index