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