diff options
author | 2013-05-31 12:34:49 +0000 | |
---|---|---|
committer | 2013-05-31 12:34:49 +0000 | |
commit | 5f3115e9412cb3b955e5a79e6867bf949fa64c77 (patch) | |
tree | c2f13a4f0cf04818a98184d5d248c3f04b2277e9 /contrib/ML4PG | |
parent | 63eefb4027b9b59f7f91a6e4aaf1763790083e8f (diff) |
Authors of ML4PG
Diffstat (limited to 'contrib/ML4PG')
-rw-r--r-- | contrib/ML4PG/AUTHORS | 5 | ||||
-rw-r--r-- | contrib/ML4PG/lemmas.txt | 4 | ||||
-rw-r--r-- | contrib/ML4PG/views.txt | 2 |
3 files changed, 9 insertions, 2 deletions
diff --git a/contrib/ML4PG/AUTHORS b/contrib/ML4PG/AUTHORS new file mode 100644 index 00000000..ab62d039 --- /dev/null +++ b/contrib/ML4PG/AUTHORS @@ -0,0 +1,5 @@ +ML4PG was designed and written by Jonathan Heras and Ekaterina Komendantskaya. +<http://www.computing.dundee.ac.uk/staff/katya/ML4PG/>. + +Jonathan Heras <jonathanheras@computing.dundee.ac.uk> +Ekaterina Komendantskaya <katya@computing.dundee.ac.uk> diff --git a/contrib/ML4PG/lemmas.txt b/contrib/ML4PG/lemmas.txt index d6c69678..764aba29 100644 --- a/contrib/ML4PG/lemmas.txt +++ b/contrib/ML4PG/lemmas.txt @@ -52,4 +52,6 @@ fact0&102$muln1&103$IH&104$factS&105$mulnA&106$mulnC&107$helper_fact_is_theta&10 &122$_(0 <= i < n.+1)&123$x&124$@eq_bigr&125$@big1&126$GRing.subr_eq0&127$in&128$H1&129$eqP&130$GRing.Theory.sumrB&131$big_ltn&132$@big_add1&133$big_addn&134$H&135$ltn_predK&136$pred_Sn&137$subr_sub&138$subnDA&139$subnS&140$H4&141$addnBA&142$subnDl&143$lemma2_aux&144$subn_eq0&145$big_nil&146$leq_eqVlt&147$lemma1&148$lemma2'&149$lemma2&150$h'&151$mulVmx&152$mulmx1&153$mulmxV&154$mulmxA&155$invmx_left&156$mul1mx&157$/pot_matrix&158$thinmx0&159$det1&160$det0&161$mulmxBr&162$pot_1&163$big_nat_recl&164$big_nat_recr &165$submx_sub&166$GRing.sub0r&167$p&168$addSn&100.1$plus_Sn_m&100.14999999999999$plus_n_Sm&100.175$addSn&100.1$plus_Sn_m&100.14999999999999$plus_n_Sm&100.175$app_nil_l2&100.1875$mult_n_O&100.19375$O_minus&100.19687499999999$mult_O_n&100.1984375$plus_n_O&100.19921875$aux12&100.199609375$aux7&100.19980468749999$aux10&100.19990234375$mulSn&100.199951171875$aux11&100.1999755859375$mulnS&100.19998779296874$andb_false_r&100.19999389648437$addSn&100.1$plus_Sn_m&100.14999999999999$plus_n_Sm&100.175$app_nil_l2&100.1875$mult_n_O&100.19375$O_minus&100.19687499999999$mult_O_n&100.1984375$plus_n_O&100.19921875$aux12&100.199609375$aux7&100.19980468749999$aux10&100.19990234375$mulSn&100.199951171875$aux11&100.1999755859375$mulnS&100.19998779296874$andb_false_r&100.19999389648437$addSn&100.1$plus_Sn_m&100.14999999999999$plus_n_Sm&100.175$app_nil_l2&100.1875$mult_n_O&100.19375$O_minus&100.19687499999999$mult_O_n&100.1984375$plus_n_O&100.19921875$aux12&100.199609375$aux7&100.19980468749999$aux10&100.19990234375$mulSn&100.199951171875$aux11&100.1999755859375$mulnS&100.19998779296874$andb_false_r&100.19999389648437$mul0n&102$big_nat1&103$muln0&104$big_nat_recr&105$mulnDr&106$IH&107$exp0n&108$big1_seq&109$in_nil&110$big_mkcond&111$muln1&112$addn2&113$mul1n&114$GRing.subr_eq&115$GRing.addrA&116$GRing.addrC&117$GRing&118$addrA&119$sumrB&120$@big_nat_recl&121$addrC &122$_(0 <= i < n.+1)&123$x&124$@eq_bigr&125$@big1&126$GRing.subr_eq0&127$in&128$H1&129$eqP&130$GRing.Theory.sumrB&131$big_ltn&132$@big_add1&133$big_addn&134$H&135$ltn_predK&136$pred_Sn&137$subr_sub&138$subnDA&139$subnS&140$H4&141$addnBA&142$subnDl&143$lemma2_aux&144$subn_eq0&145$big_nil&146$leq_eqVlt&147$lemma1&148$lemma2'&149$lemma2&150$h'&151$mulVmx&152$mulmx1&153$mulmxV&154$mulmxA&155$invmx_left&156$mul1mx&157$/pot_matrix&158$thinmx0&159$det1&160$det0&161$mulmxBr&162$pot_1&163$big_nat_recl&164$big_nat_recr -&165$submx_sub&166$GRing.sub0r&167$p&168$addSn&100.1$plus_Sn_m&100.14999999999999$plus_n_Sm&100.175$app_nil_l2&100.1875$mult_n_O&100.19375$O_minus&100.19687499999999$mult_O_n&100.1984375$plus_n_O&100.19921875$aux12&100.199609375$aux7&100.19980468749999$aux10&100.19990234375$mulSn&100.199951171875$aux11&100.1999755859375$mulnS&100.19998779296874$andb_false_r&100.19999389648437$
\ No newline at end of file +&165$submx_sub&166$GRing.sub0r&167$p&168$addSn&100.1$plus_Sn_m&100.14999999999999$plus_n_Sm&100.175$app_nil_l2&100.1875$mult_n_O&100.19375$O_minus&100.19687499999999$mult_O_n&100.1984375$plus_n_O&100.19921875$aux12&100.199609375$aux7&100.19980468749999$aux10&100.19990234375$mulSn&100.199951171875$aux11&100.1999755859375$mulnS&100.19998779296874$andb_false_r&100.19999389648437$mul0n&102$big_nat1&103$muln0&104$big_nat_recr&105$mulnDr&106$IH&107$exp0n&108$big1_seq&109$in_nil&110$big_mkcond&111$muln1&112$addn2&113$mul1n&114$GRing.subr_eq&115$GRing.addrA&116$GRing.addrC&117$GRing&118$addrA&119$sumrB&120$@big_nat_recl&121$addrC +&122$_(0 <= i < n.+1)&123$x&124$@eq_bigr&125$@big1&126$GRing.subr_eq0&127$in&128$H1&129$eqP&130$GRing.Theory.sumrB&131$big_ltn&132$@big_add1&133$big_addn&134$H&135$ltn_predK&136$pred_Sn&137$subr_sub&138$subnDA&139$subnS&140$H4&141$addnBA&142$subnDl&143$lemma2_aux&144$subn_eq0&145$big_nil&146$leq_eqVlt&147$lemma1&148$lemma2'&149$lemma2&150$h'&151$mulVmx&152$mulmx1&153$mulmxV&154$mulmxA&155$invmx_left&156$mul1mx&157$/pot_matrix&158$thinmx0&159$det1&160$det0&161$mulmxBr&162$pot_1&163$big_nat_recl&164$big_nat_recr +&165$submx_sub&166$GRing.sub0r&167$p&168$
\ No newline at end of file diff --git a/contrib/ML4PG/views.txt b/contrib/ML4PG/views.txt index 016fdc79..4b8dfa6a 100644 --- a/contrib/ML4PG/views.txt +++ b/contrib/ML4PG/views.txt @@ -1 +1 @@ -theta_fact&102$fn_fact&103$theta_fact&102$fn_fact&103$theta_fact&102$fn_fact&103$gtn_eqF&102$ltnW&103$implyP&104$leP:&105$eqnP&106$leq_trans&107$subnBA->&108$addnBA&109$subSn&110$leq_sub2r&111$leq_sub2l&112$subnSK&113$maxn&114$maxn_idPl&115$minn&116$minn_idPl&117$minn_idPr/leq_maxl&118$minn_idPl/leq_maxr&119$maxn_idPr/geq_minl&120$maxn_idPl/geq_minr&121$orP:&122$minn_idPr&123$ex_minn&124$ex_maxn&125$prednK&126$leq_pmull&127$leq&128$subnK&129$leqifP&130$leqif&131$eqP:&132$leqif_refl&133$rowP&102$1&103$drlower1&104$invmx_uniq&105$rowP&102$1&103$drlower1&104$invmx_uniq&105$fn_fact&102$b&106$a&107$pot_matrix&108$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$theta_fact&102$fn_fact&103$fn_fact&102$theta_fact&103$fn_fact&104$theta_fact&102$fn_fact&103$fn_fact&102$theta_fact&102$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$theta_fact&102$fn_fact&103$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$gtn_eqF&102$ltnW&103$implyP&104$leP:&105$eqnP&106$leq_trans&107$subnBA->&108$addnBA&109$subSn&110$leq_sub2r&111$leq_sub2l&112$subnSK&113$maxn&114$maxn_idPl&115$minn&116$minn_idPl&117$minn_idPr/leq_maxl&118$minn_idPl/leq_maxr&119$maxn_idPr/geq_minl&120$maxn_idPl/geq_minr&121$orP:&122$minn_idPr&123$ex_minn&124$ex_maxn&125$prednK&126$leq_pmull&127$leq&128$subnK&129$leqifP&130$monotone_leqif&131$eqP:&132$leqif_refl&133$leq_pmul2l:&134$Mn1:&135$leq_pmul2r:&136$Mm2:&137$gtn_eqF&102$ltnW&103$implyP&104$leP:&105$eqnP&106$leq_trans&107$subnBA->&108$addnBA&109$subSn&110$leq_sub2r&111$leq_sub2l&112$subnSK&113$maxn&114$maxn_idPl&115$minn&116$minn_idPl&117$minn_idPr/leq_maxl&118$minn_idPl/leq_maxr&119$maxn_idPr/geq_minl&120$maxn_idPl/geq_minr&121$orP:&122$minn_idPr&123$ex_minn&124$ex_maxn&125$prednK&126$leq_pmull&127$leq&128$subnK&129$leqifP&130$monotone_leqif&131$eqP:&132$leqif_refl&133$leq_pmul2l:&134$Mn1:&135$leq_pmul2r:&136$Mm2:&137$gtn_eqF&102$ltnW&103$implyP&104$leP:&105$eqnP&106$leq_trans&107$subnBA->&108$addnBA&109$subSn&110$leq_sub2r&111$leq_sub2l&112$subnSK&113$maxn&114$maxn_idPl&115$minn&116$minn_idPl&117$minn_idPr/leq_maxl&118$minn_idPl/leq_maxr&119$maxn_idPr/geq_minl&120$maxn_idPl/geq_minr&121$orP:&122$minn_idPr&123$ex_minn&124$ex_maxn&125$prednK&126$leq_pmull&127$leq&128$subnK&129$leqifP&130$monotone_leqif&131$eqP:&132$leqif_refl&133$leq_pmul2l:&134$Mn1:&135$leq_pmul2r:&136$Mm2:&137$gtn_eqF&102$ltnW&103$implyP&104$leP:&105$eqnP&106$leq_trans&107$subnBA->&108$addnBA&109$subSn&110$leq_sub2r&111$leq_sub2l&112$subnSK&113$maxn&114$maxn_idPl&115$minn&116$minn_idPl&117$minn_idPr/leq_maxl&118$minn_idPl/leq_maxr&119$maxn_idPr/geq_minl&120$maxn_idPl/geq_minr&121$orP:&122$minn_idPr&123$ex_minn&124$ex_maxn&125$prednK&126$leq_pmull&127$leq&128$subnK&129$leqifP&130$monotone_leqif&131$eqP:&132$leqif_refl&133$leq_pmul2l:&134$Mn1:&135$leq_pmul2r:&136$Mm2:&137$lastP:&102$perm_to_rem/(eq_big_perm _)->&103$eq_big_perm&104$big_rem->&105$rem_filter->&106$IHn&107$familyP&108$ffunP&109$eqP/Df&110$IHr&111$familyP/(_ i)&112$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$b&102$a&103$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$
\ No newline at end of file +theta_fact&102$fn_fact&103$theta_fact&102$fn_fact&103$theta_fact&102$fn_fact&103$gtn_eqF&102$ltnW&103$implyP&104$leP:&105$eqnP&106$leq_trans&107$subnBA->&108$addnBA&109$subSn&110$leq_sub2r&111$leq_sub2l&112$subnSK&113$maxn&114$maxn_idPl&115$minn&116$minn_idPl&117$minn_idPr/leq_maxl&118$minn_idPl/leq_maxr&119$maxn_idPr/geq_minl&120$maxn_idPl/geq_minr&121$orP:&122$minn_idPr&123$ex_minn&124$ex_maxn&125$prednK&126$leq_pmull&127$leq&128$subnK&129$leqifP&130$leqif&131$eqP:&132$leqif_refl&133$rowP&102$1&103$drlower1&104$invmx_uniq&105$rowP&102$1&103$drlower1&104$invmx_uniq&105$fn_fact&102$b&106$a&107$pot_matrix&108$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$theta_fact&102$fn_fact&103$fn_fact&102$theta_fact&103$fn_fact&104$theta_fact&102$fn_fact&103$fn_fact&102$theta_fact&102$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$theta_fact&102$fn_fact&103$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$gtn_eqF&102$ltnW&103$implyP&104$leP:&105$eqnP&106$leq_trans&107$subnBA->&108$addnBA&109$subSn&110$leq_sub2r&111$leq_sub2l&112$subnSK&113$maxn&114$maxn_idPl&115$minn&116$minn_idPl&117$minn_idPr/leq_maxl&118$minn_idPl/leq_maxr&119$maxn_idPr/geq_minl&120$maxn_idPl/geq_minr&121$orP:&122$minn_idPr&123$ex_minn&124$ex_maxn&125$prednK&126$leq_pmull&127$leq&128$subnK&129$leqifP&130$monotone_leqif&131$eqP:&132$leqif_refl&133$leq_pmul2l:&134$Mn1:&135$leq_pmul2r:&136$Mm2:&137$gtn_eqF&102$ltnW&103$implyP&104$leP:&105$eqnP&106$leq_trans&107$subnBA->&108$addnBA&109$subSn&110$leq_sub2r&111$leq_sub2l&112$subnSK&113$maxn&114$maxn_idPl&115$minn&116$minn_idPl&117$minn_idPr/leq_maxl&118$minn_idPl/leq_maxr&119$maxn_idPr/geq_minl&120$maxn_idPl/geq_minr&121$orP:&122$minn_idPr&123$ex_minn&124$ex_maxn&125$prednK&126$leq_pmull&127$leq&128$subnK&129$leqifP&130$monotone_leqif&131$eqP:&132$leqif_refl&133$leq_pmul2l:&134$Mn1:&135$leq_pmul2r:&136$Mm2:&137$gtn_eqF&102$ltnW&103$implyP&104$leP:&105$eqnP&106$leq_trans&107$subnBA->&108$addnBA&109$subSn&110$leq_sub2r&111$leq_sub2l&112$subnSK&113$maxn&114$maxn_idPl&115$minn&116$minn_idPl&117$minn_idPr/leq_maxl&118$minn_idPl/leq_maxr&119$maxn_idPr/geq_minl&120$maxn_idPl/geq_minr&121$orP:&122$minn_idPr&123$ex_minn&124$ex_maxn&125$prednK&126$leq_pmull&127$leq&128$subnK&129$leqifP&130$monotone_leqif&131$eqP:&132$leqif_refl&133$leq_pmul2l:&134$Mn1:&135$leq_pmul2r:&136$Mm2:&137$gtn_eqF&102$ltnW&103$implyP&104$leP:&105$eqnP&106$leq_trans&107$subnBA->&108$addnBA&109$subSn&110$leq_sub2r&111$leq_sub2l&112$subnSK&113$maxn&114$maxn_idPl&115$minn&116$minn_idPl&117$minn_idPr/leq_maxl&118$minn_idPl/leq_maxr&119$maxn_idPr/geq_minl&120$maxn_idPl/geq_minr&121$orP:&122$minn_idPr&123$ex_minn&124$ex_maxn&125$prednK&126$leq_pmull&127$leq&128$subnK&129$leqifP&130$monotone_leqif&131$eqP:&132$leqif_refl&133$leq_pmul2l:&134$Mn1:&135$leq_pmul2r:&136$Mm2:&137$lastP:&102$perm_to_rem/(eq_big_perm _)->&103$eq_big_perm&104$big_rem->&105$rem_filter->&106$IHn&107$familyP&108$ffunP&109$eqP/Df&110$IHr&111$familyP/(_ i)&112$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$b&102$a&103$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$b&102$a&103$pot_matrix&104$
\ No newline at end of file |