Nuprl Definition : bar_bwd_fim_classical
bar_bwd_fim_classical(R; A) ==
(
a:
List. ((
R a) 
(A a))) (a: List. ((s:. (A (a @ [s]))) (A a))) (A [])
Definitions occuring in Statement :
append: as @ bs,
nat: ,
all: x:A. B[x],
squash: T,
implies: P Q,
apply: f a
bar\_bwd\_fim\_classical(R; A) ==
(\mforall{}a:\mBbbN{} List. ((\mdownarrow{}R a) {}\mRightarrow{} (\mdownarrow{}A a))) {}\mRightarrow{} (\mforall{}a:\mBbbN{} List. ((\mforall{}s:\mBbbN{}. (\mdownarrow{}A (a @ [s]))) {}\mRightarrow{} (\mdownarrow{}A a))) {}\mRightarrow{} (\mdownarrow{}A [])
Date html generated:
2013_03_20-AM-10_31_37
Last ObjectModification:
2013_02_25-PM-05_11_42
Home
Index