Nuprl Lemma : ispolyform_node_lemma
∀n,b,a:Top.  (ispolyform(tree_node(a;b)) n ~ ((ispolyform(a) (n - 1)) ∧b (ispolyform(b) n)) ∧b 0 <z n)
Proof
Definitions occuring in Statement : 
ispolyform: ispolyform(p)
, 
tree_node: tree_node(left;right)
, 
band: p ∧b q
, 
lt_int: i <z j
, 
top: Top
, 
all: ∀x:A. B[x]
, 
apply: f a
, 
subtract: n - m
, 
natural_number: $n
, 
sqequal: s ~ t
Definitions unfolded in proof : 
ispolyform: ispolyform(p)
, 
tree_node: tree_node(left;right)
, 
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,b,a:Top.
    (ispolyform(tree\_node(a;b))  n  \msim{}  ((ispolyform(a)  (n  -  1))  \mwedge{}\msubb{}  (ispolyform(b)  n))  \mwedge{}\msubb{}  0  <z  n)
Date html generated:
2017_10_01-AM-08_32_12
Last ObjectModification:
2017_05_02-PM-00_37_58
Theory : integer!polynomial!trees
Home
Index