1signature leakageLib = 2sig 3 4 include Abbrev 5 6 val REPEAT_SAFE_EVAL : term -> thm 7 val FIND_CONV : term -> (term -> thm) -> conv 8 val ONCE_FIND_CONV : term -> (term -> thm) -> conv 9 val UNFOLD_CONV : (thm list) -> (term -> thm) -> conv 10 val MAKE_ALL_DISTINCT_CONV : (term -> thm) -> conv 11 val MEM_CONV : (term -> thm) -> conv 12 val F_UNCHANGED_CONV : (term -> thm) -> conv 13 val T_UNCHANGED_CONV : (term -> thm) -> conv 14 val T_F_UNCHANGED_CONV : (term -> thm) -> conv 15 val LEAKAGE_COMPUTE_PROVE_FINITE : term -> thm list -> thm 16 val LEAKAGE_COMPUTE_FINITE_HLR : term * term * term -> thm list -> thm list 17 val LEAKAGE_COMPUTE_CROSS_NOT_EMPTY : term * term * term -> thm list -> thm 18 val LEAKAGE_COMPUTE_INITIAL_REDUCE : term * term * term -> thm list -> conv 19 val COMPUTE_CARD : term -> (term -> thm) -> (term -> thm) -> thm 20 val COMPUTE_HLR_CARDS : term * term * term -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> thm list 21 val LEAKAGE_COMPUTE_REDUCE_CARDS : term * term * term -> thm list -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> conv 22 val LEAKAGE_COMPUTE_HLR_CROSS : term * term * term -> thm list -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> conv 23 val LEAKAGE_COMPUTE_IMAGE_HLR_CROSS : term * term * term -> thm list -> thm list -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> conv 24 val RECURSIVE_UNWIND_SUM : (term -> thm) -> (term -> thm) -> term -> thm 25 val LEAKAGE_COMPUTE_UNWIND_OUTER_SUM : (term -> thm) -> (term -> thm) -> (term -> thm) -> conv 26 val LEAKAGE_COMPUTE_UNWIND_INNER_SUM : term * term -> thm list -> thm list -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> conv 27 val LEAKAGE_COMPUTE_CONV : term * term * term -> thm list -> thm list -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> conv 28 29end 30