Proof rmat to quat formula

b289ee40 · POLLIEN Baptiste · 857e39ff · b289ee40
Commit b289ee40 authored Apr 30, 2021 by POLLIEN Baptiste
13 changed files
--- a/sw/airborne/.frama-c/wp/interactive/lemma_equivalence_rmat_quat.v
+++ b/sw/airborne/.frama-c/wp/interactive/lemma_equivalence_rmat_quat.v
+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require Reals.Rbasic_fun.
+Require Reals.R_sqrt.
+Require BuiltIn.
+Require HighOrd.
+Require bool.Bool.
+Require int.Int.
+Require int.Abs.
+Require int.ComputerDivision.
+Require real.Real.
+Require real.RealInfix.
+Require real.Abs.
+Require real.FromInt.
+Require real.Square.
+Require map.Map.
+
+Parameter eqb:
+  forall {a:Type} {a_WT:WhyType a}, a -> a -> Init.Datatypes.bool.
+
+Axiom eqb1 :
+  forall {a:Type} {a_WT:WhyType a},
+  forall (x:a) (y:a), ((eqb x y) = Init.Datatypes.true) <-> (x = y).
+
+Axiom eqb_false :
+  forall {a:Type} {a_WT:WhyType a},
+  forall (x:a) (y:a), ((eqb x y) = Init.Datatypes.false) <-> ~ (x = y).
+
+Parameter neqb:
+  forall {a:Type} {a_WT:WhyType a}, a -> a -> Init.Datatypes.bool.
+
+Axiom neqb1 :
+  forall {a:Type} {a_WT:WhyType a},
+  forall (x:a) (y:a), ((neqb x y) = Init.Datatypes.true) <-> ~ (x = y).
+
+Parameter zlt: Numbers.BinNums.Z -> Numbers.BinNums.Z -> Init.Datatypes.bool.
+
+Parameter zleq:
+  Numbers.BinNums.Z -> Numbers.BinNums.Z -> Init.Datatypes.bool.
+
+Axiom zlt1 :
+  forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z),
+  ((zlt x y) = Init.Datatypes.true) <-> (x < y)%Z.
+
+Axiom zleq1 :
+  forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z),
+  ((zleq x y) = Init.Datatypes.true) <-> (x <= y)%Z.
+
+Parameter rlt:
+  Reals.Rdefinitions.R -> Reals.Rdefinitions.R -> Init.Datatypes.bool.
+
+Parameter rleq:
+  Reals.Rdefinitions.R -> Reals.Rdefinitions.R -> Init.Datatypes.bool.
+
+Axiom rlt1 :
+  forall (x:Reals.Rdefinitions.R) (y:Reals.Rdefinitions.R),
+  ((rlt x y) = Init.Datatypes.true) <-> (x < y)%R.
+
+Axiom rleq1 :
+  forall (x:Reals.Rdefinitions.R) (y:Reals.Rdefinitions.R),
+  ((rleq x y) = Init.Datatypes.true) <-> (x <= y)%R.
+
+(* Why3 assumption *)
+Definition real_of_int (x:Numbers.BinNums.Z) : Reals.Rdefinitions.R :=
+  BuiltIn.IZR x.
+
+Axiom c_euclidian :
+  forall (n:Numbers.BinNums.Z) (d:Numbers.BinNums.Z), ~ (d = 0%Z) ->
+  (n = (((ZArith.BinInt.Z.quot n d) * d)%Z + (ZArith.BinInt.Z.rem n d))%Z).
+
+Axiom cmod_remainder :
+  forall (n:Numbers.BinNums.Z) (d:Numbers.BinNums.Z),
+  ((0%Z <= n)%Z -> (0%Z < d)%Z ->
+   (0%Z <= (ZArith.BinInt.Z.rem n d))%Z /\ ((ZArith.BinInt.Z.rem n d) < d)%Z) /\
+  ((n <= 0%Z)%Z -> (0%Z < d)%Z ->
+   ((-d)%Z < (ZArith.BinInt.Z.rem n d))%Z /\
+   ((ZArith.BinInt.Z.rem n d) <= 0%Z)%Z) /\
+  ((0%Z <= n)%Z -> (d < 0%Z)%Z ->
+   (0%Z <= (ZArith.BinInt.Z.rem n d))%Z /\
+   ((ZArith.BinInt.Z.rem n d) < (-d)%Z)%Z) /\
+  ((n <= 0%Z)%Z -> (d < 0%Z)%Z ->
+   (d < (ZArith.BinInt.Z.rem n d))%Z /\ ((ZArith.BinInt.Z.rem n d) <= 0%Z)%Z).
+
+Axiom cdiv_neutral :
+  forall (a:Numbers.BinNums.Z), ((ZArith.BinInt.Z.quot a 1%Z) = a).
+
+Axiom cdiv_inv :
+  forall (a:Numbers.BinNums.Z), ~ (a = 0%Z) ->
+  ((ZArith.BinInt.Z.quot a a) = 1%Z).
+
+Axiom cdiv_closed_remainder :
+  forall (a:Numbers.BinNums.Z) (b:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
+  (0%Z <= a)%Z -> (0%Z <= b)%Z ->
+  (0%Z <= (b - a)%Z)%Z /\ ((b - a)%Z < n)%Z ->
+  ((ZArith.BinInt.Z.rem a n) = (ZArith.BinInt.Z.rem b n)) -> (a = b).
+
+(* Why3 assumption *)
+Inductive addr :=
+  | addr'mk : Numbers.BinNums.Z -> Numbers.BinNums.Z -> addr.
+Axiom addr_WhyType : WhyType addr.
+Existing Instance addr_WhyType.
+
+(* Why3 assumption *)
+Definition offset (v:addr) : Numbers.BinNums.Z :=
+  match v with
+  | addr'mk x x1 => x1
+  end.
+
+(* Why3 assumption *)
+Definition base (v:addr) : Numbers.BinNums.Z :=
+  match v with
+  | addr'mk x x1 => x
+  end.
+
+Parameter addr_le: addr -> addr -> Prop.
+
+Parameter addr_lt: addr -> addr -> Prop.
+
+Parameter addr_le_bool: addr -> addr -> Init.Datatypes.bool.
+
+Parameter addr_lt_bool: addr -> addr -> Init.Datatypes.bool.
+
+Axiom addr_le_def :
+  forall (p:addr) (q:addr), ((base p) = (base q)) ->
+  addr_le p q <-> ((offset p) <= (offset q))%Z.
+
+Axiom addr_lt_def :
+  forall (p:addr) (q:addr), ((base p) = (base q)) ->
+  addr_lt p q <-> ((offset p) < (offset q))%Z.
+
+Axiom addr_le_bool_def :
+  forall (p:addr) (q:addr),
+  addr_le p q <-> ((addr_le_bool p q) = Init.Datatypes.true).
+
+Axiom addr_lt_bool_def :
+  forall (p:addr) (q:addr),
+  addr_lt p q <-> ((addr_lt_bool p q) = Init.Datatypes.true).
+
+(* Why3 assumption *)
+Definition null : addr := addr'mk 0%Z 0%Z.
+
+(* Why3 assumption *)
+Definition global (b:Numbers.BinNums.Z) : addr := addr'mk b 0%Z.
+
+(* Why3 assumption *)
+Definition shift (p:addr) (k:Numbers.BinNums.Z) : addr :=
+  addr'mk (base p) ((offset p) + k)%Z.
+
+(* Why3 assumption *)
+Definition included (p:addr) (a:Numbers.BinNums.Z) (q:addr)
+    (b:Numbers.BinNums.Z) : Prop :=
+  (0%Z < a)%Z ->
+  (0%Z <= b)%Z /\
+  ((base p) = (base q)) /\
+  ((offset q) <= (offset p))%Z /\
+  (((offset p) + a)%Z <= ((offset q) + b)%Z)%Z.
+
+(* Why3 assumption *)
+Definition separated (p:addr) (a:Numbers.BinNums.Z) (q:addr)
+    (b:Numbers.BinNums.Z) : Prop :=
+  (a <= 0%Z)%Z \/
+  (b <= 0%Z)%Z \/
+  ~ ((base p) = (base q)) \/
+  (((offset q) + b)%Z <= (offset p))%Z \/
+  (((offset p) + a)%Z <= (offset q))%Z.
+
+(* Why3 assumption *)
+Definition eqmem {a:Type} {a_WT:WhyType a} (m1:addr -> a) (m2:addr -> a)
+    (p:addr) (a1:Numbers.BinNums.Z) : Prop :=
+  forall (q:addr), included q 1%Z p a1 -> ((m1 q) = (m2 q)).
+
+Parameter havoc:
+  forall {a:Type} {a_WT:WhyType a}, (addr -> a) -> (addr -> a) -> addr ->
+  Numbers.BinNums.Z -> addr -> a.
+
+(* Why3 assumption *)
+Definition valid_rw (m:Numbers.BinNums.Z -> Numbers.BinNums.Z) (p:addr)
+    (n:Numbers.BinNums.Z) : Prop :=
+  (0%Z < n)%Z ->
+  (0%Z < (base p))%Z /\
+  (0%Z <= (offset p))%Z /\ (((offset p) + n)%Z <= (m (base p)))%Z.
+
+(* Why3 assumption *)
+Definition valid_rd (m:Numbers.BinNums.Z -> Numbers.BinNums.Z) (p:addr)
+    (n:Numbers.BinNums.Z) : Prop :=
+  (0%Z < n)%Z ->
+  ~ (0%Z = (base p)) /\
+  (0%Z <= (offset p))%Z /\ (((offset p) + n)%Z <= (m (base p)))%Z.
+
+(* Why3 assumption *)
+Definition valid_obj (m:Numbers.BinNums.Z -> Numbers.BinNums.Z) (p:addr)
+    (n:Numbers.BinNums.Z) : Prop :=
+  (0%Z < n)%Z ->
+  (p = null) \/
+  ~ (0%Z = (base p)) /\
+  (0%Z <= (offset p))%Z /\ (((offset p) + n)%Z <= (1%Z + (m (base p)))%Z)%Z.
+
+(* Why3 assumption *)
+Definition invalid (m:Numbers.BinNums.Z -> Numbers.BinNums.Z) (p:addr)
+    (n:Numbers.BinNums.Z) : Prop :=
+  (n <= 0%Z)%Z \/
+  ((base p) = 0%Z) \/
+  ((m (base p)) <= (offset p))%Z \/ (((offset p) + n)%Z <= 0%Z)%Z.
+
+Axiom valid_rw_rd :
+  forall (m:Numbers.BinNums.Z -> Numbers.BinNums.Z), forall (p:addr),
+  forall (n:Numbers.BinNums.Z), valid_rw m p n -> valid_rd m p n.
+
+Axiom valid_string :
+  forall (m:Numbers.BinNums.Z -> Numbers.BinNums.Z), forall (p:addr),
+  ((base p) < 0%Z)%Z ->
+  (0%Z <= (offset p))%Z /\ ((offset p) < (m (base p)))%Z ->
+  valid_rd m p 1%Z /\ ~ valid_rw m p 1%Z.
+
+Axiom separated_1 :
+  forall (p:addr) (q:addr),
+  forall (a:Numbers.BinNums.Z) (b:Numbers.BinNums.Z) (i:Numbers.BinNums.Z)
+    (j:Numbers.BinNums.Z),
+  separated p a q b -> ((offset p) <= i)%Z /\ (i < ((offset p) + a)%Z)%Z ->
+  ((offset q) <= j)%Z /\ (j < ((offset q) + b)%Z)%Z ->
+  ~ ((addr'mk (base p) i) = (addr'mk (base q) j)).
+
+Parameter region: Numbers.BinNums.Z -> Numbers.BinNums.Z.
+
+Parameter linked: (Numbers.BinNums.Z -> Numbers.BinNums.Z) -> Prop.
+
+Parameter sconst: (addr -> Numbers.BinNums.Z) -> Prop.
+
+(* Why3 assumption *)
+Definition framed (m:addr -> addr) : Prop :=
+  forall (p:addr), ((region (base (m p))) <= 0%Z)%Z.
+
+Axiom separated_included :
+  forall (p:addr) (q:addr),
+  forall (a:Numbers.BinNums.Z) (b:Numbers.BinNums.Z), (0%Z < a)%Z ->
+  (0%Z < b)%Z -> separated p a q b -> ~ included p a q b.
+
+Axiom included_trans :
+  forall (p:addr) (q:addr) (r:addr),
+  forall (a:Numbers.BinNums.Z) (b:Numbers.BinNums.Z) (c:Numbers.BinNums.Z),
+  included p a q b -> included q b r c -> included p a r c.
+
+Axiom separated_trans :
+  forall (p:addr) (q:addr) (r:addr),
+  forall (a:Numbers.BinNums.Z) (b:Numbers.BinNums.Z) (c:Numbers.BinNums.Z),
+  included p a q b -> separated q b r c -> separated p a r c.
+
+Axiom separated_sym :
+  forall (p:addr) (q:addr),
+  forall (a:Numbers.BinNums.Z) (b:Numbers.BinNums.Z),
+  separated p a q b <-> separated q b p a.
+
+Axiom eqmem_included :
+  forall {a:Type} {a_WT:WhyType a},
+  forall (m1:addr -> a) (m2:addr -> a), forall (p:addr) (q:addr),
+  forall (a1:Numbers.BinNums.Z) (b:Numbers.BinNums.Z), included p a1 q b ->
+  eqmem m1 m2 q b -> eqmem m1 m2 p a1.
+
+Axiom eqmem_sym :
+  forall {a:Type} {a_WT:WhyType a},
+  forall (m1:addr -> a) (m2:addr -> a), forall (p:addr),
+  forall (a1:Numbers.BinNums.Z), eqmem m1 m2 p a1 -> eqmem m2 m1 p a1.
+
+Axiom havoc_access :
+  forall {a:Type} {a_WT:WhyType a},
+  forall (m0:addr -> a) (m1:addr -> a), forall (q:addr) (p:addr),
+  forall (a1:Numbers.BinNums.Z),
+  (separated q 1%Z p a1 -> ((havoc m0 m1 p a1 q) = (m1 q))) /\
+  (~ separated q 1%Z p a1 -> ((havoc m0 m1 p a1 q) = (m0 q))).
+
+Parameter cinits: (addr -> Init.Datatypes.bool) -> Prop.
+
+(* Why3 assumption *)
+Definition is_init_range (m:addr -> Init.Datatypes.bool) (p:addr)
+    (l:Numbers.BinNums.Z) : Prop :=
+  forall (i:Numbers.BinNums.Z), (0%Z <= i)%Z /\ (i < l)%Z ->
+  ((m (shift p i)) = Init.Datatypes.true).
+
+Parameter set_init:
+  (addr -> Init.Datatypes.bool) -> addr -> Numbers.BinNums.Z ->
+  addr -> Init.Datatypes.bool.
+
+Axiom set_init_access :
+  forall (m:addr -> Init.Datatypes.bool), forall (q:addr) (p:addr),
+  forall (a:Numbers.BinNums.Z),
+  (separated q 1%Z p a -> ((set_init m p a q) = (m q))) /\
+  (~ separated q 1%Z p a -> ((set_init m p a q) = Init.Datatypes.true)).
+
+(* Why3 assumption *)
+Definition monotonic_init (m1:addr -> Init.Datatypes.bool)
+    (m2:addr -> Init.Datatypes.bool) : Prop :=
+  forall (p:addr), ((m1 p) = Init.Datatypes.true) ->
+  ((m2 p) = Init.Datatypes.true).
+
+Parameter int_of_addr: addr -> Numbers.BinNums.Z.
+
+Parameter addr_of_int: Numbers.BinNums.Z -> addr.
+
+Axiom table : Type.
+Parameter table_WhyType : WhyType table.
+Existing Instance table_WhyType.
+
+Parameter table_of_base: Numbers.BinNums.Z -> table.
+
+Parameter table_to_offset: table -> Numbers.BinNums.Z -> Numbers.BinNums.Z.
+
+Axiom table_to_offset_zero :
+  forall (t:table), ((table_to_offset t 0%Z) = 0%Z).
+
+Axiom table_to_offset_monotonic :
+  forall (t:table), forall (o1:Numbers.BinNums.Z) (o2:Numbers.BinNums.Z),
+  (o1 <= o2)%Z <-> ((table_to_offset t o1) <= (table_to_offset t o2))%Z.
+
+Axiom int_of_addr_bijection :
+  forall (a:Numbers.BinNums.Z), ((int_of_addr (addr_of_int a)) = a).
+
+Axiom addr_of_int_bijection :
+  forall (p:addr), ((addr_of_int (int_of_addr p)) = p).
+
+Axiom addr_of_null : ((int_of_addr null) = 0%Z).
+
+(* Why3 assumption *)
+Definition P_unary_quaternion_1_ (Mf32:addr -> Reals.Rdefinitions.R)
+    (q:addr) : Prop :=
+  let r := Mf32 (shift q 0%Z) in
+  let r1 := Mf32 (shift q 1%Z) in
+  let r2 := Mf32 (shift q 2%Z) in
+  let r3 := Mf32 (shift q 3%Z) in
+  (((((r * r)%R + (r1 * r1)%R)%R + (r2 * r2)%R)%R + (r3 * r3)%R)%R = 1%R).
+
+(* Why3 assumption *)
+Inductive S12_RealRMat_s :=
+  | S12_RealRMat_s1 : Reals.Rdefinitions.R -> Reals.Rdefinitions.R ->
+      Reals.Rdefinitions.R -> Reals.Rdefinitions.R -> Reals.Rdefinitions.R ->
+      Reals.Rdefinitions.R -> Reals.Rdefinitions.R -> Reals.Rdefinitions.R ->
+      Reals.Rdefinitions.R -> S12_RealRMat_s.
+Axiom S12_RealRMat_s_WhyType : WhyType S12_RealRMat_s.
+Existing Instance S12_RealRMat_s_WhyType.
+
+(* Why3 assumption *)
+Definition F12_RealRMat_s_a22 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
+  match v with
+  | S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x8
+  end.
+
+(* Why3 assumption *)
+Definition F12_RealRMat_s_a21 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
+  match v with
+  | S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x7
+  end.
+
+(* Why3 assumption *)
+Definition F12_RealRMat_s_a20 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
+  match v with
+  | S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x6
+  end.
+
+(* Why3 assumption *)
+Definition F12_RealRMat_s_a12 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
+  match v with
+  | S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x5
+  end.
+
+(* Why3 assumption *)
+Definition F12_RealRMat_s_a11 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
+  match v with
+  | S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x4
+  end.
+
+(* Why3 assumption *)
+Definition F12_RealRMat_s_a10 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
+  match v with
+  | S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x3
+  end.
+
+(* Why3 assumption *)
+Definition F12_RealRMat_s_a02 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
+  match v with
+  | S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x2
+  end.
+
+(* Why3 assumption *)
+Definition F12_RealRMat_s_a01 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
+  match v with
+  | S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x1
+  end.
+
+(* Why3 assumption *)
+Definition F12_RealRMat_s_a00 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
+  match v with
+  | S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x
+  end.
+
+(* Why3 assumption *)
+Definition EqS12_RealRMat_s (S:S12_RealRMat_s) (S1:S12_RealRMat_s) : Prop :=
+  (((((((((F12_RealRMat_s_a00 S1) = (F12_RealRMat_s_a00 S)) /\
+         ((F12_RealRMat_s_a01 S1) = (F12_RealRMat_s_a01 S))) /\
+        ((F12_RealRMat_s_a02 S1) = (F12_RealRMat_s_a02 S))) /\
+       ((F12_RealRMat_s_a10 S1) = (F12_RealRMat_s_a10 S))) /\
+      ((F12_RealRMat_s_a11 S1) = (F12_RealRMat_s_a11 S))) /\
+     ((F12_RealRMat_s_a12 S1) = (F12_RealRMat_s_a12 S))) /\
+    ((F12_RealRMat_s_a20 S1) = (F12_RealRMat_s_a20 S))) /\
+   ((F12_RealRMat_s_a21 S1) = (F12_RealRMat_s_a21 S))) /\
+  ((F12_RealRMat_s_a22 S1) = (F12_RealRMat_s_a22 S)).
+
+(* Why3 assumption *)
+Definition L_mult_RealRMat (rmat1:S12_RealRMat_s) (rmat2:S12_RealRMat_s) :
+    S12_RealRMat_s :=
+  let r := F12_RealRMat_s_a00 rmat1 in
+  let r1 := F12_RealRMat_s_a00 rmat2 in
+  let r2 := F12_RealRMat_s_a01 rmat1 in
+  let r3 := F12_RealRMat_s_a10 rmat2 in
+  let r4 := F12_RealRMat_s_a02 rmat1 in
+  let r5 := F12_RealRMat_s_a20 rmat2 in
+  let r6 := F12_RealRMat_s_a01 rmat2 in
+  let r7 := F12_RealRMat_s_a11 rmat2 in
+  let r8 := F12_RealRMat_s_a21 rmat2 in
+  let r9 := F12_RealRMat_s_a02 rmat2 in
+  let r10 := F12_RealRMat_s_a12 rmat2 in
+  let r11 := F12_RealRMat_s_a22 rmat2 in
+  let r12 := F12_RealRMat_s_a10 rmat1 in
+  let r13 := F12_RealRMat_s_a11 rmat1 in
+  let r14 := F12_RealRMat_s_a12 rmat1 in
+  let r15 := F12_RealRMat_s_a20 rmat1 in
+  let r16 := F12_RealRMat_s_a21 rmat1 in
+  let r17 := F12_RealRMat_s_a22 rmat1 in
+  S12_RealRMat_s1 (((r * r1)%R + (r2 * r3)%R)%R + (r4 * r5)%R)%R
+  (((r * r6)%R + (r2 * r7)%R)%R + (r4 * r8)%R)%R
+  (((r * r9)%R + (r2 * r10)%R)%R + (r4 * r11)%R)%R
+  (((r12 * r1)%R + (r13 * r3)%R)%R + (r14 * r5)%R)%R
+  (((r12 * r6)%R + (r13 * r7)%R)%R + (r14 * r8)%R)%R
+  (((r12 * r9)%R + (r13 * r10)%R)%R + (r14 * r11)%R)%R
+  (((r15 * r1)%R + (r16 * r3)%R)%R + (r17 * r5)%R)%R
+  (((r15 * r6)%R + (r16 * r7)%R)%R + (r17 * r8)%R)%R
+  (((r15 * r9)%R + (r16 * r10)%R)%R + (r17 * r11)%R)%R.
+
+(* Why3 assumption *)
+Definition L_transpose (rmat:S12_RealRMat_s) : S12_RealRMat_s :=
+  S12_RealRMat_s1 (F12_RealRMat_s_a00 rmat) (F12_RealRMat_s_a10 rmat)
+  (F12_RealRMat_s_a20 rmat) (F12_RealRMat_s_a01 rmat)
+  (F12_RealRMat_s_a11 rmat) (F12_RealRMat_s_a21 rmat)
+  (F12_RealRMat_s_a02 rmat) (F12_RealRMat_s_a12 rmat)
+  (F12_RealRMat_s_a22 rmat).
+
+(* Why3 assumption *)
+Definition P_rotation_matrix (rmat:S12_RealRMat_s) : Prop :=
+  EqS12_RealRMat_s (L_mult_RealRMat rmat (L_transpose rmat))
+  (S12_RealRMat_s1 1%R 0%R 0%R 0%R 1%R 0%R 0%R 0%R 1%R).
+
+(* Why3 assumption *)
+Definition L_mult_scalar (rmat:S12_RealRMat_s) (a:Numbers.BinNums.Z) :
+    S12_RealRMat_s :=
+  let r := real_of_int a in
+  S12_RealRMat_s1 (r * (F12_RealRMat_s_a00 rmat))%R
+  (r * (F12_RealRMat_s_a01 rmat))%R (r * (F12_RealRMat_s_a02 rmat))%R
+  (r * (F12_RealRMat_s_a10 rmat))%R (r * (F12_RealRMat_s_a11 rmat))%R
+  (r * (F12_RealRMat_s_a12 rmat))%R (r * (F12_RealRMat_s_a20 rmat))%R
+  (r * (F12_RealRMat_s_a21 rmat))%R (r * (F12_RealRMat_s_a22 rmat))%R.
+
+Axiom Q_mult_id_rmat_neutral :
+  forall (rmat:S12_RealRMat_s),
+  EqS12_RealRMat_s
+  (L_mult_RealRMat rmat
+   (S12_RealRMat_s1 1%R 0%R 0%R 0%R 1%R 0%R 0%R 0%R 1%R))
+  rmat.
+
+Axiom Q_mult_rmat_id_neutral :
+  forall (rmat:S12_RealRMat_s),
+  EqS12_RealRMat_s
+  (L_mult_RealRMat (S12_RealRMat_s1 1%R 0%R 0%R 0%R 1%R 0%R 0%R 0%R 1%R)
+   rmat)
+  rmat.
+
+Axiom Q_transpose_id :
+  forall (a:Numbers.BinNums.Z),
+  let a1 :=
+  L_mult_scalar (S12_RealRMat_s1 1%R 0%R 0%R 0%R 1%R 0%R 0%R 0%R 1%R) a in
+  EqS12_RealRMat_s (L_transpose a1) a1.
+
+Axiom Q_transpose_transpose_rmat :
+  forall (rmat:S12_RealRMat_s),
+  EqS12_RealRMat_s (L_transpose (L_transpose rmat)) rmat.
+
+(* Why3 assumption *)
+Definition L_l_RMat_of_FloatQuat_1_ (Mf32:addr -> Reals.Rdefinitions.R)
+    (q:addr) : S12_RealRMat_s :=
+  let r := Mf32 (shift q 2%Z) in
+  let r1 := (r * r)%R in
+  let r2 := ((-1%R)%R * r1)%R in
+  let r3 := Mf32 (shift q 3%Z) in
+  let r4 := (r3 * r3)%R in
+  let r5 := ((-1%R)%R * r4)%R in
+  let r6 := Mf32 (shift q 0%Z) in
+  let r7 := (r6 * r6)%R in
+  let r8 := Mf32 (shift q 1%Z) in
+  let r9 := (r8 * r8)%R in
+  let r10 := (r6 * r3)%R in
+  let r11 := (r8 * r)%R in
+  let r12 := (r6 * r)%R in
+  let r13 := (r8 * r3)%R in
+  let r14 := ((-1%R)%R * r9)%R in
+  let r15 := (r6 * r8)%R in
+  let r16 := (r * r3)%R in
+  S12_RealRMat_s1 (((r2 + r5)%R + r7)%R + r9)%R
+  (2%R * (((-1%R)%R * r10)%R + r11)%R)%R (2%R * (r12 + r13)%R)%R
+  (2%R * (r10 + r11)%R)%R (((r14 + r5)%R + r7)%R + r1)%R
+  (2%R * (((-1%R)%R * r15)%R + r16)%R)%R
+  (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_quat_of_rmat_ortho :
+  forall (Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
+  P_unary_quaternion_1_ Mf32 q ->
+  P_rotation_matrix (L_l_RMat_of_FloatQuat_1_ Mf32 q).
+
+(* Why3 assumption *)
+Inductive S13_RealQuat_s :=
+  | S13_RealQuat_s1 : Reals.Rdefinitions.R -> Reals.Rdefinitions.R ->
+      Reals.Rdefinitions.R -> Reals.Rdefinitions.R -> S13_RealQuat_s.
+Axiom S13_RealQuat_s_WhyType : WhyType S13_RealQuat_s.
+Existing Instance S13_RealQuat_s_WhyType.
+
+(* Why3 assumption *)
+Definition F13_RealQuat_s_qz (v:S13_RealQuat_s) : Reals.Rdefinitions.R :=
+  match v with
+  | S13_RealQuat_s1 x x1 x2 x3 => x3
+  end.
+
+(* Why3 assumption *)
+Definition F13_RealQuat_s_qy (v:S13_RealQuat_s) : Reals.Rdefinitions.R :=
+  match v with
+  | S13_RealQuat_s1 x x1 x2 x3 => x2
+  end.
+
+(* Why3 assumption *)
+Definition F13_RealQuat_s_qx (v:S13_RealQuat_s) : Reals.Rdefinitions.R :=