formula_list

Nuprl Theory formula_list

(only non hidden objects are presented)

DISP list_rank_df ==

ABS list_rank == L.reduce(x,y. x + y;0;L)

ML list_rank_unroll let list_rankC = UnfoldC `list_rank` ANDTHENC ReduceC ;; let list_rank_nil_unrollC = FwdMacroC `list_rank_nil_unrollC` list_rankC [] ;; let list_rank_cons_unrollC = MacroC `list_rank_cons_unrollC` list_rankC (h::t) (HigherC list_rankC) h + t ;; let list_rank_unrollC = list_rank_nil_unrollC ORELSEC list_rank_cons_unrollC ;; add_AbReduce_conv `list_rank` list_rank_unrollC;;

THM list_rank_wf Formula List

THM list_rank_append_homomorphism M,N:Formula List. (M @ N) = M + N

ML list_rank_append_unroll let list_rank_append_conv = LemmaC `list_rank_append_homomorphism` ;;

the other theories

`DISP`	`list_rank_df`	`==`
`ABS`	`list_rank`	`== L.reduce(x,y. x + y;0;L)`
`ML`	`list_rank_unroll`	let list_rankC = UnfoldC `list_rank` ANDTHENC ReduceC ;; let list_rank_nil_unrollC = FwdMacroC `list_rank_nil_unrollC` list_rankC [] ;; let list_rank_cons_unrollC = MacroC `list_rank_cons_unrollC` list_rankC (h::t) (HigherC list_rankC) h + t ;; let list_rank_unrollC = list_rank_nil_unrollC ORELSEC list_rank_cons_unrollC ;; add_AbReduce_conv `list_rank` list_rank_unrollC;;
`THM`	`list_rank_wf`	`Formula List`
`THM`	`list_rank_append_homomorphism`	`M,N:Formula List. (M @ N) = M + N`
`ML`	`list_rank_append_unroll`	let list_rank_append_conv = LemmaC `list_rank_append_homomorphism` ;;