Nuprl Lemma : ispolyform_leaf_lemma
∀n,x:Top.  (ispolyform(tree_leaf(x)) n ~ tt)
Proof
Definitions occuring in Statement : 
ispolyform: ispolyform(p)
, 
tree_leaf: tree_leaf(value)
, 
btrue: tt
, 
top: Top
, 
all: ∀x:A. B[x]
, 
apply: f a
, 
sqequal: s ~ t
Definitions unfolded in proof : 
ispolyform: ispolyform(p)
, 
tree_leaf: tree_leaf(value)
, 
tree_ind: tree_ind, 
all: ∀x:A. B[x]
, 
member: t ∈ T
Lemmas referenced : 
top_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalRule, 
sqequalReflexivity, 
sqequalTransitivity, 
computationStep, 
lambdaFormation, 
cut, 
introduction, 
extract_by_obid, 
hypothesis
Latex:
\mforall{}n,x:Top.    (ispolyform(tree\_leaf(x))  n  \msim{}  tt)
Date html generated:
2017_10_01-AM-08_32_13
Last ObjectModification:
2017_05_02-PM-00_38_31
Theory : integer!polynomial!trees
Home
Index