Commit 7a574651 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix Coq scripts for examples/mergesort_list.mlw.

parent f6390a01
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Definition unit := unit.
Require list.List.
Require list.Length.
Require list.Mem.
Require list.Append.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
Inductive list (a:Type) :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Set Contextual Implicit.
Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.
Set Implicit Arguments.
Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
match l with
| Nil => 0%Z
| (Cons _ r) => (1%Z + (length r))%Z
end.
Unset Implicit Arguments.
Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
(0%Z <= (length l))%Z.
Axiom Length_nil : forall (a:Type), forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil:(list a))).
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive sorted : (list Z) -> Prop :=
| Sorted_Nil : (sorted (Nil:(list Z)))
| Sorted_One : forall (x:Z), (sorted (Cons x (Nil:(list Z))))
| Sorted_Two : forall (x:Z) (y:Z) (l:(list Z)), (x <= y)%Z ->
((sorted (Cons y l)) -> (sorted (Cons x (Cons y l)))).
Set Implicit Arguments.
Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
match l with
| Nil => False
| (Cons y r) => (x = y) \/ (mem x r)
end.
Unset Implicit Arguments.
Axiom sorted_mem : forall (x:Z) (l:(list Z)), ((forall (y:Z), (mem y l) ->
(x <= y)%Z) /\ (sorted l)) <-> (sorted (Cons x l)).
Set Implicit Arguments.
Fixpoint infix_plpl (a:Type)(l1:(list a)) (l2:(list a)) {struct l1}: (list
a) :=
match l1 with
| Nil => l2
| (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2))
end.
Unset Implicit Arguments.
Axiom Append_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a))
(l3:(list a)), ((infix_plpl l1 (infix_plpl l2
l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
Axiom Append_l_nil : forall (a:Type), forall (l:(list a)), ((infix_plpl l
(Nil:(list a))) = l).
Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z).
Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
(mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)).
Axiom mem_decomp : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) ->
exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))).
| Sorted_Nil : (sorted nil)
| Sorted_One : forall (x:Z), (sorted (cons x nil))
| Sorted_Two : forall (x:Z) (y:Z) (l:(list Z)), (x <= y)%Z -> ((sorted
(cons y l)) -> (sorted (cons x (cons y l)))).
Parameter num_occ: forall (a:Type), a -> (list a) -> Z.
Axiom sorted_mem : forall (x:Z) (l:(list Z)), ((forall (y:Z), (list.Mem.mem y
l) -> (x <= y)%Z) /\ (sorted l)) <-> (sorted (cons x l)).
Implicit Arguments num_occ.
Parameter num_occ: forall {a:Type} {a_WT:WhyType a}, a -> (list a) -> Z.
Axiom num_occ_def : forall (a:Type), forall (x:a) (l:(list a)),
Axiom num_occ_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l:(list a)),
match l with
| Nil => ((num_occ x l) = 0%Z)
| (Cons y r) => ((x = y) -> ((num_occ x l) = (1%Z + (num_occ x r))%Z)) /\
| nil => ((num_occ x l) = 0%Z)
| (cons y r) => ((x = y) -> ((num_occ x l) = (1%Z + (num_occ x r))%Z)) /\
((~ (x = y)) -> ((num_occ x l) = (0%Z + (num_occ x r))%Z))
end.
Axiom Mem_Num_Occ : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) <->
(0%Z < (num_occ x l))%Z.
Axiom Mem_Num_Occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l:(list a)), (list.Mem.mem x l) <-> (0%Z < (num_occ x l))%Z.
Axiom Append_Num_Occ : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list
a)), ((num_occ x (infix_plpl l1 l2)) = ((num_occ x l1) + (num_occ x
l2))%Z).
Axiom Append_Num_Occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), ((num_occ x (List.app l1 l2)) = ((num_occ x
l1) + (num_occ x l2))%Z).
Definition permut (a:Type)(l1:(list a)) (l2:(list a)): Prop := forall (x:a),
((num_occ x l1) = (num_occ x l2)).
Implicit Arguments permut.
(* Why3 assumption *)
Definition permut {a:Type} {a_WT:WhyType a} (l1:(list a))
(l2:(list a)): Prop := forall (x:a), ((num_occ x l1) = (num_occ x l2)).
Axiom Permut_refl : forall (a:Type), forall (l:(list a)), (permut l l).
Axiom Permut_refl : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
(permut l l).
Axiom Permut_sym : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
(permut l1 l2) -> (permut l2 l1).
Axiom Permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), (permut l1 l2) -> (permut l2 l1).
Axiom Permut_trans : forall (a:Type), forall (l1:(list a)) (l2:(list a))
(l3:(list a)), (permut l1 l2) -> ((permut l2 l3) -> (permut l1 l3)).
Axiom Permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), (permut l1 l2) -> ((permut l2 l3) -> (permut
l1 l3)).
Axiom Permut_cons : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list
a)), (permut l1 l2) -> (permut (Cons x l1) (Cons x l2)).
Axiom Permut_cons : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), (permut l1 l2) -> (permut (cons x l1)
(cons x l2)).
Axiom Permut_swap : forall (a:Type), forall (x:a) (y:a) (l:(list a)),
(permut (Cons x (Cons y l)) (Cons y (Cons x l))).
Axiom Permut_swap : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(l:(list a)), (permut (cons x (cons y l)) (cons y (cons x l))).
Axiom Permut_mem : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
(permut l1 l2) -> ((mem x l1) -> (mem x l2)).
Axiom Permut_cons_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), (permut (List.app (cons x l1) l2)
(List.app l1 (cons x l2))).
Axiom Permut_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
(permut l1 l2) -> ((length l1) = (length l2)).
Axiom Permut_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), (permut (List.app (List.app l1 l2) l3)
(List.app l1 (List.app l2 l3))).
Axiom Permut_cons_append : forall (a:Type), forall (x:a) (l1:(list a))
(l2:(list a)), (permut (infix_plpl (Cons x l1) l2) (infix_plpl l1 (Cons x
l2))).
Axiom Permut_append : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (k1:(list a)) (k2:(list a)), (permut l1 k1) -> ((permut l2
k2) -> (permut (List.app l1 l2) (List.app k1 k2))).
Axiom Permut_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a))
(l3:(list a)), (permut (infix_plpl (infix_plpl l1 l2) l3) (infix_plpl l1
(infix_plpl l2 l3))).
Axiom Permut_append_swap : forall {a:Type} {a_WT:WhyType a},
forall (l1:(list a)) (l2:(list a)), (permut (List.app l1 l2)
(List.app l2 l1)).
Axiom Permut_append : forall (a:Type), forall (l1:(list a)) (l2:(list a))
(k1:(list a)) (k2:(list a)), (permut l1 k1) -> ((permut l2 k2) ->
(permut (infix_plpl l1 l2) (infix_plpl k1 k2))).
Axiom Permut_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), (permut l1 l2) -> ((list.Mem.mem x l1) ->
(list.Mem.mem x l2)).
Axiom Permut_append_swap : forall (a:Type), forall (l1:(list a)) (l2:(list
a)), (permut (infix_plpl l1 l2) (infix_plpl l2 l1)).
Axiom Permut_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), (permut l1 l2) ->
((list.Length.length l1) = (list.Length.length l2)).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem WP_parameter_merge : forall (l1:(list Z)), forall (l2:(list Z)),
((sorted l1) /\ (sorted l2)) ->
(* Why3 goal *)
Theorem WP_parameter_merge : forall (l1:(list Z)) (l2:(list Z)), ((sorted
l1) /\ (sorted l2)) ->
match l2 with
| (Cons x x1) =>
| (cons x x1) =>
match l1 with
| (Cons x2 x3) => (~ (x2 <= x)%Z) ->
((((0%Z <= ((length l1) + (length l2))%Z)%Z /\
(((length l1) + (length x1))%Z < ((length l1) + (length l2))%Z)%Z) /\
((sorted l1) /\ (sorted x1))) -> forall (result:(list Z)),
((sorted result) /\ (permut result (infix_plpl l1 x1))) ->
(permut (Cons x result) (infix_plpl l1 l2)))
| Nil => True
| (cons x2 x3) => (~ (x2 <= x)%Z) -> (((sorted l1) /\ (sorted x1)) ->
forall (o:(list Z)), ((sorted o) /\ (permut o (List.app l1 x1))) ->
(permut (cons x o) (List.app l1 l2)))
| nil => True
end
| Nil => True
| nil => True
end.
(* YOU MAY EDIT THE PROOF BELOW *)
(* Why3 intros l1 l2 (h1,h2). *)
intuition.
destruct l2; intuition.
destruct l1; intuition.
apply Permut_trans with (Cons z (infix_plpl (Cons z0 l1) l2)); auto.
apply Permut_trans with (cons z (app (cons z0 l1) l2)); auto.
apply Permut_cons; auto.
apply Permut_cons_append.
apply (Permut_cons_append z).
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require list.List.
Require list.Length.
Require list.Mem.
Require list.Append.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive list (a:Type) :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Set Contextual Implicit.
Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
match l with
| Nil => 0%Z
| (Cons _ r) => (1%Z + (length r))%Z
end.
Unset Implicit Arguments.
Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
(0%Z <= (length l))%Z.
Axiom Length_nil : forall (a:Type), forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil :(list a))).
Definition unit := unit.
(* Why3 assumption *)
Inductive sorted : (list Z) -> Prop :=
| Sorted_Nil : (sorted (Nil :(list Z)))
| Sorted_One : forall (x:Z), (sorted (Cons x (Nil :(list Z))))
| Sorted_Two : forall (x:Z) (y:Z) (l:(list Z)), (x <= y)%Z ->
((sorted (Cons y l)) -> (sorted (Cons x (Cons y l)))).
| Sorted_Nil : (sorted nil)
| Sorted_One : forall (x:Z), (sorted (cons x nil))
| Sorted_Two : forall (x:Z) (y:Z) (l:(list Z)), (x <= y)%Z -> ((sorted
(cons y l)) -> (sorted (cons x (cons y l)))).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
match l with
| Nil => False
| (Cons y r) => (x = y) \/ (mem x r)
end.
Unset Implicit Arguments.
Axiom sorted_mem : forall (x:Z) (l:(list Z)), ((forall (y:Z), (list.Mem.mem y
l) -> (x <= y)%Z) /\ (sorted l)) <-> (sorted (cons x l)).
Axiom sorted_mem : forall (x:Z) (l:(list Z)), ((forall (y:Z), (mem y l) ->
(x <= y)%Z) /\ (sorted l)) <-> (sorted (Cons x l)).
Parameter num_occ: forall {a:Type} {a_WT:WhyType a}, a -> (list a) -> Z.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint infix_plpl (a:Type)(l1:(list a)) (l2:(list a)) {struct l1}: (list
a) :=
match l1 with
| Nil => l2
| (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2))
end.
Unset Implicit Arguments.
Axiom Append_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a))
(l3:(list a)), ((infix_plpl l1 (infix_plpl l2
l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
Axiom Append_l_nil : forall (a:Type), forall (l:(list a)), ((infix_plpl l
(Nil :(list a))) = l).
Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z).
Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
(mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)).
Axiom mem_decomp : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) ->
exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))).
Parameter num_occ: forall (a:Type), a -> (list a) -> Z.
Implicit Arguments num_occ.
Axiom num_occ_def : forall (a:Type), forall (x:a) (l:(list a)),
Axiom num_occ_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l:(list a)),
match l with
| Nil => ((num_occ x l) = 0%Z)
| (Cons y r) => ((x = y) -> ((num_occ x l) = (1%Z + (num_occ x r))%Z)) /\
| nil => ((num_occ x l) = 0%Z)
| (cons y r) => ((x = y) -> ((num_occ x l) = (1%Z + (num_occ x r))%Z)) /\
((~ (x = y)) -> ((num_occ x l) = (0%Z + (num_occ x r))%Z))
end.
Axiom Mem_Num_Occ : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) <->
(0%Z < (num_occ x l))%Z.
Axiom Mem_Num_Occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l:(list a)), (list.Mem.mem x l) <-> (0%Z < (num_occ x l))%Z.
Axiom Append_Num_Occ : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list
a)), ((num_occ x (infix_plpl l1 l2)) = ((num_occ x l1) + (num_occ x
l2))%Z).
Axiom Append_Num_Occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), ((num_occ x (List.app l1 l2)) = ((num_occ x
l1) + (num_occ x l2))%Z).
(* Why3 assumption *)
Definition permut (a:Type)(l1:(list a)) (l2:(list a)): Prop := forall (x:a),
((num_occ x l1) = (num_occ x l2)).
Implicit Arguments permut.
Axiom Permut_refl : forall (a:Type), forall (l:(list a)), (permut l l).
Definition permut {a:Type} {a_WT:WhyType a} (l1:(list a))
(l2:(list a)): Prop := forall (x:a), ((num_occ x l1) = (num_occ x l2)).
Axiom Permut_sym : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
(permut l1 l2) -> (permut l2 l1).
Axiom Permut_refl : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
(permut l l).
Axiom Permut_trans : forall (a:Type), forall (l1:(list a)) (l2:(list a))
(l3:(list a)), (permut l1 l2) -> ((permut l2 l3) -> (permut l1 l3)).
Axiom Permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), (permut l1 l2) -> (permut l2 l1).
Axiom Permut_cons : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list
a)), (permut l1 l2) -> (permut (Cons x l1) (Cons x l2)).
Axiom Permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), (permut l1 l2) -> ((permut l2 l3) -> (permut
l1 l3)).
Axiom Permut_swap : forall (a:Type), forall (x:a) (y:a) (l:(list a)),
(permut (Cons x (Cons y l)) (Cons y (Cons x l))).
Axiom Permut_cons : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), (permut l1 l2) -> (permut (cons x l1)
(cons x l2)).
Axiom Permut_cons_append : forall (a:Type), forall (x:a) (l1:(list a))
(l2:(list a)), (permut (infix_plpl (Cons x l1) l2) (infix_plpl l1 (Cons x
l2))).
Axiom Permut_swap : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(l:(list a)), (permut (cons x (cons y l)) (cons y (cons x l))).
Axiom Permut_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a))
(l3:(list a)), (permut (infix_plpl (infix_plpl l1 l2) l3) (infix_plpl l1
(infix_plpl l2 l3))).
Axiom Permut_cons_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), (permut (List.app (cons x l1) l2)
(List.app l1 (cons x l2))).
Axiom Permut_append : forall (a:Type), forall (l1:(list a)) (l2:(list a))
(k1:(list a)) (k2:(list a)), (permut l1 k1) -> ((permut l2 k2) ->
(permut (infix_plpl l1 l2) (infix_plpl k1 k2))).
Axiom Permut_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), (permut (List.app (List.app l1 l2) l3)
(List.app l1 (List.app l2 l3))).
Axiom Permut_append_swap : forall (a:Type), forall (l1:(list a)) (l2:(list
a)), (permut (infix_plpl l1 l2) (infix_plpl l2 l1)).
Axiom Permut_append : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (k1:(list a)) (k2:(list a)), (permut l1 k1) -> ((permut l2
k2) -> (permut (List.app l1 l2) (List.app k1 k2))).
Axiom Permut_mem : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
(permut l1 l2) -> ((mem x l1) -> (mem x l2)).
Axiom Permut_append_swap : forall {a:Type} {a_WT:WhyType a},
forall (l1:(list a)) (l2:(list a)), (permut (List.app l1 l2)
(List.app l2 l1)).
Axiom Permut_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
(permut l1 l2) -> ((length l1) = (length l2)).
Axiom Permut_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), (permut l1 l2) -> ((list.Mem.mem x l1) ->
(list.Mem.mem x l2)).
Axiom Permut_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), (permut l1 l2) ->
((list.Length.length l1) = (list.Length.length l2)).
(* Why3 goal *)
Theorem WP_parameter_mergesort : forall (l:(list Z)),
match l with
| (Nil|(Cons _ Nil)) => True
| _ => (2%Z <= (length l))%Z -> forall (result:(list Z)) (result1:(list
Z)), ((1%Z <= (length result))%Z /\ ((1%Z <= (length result1))%Z /\
(permut l (infix_plpl result result1)))) -> (((0%Z <= (length l))%Z /\
((length result1) < (length l))%Z) -> forall (o:(list Z)),
((sorted o) /\ (permut o result1)) -> (((0%Z <= (length l))%Z /\
((length result) < (length l))%Z) -> forall (o1:(list Z)),
((sorted o1) /\ (permut o1 result)) -> (((sorted o1) /\ (sorted o)) ->
forall (result2:(list Z)), ((sorted result2) /\ (permut result2
(infix_plpl o1 o))) -> (permut result2 l))))
| (nil|(cons _ nil)) => True
| _ => (2%Z <= (list.Length.length l))%Z -> forall (result:(list Z))
(result1:(list Z)), ((1%Z <= (list.Length.length result))%Z /\
((1%Z <= (list.Length.length result1))%Z /\ (permut l
(List.app result result1)))) -> forall (o:(list Z)), ((sorted o) /\
(permut o result1)) -> forall (o1:(list Z)), ((sorted o1) /\ (permut o1
result)) -> (((sorted o1) /\ (sorted o)) -> forall (result2:(list Z)),
((sorted result2) /\ (permut result2 (List.app o1 o))) -> (permut
result2 l))
end.
(* YOU MAY EDIT THE PROOF BELOW *)
(* Why3 intros l. *)
destruct l; try trivial.
destruct l; try trivial.
intuition.
apply Permut_trans with (infix_plpl o1 o); auto.
apply Permut_trans with (infix_plpl result result1); auto.
apply Permut_trans with (app o1 o); auto.
apply Permut_trans with (app result result1); auto.
apply Permut_append; auto.
apply Permut_sym; auto.
Qed.
......
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