Nuprl Lemma : comb_for_massoc_wf

λg,a,b,z. (a b) ∈ g:GrpSig ⟶ a:|g| ⟶ b:|g| ⟶ (↓True) ⟶ ℙ


Proof




Definitions occuring in Statement :  massoc: b prop: squash: T true: True member: t ∈ T lambda: λx.A[x] function: x:A ⟶ B[x] grp_car: |g| grp_sig: GrpSig
Definitions unfolded in proof :  member: t ∈ T squash: T all: x:A. B[x] uall: [x:A]. B[x] prop:
Lemmas referenced :  massoc_wf squash_wf true_wf grp_car_wf grp_sig_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaEquality sqequalHypSubstitution imageElimination cut lemma_by_obid dependent_functionElimination thin hypothesisEquality equalityTransitivity hypothesis equalitySymmetry isectElimination

Latex:
\mlambda{}g,a,b,z.  (a  \msim{}  b)  \mmember{}  g:GrpSig  {}\mrightarrow{}  a:|g|  {}\mrightarrow{}  b:|g|  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbP{}



Date html generated: 2016_05_16-AM-07_43_21
Last ObjectModification: 2015_12_28-PM-05_54_37

Theory : factor_1


Home Index