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

drwxr-xr-x		..
-rw-r--r--	3417	arith_2a.ma	blob \| history \| raw
-rw-r--r--	2094	arith_2b.ma	blob \| history \| raw
-rw-r--r--	1824	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--	2022	nat_iter.ma	blob \| history \| raw
-rw-r--r--	4204	nat_le.ma	blob \| history \| raw
-rw-r--r--	2541	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--	3837	nat_le_plus.ma	blob \| history \| raw
-rw-r--r--	2296	nat_le_pred.ma	blob \| history \| raw
-rw-r--r--	5559	nat_lt.ma	blob \| history \| raw
-rw-r--r--	2983	nat_lt_minus.ma	blob \| history \| raw
-rw-r--r--	2116	nat_lt_minus_plus.ma	blob \| history \| raw
-rw-r--r--	2170	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--	2543	nat_minus.ma	blob \| history \| raw
-rw-r--r--	2875	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--	1599	nat_plus_rplus.ma	blob \| history \| raw
-rw-r--r--	2173	nat_pred.ma	blob \| history \| raw
-rw-r--r--	1942	nat_pred_succ.ma	blob \| history \| raw
-rw-r--r--	1546	nat_rplus.ma	blob \| history \| raw
-rw-r--r--	1475	nat_rplus_pplus.ma	blob \| history \| raw
-rw-r--r--	1662	nat_rplus_succ.ma	blob \| history \| raw
-rw-r--r--	3150	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--	2383	pnat.ma	blob \| history \| raw
-rw-r--r--	2449	pnat_iter.ma	blob \| history \| raw
-rw-r--r--	3848	pnat_le.ma	blob \| history \| raw
-rw-r--r--	1516	pnat_le_plus.ma	blob \| history \| raw
-rw-r--r--	2038	pnat_le_pred.ma	blob \| history \| raw
-rw-r--r--	5060	pnat_lt.ma	blob \| history \| raw
-rw-r--r--	1859	pnat_lt_plus.ma	blob \| history \| raw
-rw-r--r--	2221	pnat_lt_pred.ma	blob \| history \| raw
-rw-r--r--	2499	pnat_plus.ma	blob \| history \| raw
-rw-r--r--	1775	pnat_pred.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--	1228	pnat_two.ma	blob \| history \| raw
-rw-r--r--	1557	wf1_ind_nlt.ma	blob \| history \| raw
-rw-r--r--	1547	wf1_ind_plt.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--	2475	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--	6132	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