Nuprl Lemma : l_tree_ind_test
max_l_tree(l_tree_leaf(3);λx.x) ~ inr ⋅ 
Proof
Definitions occuring in Statement : 
max_l_tree: max_l_tree(t;f)
, 
l_tree_leaf: l_tree_leaf(val)
, 
it: ⋅
, 
lambda: λx.A[x]
, 
inr: inr x 
, 
natural_number: $n
, 
sqequal: s ~ t
Definitions unfolded in proof : 
max_l_tree: max_l_tree(t;f)
, 
l_tree_leaf: l_tree_leaf(val)
, 
l_tree_ind: l_tree_ind
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
sqequalRule
Latex:
max\_l\_tree(l\_tree\_leaf(3);\mlambda{}x.x)  \msim{}  inr  \mcdot{} 
Date html generated:
2018_05_22-PM-09_39_44
Last ObjectModification:
2018_01_23-PM-01_04_27
Theory : labeled!trees
Home
Index