commit by user utente

[helm.git] / weblib / ricciott / prova.ma

diff --git a/weblib/ricciott/prova.ma b/weblib/ricciott/prova.ma
new file mode 100644 (file)
index 0000000..cd95fd0
--- /dev/null
+++ b/weblib/ricciott/prova.ma
@@ -0,0 +1,27 @@
+include "basics/pts.ma".
+
+axiom R : Type[0].
+axiom V : Type[0].
+
+axiom f : \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6.
+
+axiom rplus : \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6.
+axiom rtimes : \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6.
+
+axiom vplus : \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6.
+axiom stimes : \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6.
+
+interpretation "real plus" 'plus x y = (rplus x y).
+interpretation "real times" 'times x y = (rtimes x y).
+
+interpretation "vector plus" 'plus x y = (vplus x y).
+interpretation "scalar product on vectors" 'times x y = (stimes x y).
+
+axiom a : \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6. axiom b : \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6.
+axiom x : \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6. axiom y : \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6. axiom z : \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6.
+
+include "basics/logic.ma".
+
+axiom fa : \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6 -> \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6.
+
+lemma pippo : \ 5a href="cic:/matita/ricciott/prova/f.dec"\ 6f\ 5/a\ 6 (\ 5a href="cic:/matita/ricciott/prova/a.dec"\ 6a\ 5/a\ 6\ 5a title="scalar product on vectors" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a href="cic:/matita/ricciott/prova/x.dec"\ 6x\ 5/a\ 6 \ 5a title="vector plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a href="cic:/matita/ricciott/prova/b.dec"\ 6b\ 5/a\ 6\ 5a title="scalar product on vectors" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a href="cic:/matita/ricciott/prova/y.dec"\ 6y\ 5/a\ 6 \ 5a title="vector plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a href="cic:/matita/ricciott/prova/z.dec"\ 6z\ 5/a\ 6) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/ricciott/prova/a.dec"\ 6a\ 5/a\ 6\ 5a title="real times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/ricciott/prova/f.dec"\ 6f\ 5/a\ 6 \ 5a href="cic:/matita/ricciott/prova/x.dec"\ 6x\ 5/a\ 6) \ 5a title="real plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a href="cic:/matita/ricciott/prova/b.dec"\ 6b\ 5/a\ 6\ 5a title="real times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/ricciott/prova/fa.dec"\ 6fa\ 5/a\ 6 \ 5a href="cic:/matita/ricciott/prova/y.dec"\ 6y\ 5/a\ 6) + z.
\ No newline at end of file