Nuprl Lemma : mreducible_wf

g:GrpSig. ∀a:|g|.  (Reducible(a) ∈ ℙ)


Proof




Definitions occuring in Statement :  mreducible: Reducible(a) prop: all: x:A. B[x] member: t ∈ T grp_car: |g| grp_sig: GrpSig
Definitions unfolded in proof :  mreducible: Reducible(a) all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] so_lambda: λ2x.t[x] infix_ap: y so_apply: x[s]
Lemmas referenced :  exists_wf grp_car_wf and_wf not_wf munit_wf equal_wf grp_op_wf grp_sig_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaEquality dependent_functionElimination applyEquality

Latex:
\mforall{}g:GrpSig.  \mforall{}a:|g|.    (Reducible(a)  \mmember{}  \mBbbP{})



Date html generated: 2016_05_16-AM-07_44_03
Last ObjectModification: 2015_12_28-PM-05_54_10

Theory : factor_1


Home Index