Created
November 27, 2010 06:17
-
-
Save kik/717629 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2288 n | |
1741 x | |
1506 apply | |
1273 m | |
1272 auto | |
1116 rewrite | |
1016 destruct | |
961 in | |
947 a | |
881 intros | |
839 forall | |
791 H | |
756 omega | |
744 P | |
733 with | |
696 S | |
685 Qed | |
644 0 | |
577 A | |
558 2 | |
541 assert | |
516 1 | |
500 y | |
498 b | |
488 intro | |
487 t | |
452 simpl | |
433 H0 | |
424 exists | |
407 f | |
403 nat | |
379 _ | |
374 Require | |
372 Import | |
345 unfold | |
342 by | |
340 Lemma | |
319 Proof | |
307 c | |
297 as | |
297 Theorem | |
294 p | |
284 H1 | |
283 replace | |
278 B | |
267 induction | |
262 e | |
249 s | |
242 T | |
241 x0 | |
211 ring | |
210 pow | |
188 Definitions | |
184 H2 | |
178 match | |
178 end | |
169 d | |
169 Q | |
166 z | |
162 Prop | |
160 t1 | |
151 C | |
150 split | |
149 xs | |
149 k | |
148 card | |
141 Leaf | |
139 Node | |
139 4 | |
138 t0 | |
130 case | |
128 t2 | |
124 Some | |
123 L | |
122 Definition | |
116 Z | |
114 X | |
113 nil | |
111 H3 | |
110 left | |
108 right | |
104 l | |
102 elim | |
101 o | |
98 clear | |
93 fun | |
91 Arith | |
90 inversion | |
88 False_ind | |
86 t3 | |
84 100 | |
83 g | |
82 sum | |
82 generalize | |
81 Mn | |
80 u | |
78 r | |
71 reflexivity | |
71 Y | |
70 env | |
69 IHn | |
67 specialize | |
66 list | |
66 double | |
65 t4 | |
65 exact | |
59 n0 | |
58 trivial | |
57 height | |
56 set | |
55 Omega | |
55 H4 | |
54 ys | |
54 Scope | |
54 Open | |
54 Let | |
54 As | |
53 N | |
52 fib | |
51 x1 | |
51 v | |
50 repeat | |
50 ZArith | |
49 tauto | |
49 remember | |
49 assumption | |
49 Z_le_dec | |
48 t5 | |
48 Fixpoint | |
48 11 | |
47 even | |
47 Collatz | |
47 3 | |
46 x2 | |
46 snd | |
46 length | |
45 i | |
45 fst | |
44 h | |
44 congruence | |
44 Z_scope | |
44 Peirce | |
44 P_dec | |
42 div2 | |
41 then | |
41 map | |
41 if | |
41 a0 | |
40 else | |
40 arith | |
40 H5 | |
39 positive | |
39 cut | |
39 Zabs | |
38 even_odd_dec | |
38 eq_nat_dec | |
37 dec | |
37 d0 | |
37 contradict | |
37 False | |
36 Zpos | |
36 O | |
36 HA | |
35 le_trans | |
35 at | |
34 q | |
34 kinaba | |
34 cbv | |
34 card_eq | |
33 qnighy | |
33 absurd | |
33 Type | |
33 Modus_ponens | |
33 I | |
32 ring_simplify | |
32 contradiction | |
32 List | |
31 rel_prime | |
31 le_lt_dec | |
31 Str_nth | |
31 Ltac | |
31 K | |
30 zarith | |
30 ksk | |
30 Excluded_Middle | |
29 symmetry | |
29 None | |
29 M | |
29 In | |
29 H6 | |
28 stk | |
28 mult_assoc | |
28 String | |
28 HB | |
27 tcard | |
27 pose | |
27 ICD | |
26 t6 | |
26 Zdiv2 | |
26 X2 | |
25 set_eq | |
25 p1 | |
25 not_even_and_odd | |
25 f2 | |
25 discriminate | |
25 compute | |
25 LPO | |
24 prime | |
24 hirose | |
24 P_all | |
23 tmp1 | |
23 scard | |
23 pz_to_pq | |
23 fold | |
23 P_ex | |
23 H7 | |
22 tri | |
22 g2 | |
22 field | |
22 eval_ops | |
22 S_last_false | |
22 IHa | |
22 91 | |
22 5 | |
21 xss | |
21 surjective_pairing | |
21 Tree | |
21 Eq | |
20 mult_comm | |
20 hy | |
20 e0 | |
19 y1 | |
19 try | |
19 le_or_lt | |
19 intersect | |
19 finite_sub | |
19 eapply | |
19 Set | |
19 HP | |
19 HD | |
19 Even | |
19 Classical | |
18 xv | |
18 true | |
18 rel_prime_sym | |
18 polyCalc | |
18 ops | |
18 iterate | |
18 injective | |
18 do | |
18 change | |
18 Z_lt_dec | |
18 X3 | |
18 X1 | |
17 y2 | |
17 total | |
17 term | |
17 sub_lists | |
17 revert | |
17 pair_i | |
17 mat | |
17 let | |
17 kik | |
17 hz | |
17 eval_expr | |
17 erewrite | |
17 decidable | |
17 Zeven_div2 | |
17 Z_eq_dec | |
17 PIE2 | |
17 Hratio | |
17 FibFunc | |
17 D | |
17 101 | |
16 using | |
16 trailing_zeros | |
16 s_Last_Theorem | |
16 perfect_square | |
16 p0 | |
16 nat_of_P | |
16 mult_plus_distr_l | |
16 mod | |
16 l0 | |
16 init_n | |
16 id_after_false | |
16 cardauto1 | |
16 card_sum | |
16 Z_le_lt_eq_dec | |
16 TtoT2 | |
16 Op | |
16 Inductive | |
16 IHm | |
16 Fermat | |
16 Falso | |
16 12 | |
16 10 | |
15 unionl | |
15 sym_eq | |
15 iso | |
15 intersect_assoc | |
15 increasing | |
15 fg2_id | |
15 false | |
15 TtoT3 | |
15 T3toT | |
15 P2N | |
15 Lt | |
15 Heqb | |
15 H8 | |
15 GCDH | |
15 Cs | |
14 t7 | |
14 pq_to_pz | |
14 o2 | |
14 mult_le_compat | |
14 lt_true_upto | |
14 gf2_id | |
14 f_equal | |
14 decoder | |
14 context | |
14 Z_of_nat | |
14 T2toT | |
14 OpAdd | |
14 IHxs | |
13 zz | |
13 term2 | |
13 t10 | |
13 rel_prime_mult_rev_l | |
13 odd_S | |
13 np | |
13 nat_decidable | |
13 mult_lt_compat_r | |
13 kururu_goedel | |
13 intuition | |
13 intersectl | |
13 injective_sub | |
13 e2 | |
13 constructor | |
13 compile | |
13 all_suffixes | |
13 all_false | |
13 Zmult_lt_0_compat | |
13 Zeven_odd_dec | |
13 TtoT4 | |
13 T7 | |
13 T4toT | |
13 IHAs | |
13 HPA | |
13 Fib | |
13 Expr | |
13 1000 | |
12 zerop | |
12 type | |
12 t01 | |
12 sqrt_2 | |
12 rwc | |
12 reg_t | |
12 plus_assoc | |
12 plus_0_r | |
12 empty | |
12 dependent | |
12 callcc | |
12 Ti53 | |
12 Ti33 | |
12 R_ack | |
12 MoCo7 | |
12 HH | |
12 HC | |
12 Gus | |
12 90 | |
11 xm | |
11 wf | |
11 union | |
11 t11 | |
11 subst | |
11 skip | |
11 pq_to_pz_ex | |
11 npair | |
11 mult_0_r | |
11 lt_irrefl | |
11 get_r | |
11 f3 | |
11 even_function | |
11 edestruct | |
11 cons | |
11 ascii_dec | |
11 Zodd | |
11 Zneg | |
11 Zmult_reg_r | |
11 Variable | |
11 TtoT5 | |
11 Ti5 | |
11 Ti3 | |
11 T5toT | |
11 Sum_of_nat | |
11 LPO_ICD | |
11 HI | |
11 Finalmat | |
11 Coq | |
11 Add | |
11 Acc_intro | |
11 Acc | |
10 zs | |
10 yy | |
10 w | |
10 tree_height_ind | |
10 transitivity | |
10 string | |
10 ranha | |
10 prime_dec | |
10 pow_unfold | |
10 pow_ge_1 | |
10 polyMult | |
10 pair_lt | |
10 p1t | |
10 p0t | |
10 o1 | |
10 mult_le_compat_l | |
10 map_map | |
10 lt_le_trans | |
10 lt_first | |
10 lt_O_Sn | |
10 hx | |
10 fouine | |
10 fibpair | |
10 exist | |
10 e1 | |
10 compose | |
10 complete | |
10 Y2 | |
10 Wf_nat | |
10 Section | |
10 Pigeon_Hole_Principle | |
10 PI | |
10 OpVar | |
10 OpConst | |
10 IHx | |
10 IHl | |
10 HeqCMP | |
10 Ha | |
10 HX2 | |
10 End | |
10 Defined | |
9 tails | |
9 sum_app | |
9 sq2 | |
9 sq1 | |
9 polyPlus | |
9 nat_rec | |
9 mult_plus_distr_r | |
9 map_app | |
9 le_n_O_eq | |
9 l1 | |
9 intersect_comm | |
9 ii | |
9 goal | |
9 get_l | |
9 from | |
9 fix | |
9 first_false | |
9 fib_collect | |
9 even_pos | |
9 even_O | |
9 eval | |
9 encoder | |
9 divergent | |
9 decP | |
9 compiler | |
9 bb | |
9 ack | |
9 Zwf | |
9 Zsucc | |
9 Zmult_lt_0_reg_r | |
9 Z_mod_mult | |
9 TtoT6 | |
9 TiA | |
9 Ti8 | |
9 Ti51 | |
9 Ti50 | |
9 T6toT | |
9 M2T | |
9 INR | |
9 IHys | |
9 Hn | |
9 HZPos | |
9 HYPos | |
9 HX | |
9 HRelPrimeYYZZ | |
9 HR0 | |
9 Div2 | |
8 z0 | |
8 y0 | |
8 xpref | |
8 xO | |
8 xI | |
8 x3 | |
8 well_def | |
8 t51 | |
8 t50 | |
8 t00 | |
8 so | |
8 s0 | |
8 prZ | |
8 pn | |
8 p1h | |
8 p0h | |
8 n1 | |
8 mult_is_O | |
8 mult_S_le_reg_l | |
8 mult | |
8 lt_n_Sn | |
8 le_antisym | |
8 jy | |
8 is_suffix | |
8 is | |
8 intersectl2 | |
8 injection | |
8 idtac | |
8 even_S | |
8 eauto | |
8 ds | |
8 div2_double | |
8 case_eq | |
8 bounded | |
8 app_comm_cons | |
8 app_ass | |
8 aBound | |
8 Zsqrt_square_id | |
8 Zplus_mod | |
8 Zabs_pos | |
8 XAB | |
8 TiA0 | |
8 Ti80 | |
8 Reals | |
8 R_scope | |
8 NNPP | |
8 Mf | |
8 Le | |
8 ICD_LPO | |
8 Hypothesis | |
8 Hhyd | |
8 HeqY | |
8 HX1 | |
8 HX0 | |
8 HEvenX | |
8 HDE | |
8 Ackermann_Function_Exists | |
8 7 | |
7 xsd | |
7 xp | |
7 wpp | |
7 well_founded | |
7 trfib | |
7 tmp2 | |
7 tmiya | |
7 t30 | |
7 sn | |
7 rel_prime_mult | |
7 reg2_m | |
7 reg1_m | |
7 prove_sup | |
7 proj2 | |
7 proj1 | |
7 pow_mono | |
7 perfect_square_dec | |
7 pattern | |
7 odd | |
7 mult_succ_r | |
7 mn | |
7 le_lt_trans | |
7 le_lt_eq_dec | |
7 jx | |
7 gf_id | |
7 fg_id | |
7 factor | |
7 f1 | |
7 elimtype | |
7 double_gt_O | |
7 decn | |
7 cardauto3 | |
7 Zsqrt_plain | |
7 Znumtheory | |
7 Zmult_lt_compat | |
7 Zmult_integral | |
7 Zlt_lower_bound_ind | |
7 Z_lt_le_dec | |
7 Ti83 | |
7 Ti82 | |
7 Ti52 | |
7 Ti4 | |
7 Ti32 | |
7 Ti31 | |
7 Ti30 | |
7 Since | |
7 R | |
7 P_of_succ_nat | |
7 IHe2 | |
7 IHe1 | |
7 Hz | |
7 Hhzd | |
7 HXPos | |
7 HX3 | |
7 HB1S | |
7 HB0 | |
7 H9 | |
7 FibSSn | |
7 Fib1 | |
7 Fib0 | |
7 EmptyString | |
7 Collatz_1000 | |
7 CollatzOne | |
7 CollatzOdd | |
7 CollatzEven | |
7 256 | |
6 xx | |
6 xH | |
6 vars | |
6 ts | |
6 tran | |
6 tmp | |
6 tg_alt | |
6 t31 | |
6 t111 | |
6 t110 | |
6 sumdec | |
6 sigmas | |
6 sa | |
6 s2 | |
6 s1 | |
6 pt | |
6 pq_to_pz_impl | |
6 polyPow | |
6 polyCalcS | |
6 plus_comm | |
6 option | |
6 nats | |
6 nat_of_P_plus_morphism | |
6 n2 | |
6 mult_0_l | |
6 lt_wf_ind | |
6 lt_ne | |
6 lt_n_Sm_le | |
6 lt_n_O | |
6 lt | |
6 le_lt_or_eq | |
6 l2 | |
6 is_prime | |
6 incr | |
6 gZA | |
6 gA8 | |
6 g85 | |
6 g53 | |
6 g30 | |
6 fib_collect_aux | |
6 factor2 | |
6 fAZ | |
6 f8A | |
6 f58 | |
6 f35 | |
6 f03 | |
6 ex_intro | |
6 even_or_odd | |
6 even_n | |
6 even_mult_l | |
6 esum | |
6 eq1 | |
6 double_even | |
6 cosum | |
6 conj | |
6 complement | |
6 col | |
6 classic | |
6 cc | |
6 beq_aux | |
6 app_eq_nil | |
6 Zodd_ex | |
6 Zmult_opp_opp | |
6 Zmult_le_compat | |
6 Zmult_comm | |
6 Zdivide_1 | |
6 Zabs_square | |
6 Zabs_nat | |
6 Var | |
6 Ti70 | |
6 Ti7 | |
6 Qmake | |
6 Pplus_minus | |
6 Pmult_comm | |
6 PPM | |
6 M91_term | |
6 L2 | |
6 Hsuf | |
6 Hin | |
6 Heqn | |
6 HeqX | |
6 HeqD | |
6 HeqC | |
6 Hc | |
6 H10 | |
6 FLT_of_n | |
6 EqSt | |
6 Const | |
6 CMP | |
5 z_to_q | |
5 vm_compute | |
5 t21 | |
5 t0_2 | |
5 scanl | |
5 rel_prime_bezout | |
5 reg3_m | |
5 red | |
5 q_to_z | |
5 ps_intro | |
5 prove_lt_IZR | |
5 prZ3 | |
5 pp_inj_tri | |
5 pp | |
5 plus_le_compat | |
5 ph | |
5 p_exp | |
5 of | |
5 notogawa | |
5 not | |
5 nn | |
5 nat_of_ascii | |
5 mult_le_compat_r | |
5 mult_assoc_reverse | |
5 mult_1_l | |
5 msk | |
5 max | |
5 m0 | |
5 lt_wf_double_ind | |
5 lt_S_n | |
5 loop_sub_iter | |
5 lem12 | |
5 lem10 | |
5 lem1 | |
5 le_n_Sn | |
5 le_O_n | |
5 lazy | |
5 kozima | |
5 it | |
5 inj_S | |
5 in_cons | |
5 hb | |
5 has_lt_irrefl | |
5 ha | |
5 gt100 | |
5 for | |
5 first_false_ne_inv | |
5 field_simplify | |
5 f2Impl | |
5 even_double | |
5 equality | |
5 eqq | |
5 emit_code | |
5 double_mult | |
5 decide | |
5 convergent | |
5 com | |
5 coll_gen | |
5 atails | |
5 ascii | |
5 Zmult_lt_compat_r | |
5 Zmult_le_0_compat | |
5 Zeven | |
5 Zabs_Zopp | |
5 Z_zerop | |
5 Z_dec | |
5 ZL4 | |
5 Tri | |
5 TiA3 | |
5 TiA2 | |
5 TiA1 | |
5 Ti81 | |
5 Ti40 | |
5 Ti1 | |
5 T_T7 | |
5 Streams | |
5 Str_nth_S | |
5 Ring | |
5 Pcompare_antisym | |
5 PI_tg | |
5 PIE3 | |
5 OgieKako | |
5 OAs | |
5 NM | |
5 Lists | |
5 Induction | |
5 IHt2 | |
5 IHp0 | |
5 IHk | |
5 Hhz | |
5 Hd | |
5 HS0 | |
5 HOddZ | |
5 HEvenZ | |
5 HDPos | |
5 Function | |
5 CompOpp | |
5 Bool | |
5 Ascii | |
4 yoshihiro503 | |
4 y_nz_const | |
4 vBound | |
4 uu | |
4 us | |
4 union_assoc | |
4 trailing_zeros_mult | |
4 trailing_zeros_equation | |
4 tmiya_ | |
4 the | |
4 t61 | |
4 t60 | |
4 t41 | |
4 t40 | |
4 t20 | |
4 square_equiv | |
4 sqpos | |
4 skip_inv | |
4 sb | |
4 s3 | |
4 rename | |
4 reals_sample | |
4 psubz | |
4 prop_prime_dec | |
4 proj1_sig | |
4 prod_prop | |
4 prime_mult | |
4 prime_factor | |
4 prZ3em | |
4 prZ2 | |
4 pqpz_extract | |
4 pqpz_destruct | |
4 powzero | |
4 powmul_a | |
4 pow_mon | |
4 plus_le_compat_l | |
4 plus | |
4 pl | |
4 pa | |
4 ok | |
4 odd_even_plus | |
4 obj | |
4 new_ys_tail | |
4 natlike_ind | |
4 nat_of_P_o_P_of_succ_nat_eq_succ | |
4 mult_succ_l | |
4 mult_1_r | |
4 main | |
4 lt_div2 | |
4 lt_S_dec | |
4 lem | |
4 le_ind | |
4 le_gt_dec | |
4 le_S_n | |
4 into | |
4 intersect_empty_r | |
4 induction_ltof1 | |
4 in_eq | |
4 iaf_O_or_plus | |
4 golf | |
4 garriguejej | |
4 g7 | |
4 g6 | |
4 g5 | |
4 g4 | |
4 g3 | |
4 find | |
4 f_dec | |
4 f7 | |
4 f6 | |
4 f5 | |
4 f4 | |
4 ex_take | |
4 even_even_plus | |
4 eq2 | |
4 eq | |
4 eo | |
4 embzn | |
4 double_mult2 | |
4 double_S | |
4 dive | |
4 destruct_square | |
4 dec_ind | |
4 dd | |
4 conv | |
4 coll_raw | |
4 break | |
4 bezout_rel_prime | |
4 autocol | |
4 ascii_of_nat | |
4 ab | |
4 _is_y | |
4 Zwf_up | |
4 Zpower_mul_dist | |
4 Zpos_plus_distr | |
4 Zplus_0_r | |
4 Zmult_lt_compat_l | |
4 Zlt_neg_0 | |
4 Zle_or_lt | |
4 Zle_lt_trans | |
4 Zle_ge | |
4 Zgt_pos_0 | |
4 Zge_le | |
4 Zgcd | |
4 Zdiv_eucl | |
4 XD | |
4 Ti43 | |
4 Ti42 | |
4 Ti41 | |
4 Ti2 | |
4 T2toT_ | |
4 SumOdd_Is_Square | |
4 Stream | |
4 Str_nth_map | |
4 Str_nth_O | |
4 Square_lemma | |
4 S_last_false_inv | |
4 Rlt_gt | |
4 Recdef | |
4 P_all_k | |
4 PI_ineq | |
4 PI_RGT_3_05 | |
4 PF | |
4 O_or_S | |
4 Morphism | |
4 Mat | |
4 M_ind1 | |
4 L1 | |
4 IHs | |
4 IHCs0 | |
4 HysTail | |
4 Hsuf0 | |
4 HinShort | |
4 Hi | |
4 Hhy | |
4 Heqa | |
4 HeqB | |
4 HRelPrimeXY | |
4 HQ | |
4 HLPO | |
4 HICD | |
4 HH2 | |
4 HEvenY | |
4 HDivY | |
4 HDivX | |
4 HBEven2 | |
4 H11 | |
4 Finite_Cantor_Bernstein_Schroeder | |
4 Check | |
4 Ascii8 | |
4 0as | |
3 y_incr_z | |
3 xy | |
3 wp | |
3 well_founded_ind | |
3 we | |
3 union_total_l | |
3 u2 | |
3 u1 | |
3 trailing_zeros_2n | |
3 tmp8 | |
3 tmp5 | |
3 tmp4 | |
3 tailsF | |
3 t0_1 | |
3 surj_lemma | |
3 struct | |
3 stackmachine_app | |
3 ss | |
3 square_is_O | |
3 sql2 | |
3 sql0 | |
3 smaller | |
3 skip_id | |
3 sigma | |
3 rel_prime_sym_iff | |
3 rel_prime_square_iff_l | |
3 r1 | |
3 pzn | |
3 pz_pq_id | |
3 proved | |
3 pq_pz_id | |
3 pp4 | |
3 powpow | |
3 pow_mono_strict | |
3 pow_hom | |
3 pow2_lt_O | |
3 polyMultCons | |
3 plus_lt_compat_l | |
3 plus_le_compat_r | |
3 plt_lt | |
3 p_p2n1 | |
3 p_fin_prod2 | |
3 os | |
3 odds | |
3 odd_prime_ge_3 | |
3 odd_mult | |
3 o0 | |
3 ntheq_eqst | |
3 nth_from | |
3 not_lt_and_le | |
3 not_gt | |
3 not_ge | |
3 nat_of_P_mult_morphism | |
3 nat_of_P_inj | |
3 mult_pow | |
3 mult_is_O_r | |
3 minus | |
3 m2p | |
3 ltof | |
3 lt_trans | |
3 lt_not_le | |
3 lt_le_S | |
3 lt_first_prop | |
3 lt_first_inv | |
3 lt_eq_lt_dec | |
3 loop_sub | |
3 loop_h | |
3 loopK | |
3 log2 | |
3 lh | |
3 lem8 | |
3 lem7 | |
3 lem4 | |
3 lem3 | |
3 lem2 | |
3 lem11 | |
3 le_refl | |
3 le_plus_r | |
3 le_plus_l | |
3 le_n_S | |
3 le_aux | |
3 le100_rec | |
3 kt3k | |
3 kg6y_ucd | |
3 intersect_union_distr_r | |
3 intersect_total_l | |
3 intersect_empty_l | |
3 inj_le | |
3 inc_s | |
3 inc | |
3 iaf_stay | |
3 iaf_is_O | |
3 hy2 | |
3 hs | |
3 have | |
3 h_inv | |
3 h_id | |
3 guess | |
3 generalNats | |
3 gen_prop | |
3 g75 | |
3 g43 | |
3 g10 | |
3 f57 | |
3 f34 | |
3 f01 | |
3 even_square | |
3 even_mult_aux | |
3 even_2n | |
3 even_2 | |
3 eq_Finalmat | |
3 elt | |
3 double_elim | |
3 dom_le_rng | |
3 decoder_neq | |
3 decoder_eq | |
3 d_even | |
3 constructive_indefinite_description_nat | |
3 compile2 | |
3 cols | |
3 ce | |
3 cardauto2 | |
3 card_empty | |
3 bool | |
3 beq | |
3 base_prop | |
3 aux | |
3 autof | |
3 app_nil_end | |
3 app | |
3 andb_prop | |
3 acc | |
3 Ztrichotomy | |
3 Zpower_exp | |
3 Zplus_eq_compat | |
3 Zodd_mult_Zodd | |
3 Zmult_plus_distr_r | |
3 Zmult_le_compat_r | |
3 Zmult_le_compat_l | |
3 Zmult_integral_l | |
3 Zmult_1_l | |
3 Zmult_0_r | |
3 Zle_lt_or_eq | |
3 Zeven_mult_Zeven_l | |
3 Zdivide_trans | |
3 Zdivide_refl | |
3 Zdivide_factor_l | |
3 Zabs_Zmult | |
3 Z_lt_ge_dec | |
3 ZNP | |
3 Z3 | |
3 Z0 | |
3 W1 | |
3 Utf8 | |
3 Ti72 | |
3 Ti71 | |
3 Ti11 | |
3 Ti10 | |
3 Sumbool | |
3 Str_nth_tl | |
3 Sql1 | |
3 Some_surj | |
3 S_last_false_lt_S_n_inv | |
3 S_last_false_increasing | |
3 S_all | |
3 Rsqr | |
3 Rplus_0_l | |
3 Rmult_lt_reg_l | |
3 Rmult_assoc | |
3 Rlt_le_trans | |
3 Rlt_0_1 | |
3 Rinv_r | |
3 Rinv_0_lt_compat | |
3 R_ack_inj | |
3 R_ack_S_S | |
3 R_ack_S_O | |
3 Pplus_comm | |
3 Pplus | |
3 Pn | |
3 Pminus | |
3 PMP | |
3 PIE | |
3 Mult | |
3 Mn_n | |
3 Mn_cont | |
3 M_ind2 | |
3 M91_mono | |
3 M91_Lt | |
3 M91 | |
3 L0 | |
3 Injective_Le | |
3 IHt0_2 | |
3 IHp1 | |
3 IHo1 | |
3 IHn1 | |
3 IHn0 | |
3 IHb | |
3 IH | |
3 Hp | |
3 Hhyp1 | |
3 Hhyp | |
3 HeqA | |
3 HZPosOrZero | |
3 HYYPos | |
3 HRelPrimeYZ | |
3 HRP | |
3 HPosX | |
3 HOddY | |
3 HModA | |
3 HI2 | |
3 HDiv2 | |
3 HDiv1 | |
3 HB4 | |
3 HB3 | |
3 Gt | |
3 FLTred_div | |
3 F | |
3 Cs0 | |
3 ConstructiveEpsilon | |
3 Cons | |
3 ColS | |
3 Ack1 | |
3 9 | |
3 3intro | |
2 zup | |
2 z3 | |
2 z2 | |
2 ys_tail | |
2 yokoyama | |
2 y_nz_P | |
2 ySn_zero_Pn | |
2 x_is_one | |
2 x_is_odd | |
2 x_is_nonneg | |
2 x_is_even | |
2 wf_proof | |
2 wf_is_wf | |
2 wf_Mn2 | |
2 wf_Mn1 | |
2 well_founded_ltof | |
2 vt | |
2 vh | |
2 ve | |
2 vb_and_ab_then_ok | |
2 vb | |
2 union_intersect_distr_l | |
2 union_empty_l | |
2 union_complement_r | |
2 union_complement_l | |
2 union_comm | |
2 type_ind | |
2 tree_height_ind_strong | |
2 tree_height_ind_limit | |
2 toaru_y | |
2 toaru_x | |
2 tmp9 | |
2 tmp7 | |
2 tmp3 | |
2 tmp10 | |
2 tl | |
2 thm | |
2 theorem | |
2 than | |
2 table | |
2 t311 | |
2 t310 | |
2 t05 | |
2 t04 | |
2 t03 | |
2 t02 | |
2 sumdec_flat | |
2 sub_z | |
2 sub_s | |
2 sub2 | |
2 sub1 | |
2 sub | |
2 square_nonneg | |
2 sqpos2 | |
2 sql1 | |
2 sq_even | |
2 some | |
2 skip_lem | |
2 seven | |
2 setoid_replace | |
2 set_eq_trans | |
2 set_eq_sym | |
2 set_eq_refl | |
2 sd_odd | |
2 sc | |
2 s_pos_dec | |
2 rel_prime_plus_rev_l | |
2 rel_prime_plus_l | |
2 rel_prime_greater_irrefl | |
2 refl_equal | |
2 r2 | |
2 psub3 | |
2 psub2 | |
2 psub10 | |
2 psub1 | |
2 psn | |
2 prop_to_type_neg | |
2 projT2 | |
2 proj2_sig | |
2 prime_factor_odd | |
2 primeMeaningEqual | |
2 pred | |
2 pp3_5 | |
2 pp3_4 | |
2 pp3_3 | |
2 pp3_2 | |
2 pp3_1 | |
2 pp2 | |
2 pp1 | |
2 powmul_e | |
2 powle_e | |
2 powle_a | |
2 pow_plus | |
2 pow_mult | |
2 pow_mono_strict_conv | |
2 pow_mono_conv | |
2 pow_mono_base | |
2 pow_is_big | |
2 pow_hom_base | |
2 pow_assoc | |
2 polyPowCons | |
2 polyPlusWork | |
2 polyMultWork | |
2 polyMult2 | |
2 polyCalc2 | |
2 poly | |
2 pm | |
2 plus_n_Sm | |
2 plus_Sn_m | |
2 pirapira | |
2 php0 | |
2 php | |
2 perfect_square_dec_strong | |
2 pell_eq | |
2 pair_lem | |
2 p_p2n4 | |
2 p_p2n3 | |
2 p_fin_prod | |
2 p_fin_inj | |
2 p_exp_aux | |
2 p4 | |
2 p3 | |
2 on | |
2 nth_sq2 | |
2 nth_sq1 | |
2 nth_scanl_sum | |
2 nth_from_S | |
2 npair_wf_ind | |
2 not_prime_divide | |
2 not_inj_S | |
2 natlike_rec | |
2 nat_scope | |
2 n00 | |
2 mult_lt_compat | |
2 mult_2_eq | |
2 minv | |
2 minus_sum | |
2 map_length | |
2 lt_wf | |
2 lt_true_upto_wf | |
2 lt_true_upto_prop | |
2 lt_true_upto_lt | |
2 lt_true_upto_exists | |
2 lt_true_upto_acc_pred | |
2 lt_true_upto_acc | |
2 lt_true_upto_S | |
2 lt_true_upto_O | |
2 lt_tg | |
2 lt_le_weak | |
2 lt_first_wf | |
2 lt_first_S | |
2 lt_first_O | |
2 lt_first_Acc | |
2 lt_decidable | |
2 loop_sub0 | |
2 loopK_2 | |
2 loopK_1 | |
2 list_to_option | |
2 lem9 | |
2 lem17 | |
2 lem16 | |
2 lem15 | |
2 lem14 | |
2 le_n4_pow | |
2 le_Sn_le | |
2 le_SS | |
2 le101_srec | |
2 konn | |
2 ixss | |
2 is_prime_true | |
2 is_prime_ind | |
2 is_prime_false | |
2 intersectl_intersectl2 | |
2 intersect_union_distr_l | |
2 intersect_complement_r | |
2 intersect_complement_l | |
2 instantiate | |
2 inc_s_aux | |
2 ifcols | |
2 ifcol1 | |
2 icd | |
2 iaf_increasing_fst | |
2 iaf_increasing | |
2 iaf_gt_i | |
2 hy3 | |
2 hy1 | |
2 hd | |
2 gf_id_ZA | |
2 gf_id_A8 | |
2 gf_id_85 | |
2 gf_id_53 | |
2 gf_id_30 | |
2 generalScanl | |
2 fourier | |
2 first_false_prop | |
2 first_false_keeps | |
2 first_false_equation | |
2 first_false_eq_inv | |
2 first_false_eq | |
2 fibnext | |
2 fib_lem | |
2 fib_eq_aux | |
2 fib_eq | |
2 fg_id_AZ | |
2 fg_id_8A | |
2 fg_id_58 | |
2 fg_id_35 | |
2 fg_id_03 | |
2 fb | |
2 facts | |
2 fa | |
2 f3_ | |
2 f2_ | |
2 f00 | |
2 exsP | |
2 exp | |
2 evsq | |
2 even_r | |
2 even_2n_mult | |
2 eval_partial | |
2 eval1 | |
2 esum_app | |
2 erutuf | |
2 eqst | |
2 eq3 | |
2 eps | |
2 e4 | |
2 dy | |
2 double_mult_2 | |
2 divi_dec | |
2 distr | |
2 discrR | |
2 different | |
2 dec_lt | |
2 dec_ind2 | |
2 d2 | |
2 construct | |
2 cons_sl | |
2 compiler_list | |
2 compiler_intro | |
2 coll_add | |
2 cofix | |
2 char | |
2 card_prod_comm | |
2 card_distr | |
2 canonical_injection | |
2 c2 | |
2 c1 | |
2 c0 | |
2 bounded_ind | |
2 bigger_2n | |
2 below2forever | |
2 b_all | |
2 and | |
2 add_prop | |
2 about | |
2 ab_sub2 | |
2 a_ring2 | |
2 a_ring | |
2 a_dec | |
2 aP2N | |
2 a2_le_4a | |
2 _x0 | |
2 Zwf_well_founded | |
2 Ztrichotomy_inf | |
2 Zsqrt_2 | |
2 Zsqrt | |
2 Zpos_minus_morphism | |
2 Zpos_eq_rev | |
2 Zpos_eq_Z_of_nat_o_nat_of_P | |
2 Zplus_reg_l | |
2 Zplus_comm | |
2 Zplus_assoc | |
2 Zorder | |
2 Zopp_plus_distr | |
2 Zopp_inj | |
2 Zodd_plus_Zodd | |
2 Zodd_not_Zeven | |
2 Zodd_div2 | |
2 Zmult_assoc | |
2 Zmult_1_r | |
2 Zminus_plus | |
2 Zminus_eq | |
2 Zlt_upper_bound_ind2 | |
2 Zlt_upper_bound_ind | |
2 Zlt_square_simpl | |
2 Zlt_not_le | |
2 Zlt_le_trans | |
2 Zlt_irrefl | |
2 Zlt_gt | |
2 Zle_trans | |
2 Zle_not_gt | |
2 Zge | |
2 Zeq_minus | |
2 Zdivide_intro | |
2 Zdivide_0 | |
2 Zcompare_plus_compat | |
2 Zabs_triangle | |
2 Zabs_eq | |
2 Z_of_nat_exists | |
2 Z_le_gt_dec | |
2 Z_ge_lt_dec | |
2 ZZ | |
2 ZD | |
2 Z2 | |
2 XX | |
2 T_T2 | |
2 SucCol | |
2 Sql2 | |
2 Setoid | |
2 S_last_false_le_S_n | |
2 SRT | |
2 Rplus_lt_reg_r | |
2 Rplus_lt_compat | |
2 Rplus_eq_compat_l | |
2 Rmult_lt_0_compat | |
2 Rmult_le_compat_r | |
2 Rmult_eq_compat_l | |
2 Rmult_comm | |
2 Rmult_1_l | |
2 Rminus_gt | |
2 Rminus | |
2 Rlt_irrefl | |
2 Rle_not_lt | |
2 Rle_0_sqr | |
2 Rgt_not_eq | |
2 Rdiv | |
2 R_ack_set | |
2 R_ack_O | |
2 Pt | |
2 Prop2Type | |
2 Pmult_plus_distr_r | |
2 Pmult_plus_distr_l | |
2 Pminus_mask | |
2 Plus | |
2 Pf | |
2 Pdouble_minus_one | |
2 Pcompare | |
2 Pair_lt_Acc | |
2 P2T | |
2 NN | |
2 Mn_none | |
2 Mn_n_aux | |
2 Mn_conv_none | |
2 MAX_SEARCH_DEPTH | |
2 M91_invX | |
2 M91_invN | |
2 M91_S | |
2 L_Collatz | |
2 LOOP | |
2 LL | |
2 LEDec | |
2 Infix | |
2 Icomp2 | |
2 Icomp1 | |
2 IL | |
2 IHx0 | |
2 IHve | |
2 IHscard | |
2 IHo | |
2 IHle | |
2 IHinit_n | |
2 IHf | |
2 IHd0 | |
2 IHc | |
2 IHRLE | |
2 IHOAs | |
2 ICD_LPO_Proof | |
2 ICDH | |
2 I2L | |
2 Ht | |
2 Hr | |
2 Hodd | |
2 Hm | |
2 HhyhzRelPrime | |
2 Hhxd | |
2 Hhx | |
2 Hhb | |
2 Hha | |
2 Hg3 | |
2 Hg2 | |
2 Hg1 | |
2 Hfalse | |
2 Hf | |
2 Heven_n | |
2 Heven_m | |
2 Heven | |
2 Heqx | |
2 Heql | |
2 Heq_2 | |
2 Heq_1 | |
2 HeqOAs | |
2 HeqCMP2 | |
2 Hdiv2_n | |
2 Hdiv2_m | |
2 Hdiv2S | |
2 Hb | |
2 H_height_or | |
2 H_height_eq | |
2 H_height | |
2 HZOddY | |
2 HZA | |
2 HZ | |
2 HY | |
2 HWPos2 | |
2 HWPos | |
2 HSPos | |
2 HRelPrimeYYZ | |
2 HRPos | |
2 HPB | |
2 HOddYY | |
2 HOddXX | |
2 HOddA | |
2 HGCD | |
2 HFE | |
2 HF | |
2 HEvenZpY | |
2 HEvenZmY | |
2 HEvenA | |
2 HE | |
2 HBOdd | |
2 HBEvenOddDec | |
2 HBEven | |
2 HB2 | |
2 HB1 | |
2 HAZ | |
2 HA8 | |
2 H8A | |
2 H85 | |
2 H58 | |
2 H53 | |
2 H35 | |
2 H30 | |
2 H03 | |
2 Fourier | |
2 FMapAVL | |
2 FLT4 | |
2 ET | |
2 E | |
2 Decn | |
2 ColU | |
2 ColO | |
2 ColF | |
2 ColE | |
2 CoFixpoint | |
2 C_Collatz | |
2 B_ | |
2 BB | |
2 B0 | |
2 Ack2 | |
2 Aadd | |
2 AA | |
2 A0 | |
2 99 | |
2 89 | |
2 316234143225 | |
2 25 | |
2 13 | |
2 0x | |
2 000 | |
1 zp | |
1 zero_or_S | |
1 yyy | |
1 yoshihiro503_witout_ring | |
1 xxx | |
1 wtakuo | |
1 write | |
1 without | |
1 why | |
1 well_founded_induction | |
1 version | |
1 value | |
1 until | |
1 union_total_r | |
1 union_same | |
1 union_intersect_distr_r | |
1 union_empty_r | |
1 union_comp | |
1 ucq | |
1 u0 | |
1 trans_EqSt | |
1 todo | |
1 tmp6 | |
1 thoery | |
1 this | |
1 test | |
1 terrible | |
1 tanakh | |
1 tail_recursive | |
1 sumbool_of_bool | |
1 sumbool_not | |
1 sum_map | |
1 sum_f_R0 | |
1 suharahiromichi | |
1 sub_lists_map | |
1 square_pos_iff | |
1 sqr_pos | |
1 simple | |
1 signature | |
1 sig | |
1 set_Setoid | |
1 sackry | |
1 s_equation | |
1 ring_Rsqr | |
1 reverse | |
1 result | |
1 rep | |
1 rel_prime_square_iff | |
1 rec | |
1 real | |
1 proposition | |
1 proof | |
1 prod | |
1 prime_odd_3_iff | |
1 prime_alt | |
1 pos | |
1 plus_permute | |
1 plus_n_O | |
1 plus_is_O | |
1 plus_assoc_reverse | |
1 plus_Snm_nSm | |
1 plus_O_n | |
1 parametricity | |
1 or_intror | |
1 or_introl | |
1 odd_mult_inv_l | |
1 not_rel_prime_0 | |
1 nonzero_succ | |
1 nofun | |
1 neq_x_c | |
1 n_Sn | |
1 mzp | |
1 mult_S_lt_compat_l | |
1 minus_n_O | |
1 memoized | |
1 map_ext | |
1 maeda_ | |
1 made | |
1 lt_n_S | |
1 lt_d0_x | |
1 lt_S | |
1 lt_0_INR | |
1 level | |
1 lemmata | |
1 le_x_d0 | |
1 le_plus_trans | |
1 le_n | |
1 le_max_r | |
1 le_max_l | |
1 le_Sn_O | |
1 kokomade | |
1 kokokara | |
1 koko | |
1 isomorphisms | |
1 intersect_total_r | |
1 intersect_same | |
1 intersect_comp | |
1 inj_plus | |
1 inj_lt_rev | |
1 inj_0 | |
1 inaniwa | |
1 in_inv | |
1 idea_from_xsd | |
1 idea_from_hirose | |
1 hypothesis | |
1 hy4 | |
1 here | |
1 gf_id_75 | |
1 gf_id_43 | |
1 gf_id_01 | |
1 gf6_id | |
1 gf5_id | |
1 gf4_id | |
1 gf3_id | |
1 gets | |
1 function | |
1 fresh | |
1 fold_right | |
1 finite | |
1 field_simplify_eq | |
1 fg_id_57 | |
1 fg_id_34 | |
1 fg_id_01 | |
1 fg6_id | |
1 fg5_id | |
1 fg4_id | |
1 fg3_id | |
1 faster | |
1 f2_ind | |
1 f2_equation | |
1 f0 | |
1 exsP0 | |
1 exm | |
1 even_plus_odd_inv_r | |
1 eq_x_c | |
1 eq_add_S | |
1 eq_S | |
1 eomole | |
1 enc_dec | |
1 eexists | |
1 econstructor | |
1 destruction | |
1 destruct_list | |
1 dec_inh_nat_subset_has_unique_least_element | |
1 dec_Zlt | |
1 debug | |
1 datatypes | |
1 cutrewrite | |
1 crossquare | |
1 continues | |
1 constrainted | |
1 complement_involutive | |
1 complement_comp | |
1 compatibility | |
1 commutative | |
1 collatz | |
1 clairvy | |
1 chirchir | |
1 card_sum_comm | |
1 card_sum_assoc | |
1 card_sum_antisym | |
1 card_prod_assoc | |
1 card_prod_antisym | |
1 card_comp | |
1 cannot | |
1 bon_ja | |
1 bigger | |
1 bh | |
1 be | |
1 basic | |
1 b_induction | |
1 b0 | |
1 associativity | |
1 anonymous | |
1 andb_false_elim | |
1 andb | |
1 all | |
1 ah | |
1 add | |
1 ab_sub1 | |
1 _x | |
1 Zwf_up_well_founded | |
1 Zpred | |
1 Zpower | |
1 Zpos_P_of_succ_nat | |
1 Zplus_opp_r | |
1 Zplus_minus_eq | |
1 Zplus_lt_compat_l | |
1 Zplus_lt_compat | |
1 Zplus_le_reg_l | |
1 Zplus_le_compat_r | |
1 Zopp | |
1 Znot_lt_ge | |
1 Zmult_reg_l | |
1 Zmult_plus_distr_l | |
1 Zmult_lt_reg_r | |
1 Zmult_lt_0_le_compat_r | |
1 Zmult_le_0_reg_r | |
1 Zmult_gt_reg_r | |
1 Zmult_gt_0_reg_l | |
1 Zmult_ge_compat_l | |
1 Zmult_divide_compat_r | |
1 Zmult_1_inversion_l | |
1 Zmod_unique | |
1 Zminus_succ_r | |
1 Zminus_plus_distr | |
1 Zminus_0_r | |
1 Zminus | |
1 Zlt_trans | |
1 Zlt_succ_le | |
1 Zlt_succ_gt | |
1 Zlt_succ | |
1 Zlt_le_succ | |
1 Zlt_0_ind | |
1 Zle_refl | |
1 Zle_not_lt | |
1 Zle_lt_succ | |
1 Zle_antisym | |
1 Zle | |
1 Zgt_lt | |
1 Zgt_le_succ | |
1 Zgcd_is_pos | |
1 Zgcd_is_gcd | |
1 Zgcd_inv_0_l | |
1 Zgcd_1_rel_prime | |
1 Zeven_plus_Zodd | |
1 Zeven_mult_Zeven_r | |
1 Zdivide_mult_l | |
1 Zdivide_factor_r | |
1 Zabs_nat_lt | |
1 Zabs_ind | |
1 Z_of_nat_prop | |
1 Z_lt_induction | |
1 Z_div_mod_full | |
1 Z_div_exact_2 | |
1 Z_as_OT | |
1 Z_Q_bijective_function | |
1 ZArith_dec | |
1 YYZ | |
1 Without | |
1 Variables | |
1 Ti22 | |
1 Ti21 | |
1 Ti20 | |
1 Think | |
1 Strong | |
1 Sort | |
1 So | |
1 Sn | |
1 Sinec | |
1 SetoidList | |
1 SearchPattern | |
1 Scheme | |
1 S_pred | |
1 Rplus_opp_l | |
1 Rplus_lt_pos | |
1 Rplus_lt_compat_r | |
1 Rplus_le_le_0_compat | |
1 Rplus_le_compat_r | |
1 Rplus_comm | |
1 Rplus_assoc | |
1 Rplus_0_r | |
1 Rmult_plus_distr_l | |
1 Rmult_lt_compat_r | |
1 Rmult_lt_compat_l | |
1 Rmult_le_pos | |
1 Rmult_le_compat_neg_l | |
1 Rmult_le_compat_l | |
1 Rmult_le_0_lt_compat | |
1 Rmult_1_r | |
1 Rmult_0_r | |
1 Rminus_diag_uniq_sym | |
1 Rlt_not_ge | |
1 Rlt_minus | |
1 Rlt_le_dec | |
1 Rle_refl | |
1 Rle_lt_trans | |
1 Rle_ge | |
1 Rle_0_1 | |
1 Rinv_1 | |
1 Rgt_ge | |
1 Rge_gt_trans | |
1 Remainder | |
1 Relation | |
1 RLE | |
1 Qeq | |
1 QArith | |
1 Proposition | |
1 Program | |
1 Print | |
1 Pn_ySn2 | |
1 Pn_ySn | |
1 Plt | |
1 Pgt | |
1 Pell | |
1 Pcompare_Eq_eq | |
1 PNZ | |
1 OrderedTypeEx | |
1 Opaque | |
1 O_S | |
1 Need | |
1 NArith | |
1 Module | |
1 Max | |
1 Mathematical | |
1 Make | |
1 Logic | |
1 J | |
1 IS | |
1 IHy | |
1 IHus | |
1 IHt0_1 | |
1 IHt | |
1 IHp | |
1 IHlt_first | |
1 IHl1 | |
1 IHi | |
1 IHe | |
1 IHa0 | |
1 IHCs | |
1 Hx | |
1 Hinit_n | |
1 HinLong | |
1 Hin1 | |
1 Hin0 | |
1 Hhyp2 | |
1 Here | |
1 Heqzz | |
1 Heqve | |
1 Heqsn | |
1 Heqmn | |
1 Heqg | |
1 Heqce | |
1 Heqbb | |
1 HeqSn | |
1 HeqAs | |
1 He | |
1 Hcorrect | |
1 Hcontradiction | |
1 Habsurd | |
1 H_height_lt_Sh | |
1 H_height_le_h | |
1 HYYPos2 | |
1 HX5 | |
1 HX4 | |
1 HRelPrimeXXYY | |
1 HRelPrimeXXY | |
1 HPosZ | |
1 HPosY | |
1 HPN | |
1 HPM | |
1 HOddX | |
1 HFPos | |
1 HB5 | |
1 HB3SS | |
1 H12 | |
1 Gauss | |
1 Functional | |
1 Fix | |
1 False_rec | |
1 Fact | |
1 FLTred_prime | |
1 DD | |
1 Compare_dec | |
1 Choice | |
1 CC | |
1 C2 | |
1 C1 | |
1 Bool_nat | |
1 BinInt | |
1 Basics | |
1 Assuming | |
1 Acc_inv | |
1 Acc_ind | |
1 98 | |
1 97 | |
1 96451413683625 | |
1 96 | |
1 95 | |
1 94 | |
1 93 | |
1 92 | |
1 91with | |
1 8 | |
1 6 | |
1 42 | |
1 30 | |
1 241792844580 | |
1 1a | |
1 114 | |
1 0n |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment