Nuprl Lemma : int_dot_nil_left_lemma

bs:Top. ([] ⋅ bs 0)


Proof




Definitions occuring in Statement :  integer-dot-product: as ⋅ bs nil: [] top: Top all: x:A. B[x] natural_number: $n sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T integer-dot-product: as ⋅ bs nil: [] it:
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis lemma_by_obid sqequalRule

Latex:
\mforall{}bs:Top.  ([]  \mcdot{}  bs  \msim{}  0)



Date html generated: 2016_05_14-AM-06_56_05
Last ObjectModification: 2015_12_26-PM-01_15_03

Theory : omega


Home Index