Nuprl Definition : proof-tree
proof-tree(Sequent;Rule;effect) ==
W(Sequent × Rule;sr.case effect sr of inl(subgoals) => ℕ||subgoals|| | inr(x) => Void)
Definitions occuring in Statement :
length: ||as||,
W: W(A;a.B[a]),
int_seg: {i..j-},
apply: f a,
product: x:A × B[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
natural_number: $n,
void: Void
Definitions occuring in definition :
W: W(A;a.B[a]),
product: x:A × B[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
apply: f a,
int_seg: {i..j-},
natural_number: $n,
length: ||as||,
void: Void
FDL editor aliases :
proof-tree
Latex:
proof-tree(Sequent;Rule;effect) ==
W(Sequent \mtimes{} Rule;sr.case effect sr of inl(subgoals) => \mBbbN{}||subgoals|| | inr(x) => Void)
Date html generated:
2016_05_15-PM-03_14_37
Last ObjectModification:
2015_09_23-AM-07_42_49
Theory : general
Home
Index