contrapos
contrapos1
not_over_forall_form
not_over_forall_form_squash
double-neg-formation
double_neg_elim
not_over_implies
contrapos_elim
contrapos_elim2
not_over_forall
not_over_forall2
not_over_forall3
not_over_forall4
excluded-middle-lower-level
not_squash_elim
not_over_forall_exists
not_over_forall_exists_form
fim97_lift_exist
exists_over_implies_pull
exists_over_implies_push
bar_fwd_fim
bar_fwd_fim_wf
bar_bwd_fim
bar_bwd_fim_wf
bar_fwd_fim_classical
bar_fwd_fim_classical_wf
bar_bwd_fim_classical
bar_bwd_fim_classical_wf
bar_26_1
bar_26_1_wf
bar_bwd_implies_fwd
bar_26_3a
bar_26_3a_wf
bar_26_3b
bar_26_3b_wf
bar_26_3a_imp_26_3b
spr
spr_wf
spr_choice_fun
spr_down_closed
negated_spr_append_back_closed
empty_spr
spr_type
in_spr
in_spr_wf
bar_26_4a
bar_26_4a_wf
gammaFIM
gammaFIM_wf
gammaFIM_id
gammaFIM_unfold
gammaFIM_unfold1
gammaFIM_true
gammaFIM_equi_length
gammaFIM_equi_length_mklist
gammaFIM_fun
gammaFIM_fun_id
bar_26_3a_imp_bar_26_4a
fin_spr
fin_spr_wf
in_fin_spr
in_fin_spr_wf
fin_spr_mem_in_fin_spr
fin_spr_mem_in_fin_spr2
FIM26_5
fan_26_6a
fan_26_6a_wf
list-in-fin_spr
list-in-fin_spr_wf
list-in-fin_spr_unfold
list-in-fin_spr_unfold_prp
boolean_as_01
fin_spr_as_list
fin_spr_as_list2
fin_spr_is_spr
in_fspr_iff_in_spr_of_fin_spr
list_of_extensions_in_fin_spr
list_of_extensions_in_fin_spr_wf
list_of_extensions_in_fin_spr1
list_of_lists_of_given_size_in_fin_spr
list_of_lists_of_given_size_in_fin_spr_wf
list_of_lists_of_given_size_in_fin_spr1
max_over_fin_spr_bound_length
shifted-sequence
shifted-sequence_wf
bar26_4a_imp_fan26_6a
gen_fin_spr
gen_fin_spr_wf
fan_26_7a
fan_26_7a_wf
fan_26_6a_imp_fan_26_7a
brouwer_prin_for_fun_27_1ax
brouwer_prin_for_fun_27_1ax_wf
monus
monus_wf
monus_of_add
monus_le
brouwer_prin_for_num_27_2_orig
brouwer_prin_for_num_27_2_orig_wf
brouwer_prin_for_num_27_2
brouwer_prin_for_num_27_2_wf
brouwer_prin_for_num27_2_equiv
brouwer_prin_fun_imp_num
brouwer_prin_for_num_simpl
brouwer_prin_for_num_simpl_wf
brouwer_prin_num_simplified_equiv
brouwer_prin_27_5
brouwer_prin_27_5_wf
brouwer_prin_27_2_imp_27_5
equal_upto
equal_upto_wf
equal_upto_mklist_eq
fan_27_7a
fan_27_7a_wf
fan_26_6a_prin27_5_imp_fan27_7a
fan_wo_dec_27_9
fan_wo_dec_27_9_wf
lift_ctr
lift_ctr_wf
dec_eq_type
dec_eq_type_wf
not_bfalse_btrue_const_fn_equal_union
strong_subtype_decidable_eq
subtype_rel_bunion
test-nat-bootstrap
nat-ind-boot
nat-ind-boot-direct
sqrt-int-aa
sqrt-int-aa2
completeInductionBootStrap
completeInductionShortExt
completeInductionFast
natInd4Boot
natInd4Boot2
natInd4BootFast
natInd4BootFast-ext
natInd4Boot22
natInd4Boot44
sqrt-int-aa-fast
sqrt-int-aa-real-fast-complete
sqrt-int-aa-real-fast-complete-ext
lec23
enumerable_implies_decidble_eq
not_base_decidble_eq_diag2
bigger
not_funcNbarB_decidable_eq_fullExt
surject_implies_decidble_eq2
not_base_enumerable3
not_base_decidable_eq_weaker
aa_hw3-3a
make_list_fan
make_list_fan_wf
aa_kleene_fan_contra
aa_kleene_fan_contra2
aa_kleene_fan_contra_total
aa_not_total_enumerable
not_total_enumerable_inc
int_enumerability_nat
aa_kleene_fan_contra4
aa_kleene_fan_contra_partial
weak_fan_th
weak_fan_th_wf
enum_not_fan
enum_not_fan2
aa_kleene_fan_contra_partial_imax
aa_dependent_fan_contra
ross_pnp
aa_list_filter_indices
aa_list_filter_indices_wf
aa_sublist_reflexive
aa_list_filtered_indices_smaller
aa_list_filtered_indices_sublist
aa_min_w_unit
aa_max_w_unit
aa_max_w_unit_wf
aa_min_w_unit_wf
aa_max_w_unit_prop1
aa_min_w_unit_prop1
aa_ltree
aa_ltree_wf
aa_lt_leaf
aa_lt_leaf_wf
aa_lt_node
aa_lt_node_wf
aa_ltree_ind
aa_ltree_ind_wf
aa_ltree-induction
aa_ltree_ind_aa_lt_leaf_compseq_tag_def
aa_ltree_ind_aa_lt_node_compseq_tag_def
aa_lt_leaf?
aa_lt_leaf?_wf
aa_lt_node?
aa_lt_node?_wf
aa_lt_node-val
aa_lt_node-val_wf
aa_lt_node-left_subtree
aa_lt_node-left_subtree_wf
aa_lt_node-right_subtree
aa_lt_node-right_subtree_wf
aa_max_ltree
aa_min_ltree
aa_min_ltree_wf
aa_max_ltree_wf
aa_bst_member
aa_bst_member_prop
aa_bst_member_prop_wf
aa_bst_member_wf
aa_binary_search_tree
aa_binary_search_tree_wf
aa_binary_search_tree_insert_long
aa_max_ltree_spec2
aa_min_ltree_spec3
aa_min_ltree_spec2
aa_max_ltree_spec
aa_min_ltree_spec
aa_max_ltree_spec3
aa_bst_member_property2
aa_bst_member_property2r
aa_bst_insert_sublemma_left
aa_bst_insert_sublemma_right
aa_bst_insert_trial4
aa_data_wrapper
aa_data_wrapper_wf
aa_data_wrapnode
aa_data_wrapnode_wf
aa_data_wrapleaf
aa_data_wrapleaf_wf
aa_data_wrapper_ind
aa_wrapper_get_data
aa_data_wrapper_ind_wf
aa_data_wrapper-induction
aa_data_wrapper_ind_aa_data_wrapnode_compseq_tag_def
aa_wrapper_get_data_wf
aa_data_wrapper_ind_aa_data_wrapleaf_compseq_tag_def
aa_data_wrapnode?
aa_data_wrapnode?_wf
aa_data_wrapnode-nd
aa_data_wrapnode-nd_wf
aa_data_wrapleaf?
aa_data_wrapleaf?_wf
aa_data_wrapleaf-val
aa_data_wrapleaf-val_wf
aa_3n_plus_1
aa_3n_step
scrap1
hw5_3_1
hw5_3_3_2
hw5_7_2
aa_3n_step_wf
aa_3n_plus_1_depth
aa_3n_plus_1_depth_pi
aa_3n_plus_1_depth_pi_wf
aa_3n_plus_1_depth_wf_comp_ind_pi_full
aa_3n_plus_1_rel
aa_3n_plus_1_rel_wf
aa_3n_plus_1_wrapped
aa_test_rec_type
aa_capply
aa_capply_wf
aa_capply_wf2
aa_pc_3n_new
aa_3n_plus_1_ctr
aa_fib_count
aa_fib_count_wf
Home
Index