Nuprl Lemma : perm_induction

n:ℕ. ∀Q:Sym(n) ⟶ ℙ.  (Q[id_perm()]  (∀p:Sym(n). (Q[p]  (∀i,j:ℕn.  Q[txpose_perm(i;j) p])))  {∀p:Sym(n). Q[p]})


Proof




Definitions occuring in Statement :  txpose_perm: txpose_perm sym_grp: Sym(n) comp_perm: comp_perm id_perm: id_perm() int_seg: {i..j-} nat: prop: guard: {T} so_apply: x[s] all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] natural_number: $n
Definitions unfolded in proof :  guard: {T} all: x:A. B[x] implies:  Q member: t ∈ T sym_grp: Sym(n) uall: [x:A]. B[x] nat: so_apply: x[s] subtype_rel: A ⊆B prop: exists: x:A. B[x] so_lambda: λ2x.t[x] perm_igrp: perm_igrp(T) mk_igrp: mk_igrp(T;op;id;inv) grp_car: |g| pi1: fst(t) uimplies: supposing a int_seg: {i..j-} top: Top mon_reduce: mon_reduce grp_id: e pi2: snd(t) infix_ap: y grp_op: *
Lemmas referenced :  perm_wf int_seg_wf subtype_rel_self comp_perm_wf txpose_perm_wf id_perm_wf nat_wf sym_grp_is_swaps list_induction all_wf equal_wf mon_reduce_wf perm_igrp_wf map_wf grp_car_wf list_wf list_subtype_base product_subtype_base set_subtype_base lelt_wf istype-int int_subtype_base le_wf map_nil_lemma istype-void reduce_nil_lemma map_cons_lemma reduce_cons_lemma
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lambdaFormation_alt universeIsType cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin isectElimination natural_numberEquality setElimination rename hypothesisEquality hypothesis functionIsType applyEquality instantiate universeEquality because_Cache inhabitedIsType productElimination independent_functionElimination productEquality lambdaEquality_alt functionEquality productIsType equalityIsType3 baseApply closedConclusion baseClosed independent_isectElimination intEquality isect_memberEquality_alt voidElimination hyp_replacement equalitySymmetry applyLambdaEquality

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}Q:Sym(n)  {}\mrightarrow{}  \mBbbP{}.
    (Q[id\_perm()]  {}\mRightarrow{}  (\mforall{}p:Sym(n).  (Q[p]  {}\mRightarrow{}  (\mforall{}i,j:\mBbbN{}n.    Q[txpose\_perm(i;j)  O  p])))  {}\mRightarrow{}  \{\mforall{}p:Sym(n).  Q[p]\})



Date html generated: 2019_10_16-PM-01_02_05
Last ObjectModification: 2018_10_08-AM-11_55_45

Theory : list_2


Home Index