Nuprl Lemma : l_mul_wf

[L:ℤ List]. (l_mul(L) ∈ ℤ)


Proof




Definitions occuring in Statement :  l_mul: l_mul(L) list: List uall: [x:A]. B[x] member: t ∈ T int:
Definitions unfolded in proof :  l_mul: l_mul(L) uall: [x:A]. B[x] member: t ∈ T
Lemmas referenced :  reduce_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin intEquality lambdaEquality multiplyEquality hypothesisEquality natural_numberEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[L:\mBbbZ{}  List].  (l\_mul(L)  \mmember{}  \mBbbZ{})



Date html generated: 2016_05_14-PM-02_54_18
Last ObjectModification: 2015_12_26-PM-02_32_56

Theory : list_1


Home Index