matita.cs.unibo.it Git - helm.git/tree - matita/matita/contribs/lambdadelta/ground/arith/

drwxr-xr-x		..
-rw-r--r--	3503	arith_2a.ma	blob \| history \| raw
-rw-r--r--	2094	arith_2b.ma	blob \| history \| raw
-rw-r--r--	2280	arith_etc.txt	blob \| history \| raw
-rw-r--r--	1812	nat.ma	blob \| history \| raw
-rw-r--r--	357	nat_etc.txt	blob \| history \| raw
-rw-r--r--	2020	nat_iter.ma	blob \| history \| raw
-rw-r--r--	4207	nat_le.ma	blob \| history \| raw
-rw-r--r--	2630	nat_le_max.ma	blob \| history \| raw
-rw-r--r--	2599	nat_le_minus.ma	blob \| history \| raw
-rw-r--r--	4670	nat_le_minus_plus.ma	blob \| history \| raw
-rw-r--r--	3729	nat_le_plus.ma	blob \| history \| raw
-rw-r--r--	2145	nat_le_pred.ma	blob \| history \| raw
-rw-r--r--	4916	nat_lt.ma	blob \| history \| raw
-rw-r--r--	2385	nat_lt_minus.ma	blob \| history \| raw
-rw-r--r--	2116	nat_lt_minus_plus.ma	blob \| history \| raw
-rw-r--r--	1987	nat_lt_plus.ma	blob \| history \| raw
-rw-r--r--	2335	nat_lt_pred.ma	blob \| history \| raw
-rw-r--r--	1566	nat_lt_tri.ma	blob \| history \| raw
-rw-r--r--	2749	nat_max.ma	blob \| history \| raw
-rw-r--r--	2540	nat_minus.ma	blob \| history \| raw
-rw-r--r--	2860	nat_minus_plus.ma	blob \| history \| raw
-rw-r--r--	4565	nat_plus.ma	blob \| history \| raw
-rw-r--r--	1877	nat_plus_pred.ma	blob \| history \| raw
-rw-r--r--	1978	nat_pred.ma	blob \| history \| raw
-rw-r--r--	1533	nat_pred_succ.ma	blob \| history \| raw
-rw-r--r--	2813	nat_succ.ma	blob \| history \| raw
-rw-r--r--	1323	nat_succ_iter.ma	blob \| history \| raw
-rw-r--r--	1612	nat_succ_tri.ma	blob \| history \| raw
-rw-r--r--	2336	nat_tri.ma	blob \| history \| raw
-rw-r--r--	2042	pnat.ma	blob \| history \| raw
-rw-r--r--	2449	pnat_iter.ma	blob \| history \| raw
-rw-r--r--	1900	pnat_plus.ma	blob \| history \| raw
-rw-r--r--	1214	pnat_split.ma	blob \| history \| raw
-rw-r--r--	2201	pnat_tri.ma	blob \| history \| raw
-rw-r--r--	1557	wf1_ind_nlt.ma	blob \| history \| raw
-rw-r--r--	1592	wf1_ind_ylt.ma	blob \| history \| raw
-rw-r--r--	1642	wf2_ind_nlt.ma	blob \| history \| raw
-rw-r--r--	1725	wf3_ind_nlt.ma	blob \| history \| raw
-rw-r--r--	2032	ynat.ma	blob \| history \| raw
-rw-r--r--	3500	ynat_le.ma	blob \| history \| raw
-rw-r--r--	2244	ynat_le_lminus.ma	blob \| history \| raw
-rw-r--r--	4484	ynat_le_lminus_plus.ma	blob \| history \| raw
-rw-r--r--	1502	ynat_le_lminus_succ.ma	blob \| history \| raw
-rw-r--r--	3967	ynat_le_plus.ma	blob \| history \| raw
-rw-r--r--	1645	ynat_le_pred.ma	blob \| history \| raw
-rw-r--r--	2315	ynat_le_pred_succ.ma	blob \| history \| raw
-rw-r--r--	1959	ynat_le_succ.ma	blob \| history \| raw
-rw-r--r--	2472	ynat_lminus.ma	blob \| history \| raw
-rw-r--r--	1571	ynat_lminus_plus.ma	blob \| history \| raw
-rw-r--r--	1329	ynat_lminus_succ.ma	blob \| history \| raw
-rw-r--r--	3158	ynat_lt.ma	blob \| history \| raw
-rw-r--r--	3951	ynat_lt_le.ma	blob \| history \| raw
-rw-r--r--	1509	ynat_lt_le_lminus.ma	blob \| history \| raw
-rw-r--r--	1609	ynat_lt_le_lminus_plus.ma	blob \| history \| raw
-rw-r--r--	2749	ynat_lt_le_plus.ma	blob \| history \| raw
-rw-r--r--	1409	ynat_lt_le_pred.ma	blob \| history \| raw
-rw-r--r--	1458	ynat_lt_le_pred_succ.ma	blob \| history \| raw
-rw-r--r--	2067	ynat_lt_le_succ.ma	blob \| history \| raw
-rw-r--r--	2218	ynat_lt_lminus.ma	blob \| history \| raw
-rw-r--r--	1671	ynat_lt_lminus_plus.ma	blob \| history \| raw
-rw-r--r--	4085	ynat_lt_plus.ma	blob \| history \| raw
-rw-r--r--	2043	ynat_lt_plus_pred.ma	blob \| history \| raw
-rw-r--r--	1431	ynat_lt_pred.ma	blob \| history \| raw
-rw-r--r--	2176	ynat_lt_pred_succ.ma	blob \| history \| raw
-rw-r--r--	2310	ynat_lt_succ.ma	blob \| history \| raw
-rw-r--r--	2509	ynat_nat.ma	blob \| history \| raw
-rw-r--r--	6127	ynat_plus.ma	blob \| history \| raw
-rw-r--r--	2246	ynat_pred.ma	blob \| history \| raw
-rw-r--r--	1654	ynat_pred_succ.ma	blob \| history \| raw
-rw-r--r--	3559	ynat_succ.ma	blob \| history \| raw