Nuprl Lemma : int_dot_cons_nil_lemma

as,a:Top.  ([a as] ⋅ [] 0)


Proof




Definitions occuring in Statement :  integer-dot-product: as ⋅ bs cons: [a b] 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 cons: [a b] so_lambda: λ2y.t[x; y] top: Top so_apply: x[s1;s2] nil: [] it:
Lemmas referenced :  top_wf spread_cons_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis lemma_by_obid sqequalRule sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality

Latex:
\mforall{}as,a:Top.    ([a  /  as]  \mcdot{}  []  \msim{}  0)



Date html generated: 2016_05_14-AM-06_56_07
Last ObjectModification: 2015_12_26-PM-01_15_00

Theory : omega


Home Index