Commit b158ffaa authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Update lemma

parent b289ee40
......@@ -277,7 +277,7 @@ Definition L_l_RMat_of_FloatQuat_2_ (q:S13_RealQuat_s) : S12_RealRMat_s :=
(2%R * (((-1%R)%R * r12)%R + r13)%R)%R (2%R * (r15 + r16)%R)%R
(((r14 + r2)%R + r7)%R + r4)%R.
Axiom Q_impl_rmat_quat_2 :
Axiom Q_impl_quat_rmat :
forall (rm:S12_RealRMat_s) (q:S13_RealQuat_s),
((L_l_FloatQuat_of_RMat_trace_pos_1_ rm) = q) ->
(0%R <= (F13_RealQuat_s_qi q))%R -> (0%R < (L_trace_1_ rm))%R ->
......
......@@ -3,9 +3,9 @@
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 1.3 } ],
"verdict": "valid", "time": 1.43 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 5.04 } ],
"verdict": "valid", "time": 5.64 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 5.74 } ],
"verdict": "valid", "time": 6.45 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
......@@ -3,9 +3,9 @@
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.53 } ],
"verdict": "valid", "time": 6.65 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 5.34 } ],
"verdict": "valid", "time": 6.97 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 5.8 } ],
"verdict": "valid", "time": 7.4 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
......@@ -3,7 +3,7 @@
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "time": 22.5714,
"verdict": "valid", "time": 22.9451,
"steps": 130 } ],
"OnLeft": [ { "prover": "Z3:4.8.6:noBV",
"verdict": "timeout", "time": 10. },
......
......@@ -398,7 +398,7 @@ logic RealRMat l_RMat_of_FloatQuat(RealQuat q) =
*/
/*@
lemma impl_rmat_quat_2:
lemma impl_quat_rmat:
\forall RealRMat rm, RealQuat q;
trace(rm) > 0 && unary_quaternion(q) && q.qi >= 0
&& q == l_FloatQuat_of_RMat_trace_pos(rm)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment