Nuprl Definition : bar_bwd

Nuprl Definition : bar_bwd_fim

bar_bwd_fim(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], implies: P

Q, apply: f a
FDL editor aliases : bar_bwd_fim
bar\_bwd\_fim(R;A) == (\mforall{}a:\mBbbN{} List. ((R a) {}\mRightarrow{} (A a))) {}\mRightarrow{} (\mforall{}a:\mBbbN{} List. ((\mforall{}s:\mBbbN{}. (A (a @ [s]))) {}\mRightarrow{} (A a))) {}\mRightarrow{} (A []) Date html generated: 2013_03_20-AM-10_31_29 Last ObjectModification: 2013_02_23-PM-04_26_26 Home Index