Complete this form and hit the "Save Changes" button!
No ratings
Are you sure you want to delete this code? Please type DELETE in the box below to confirm.
Are you sure you want to verify this code?
Are you sure you want to publish this code?
Are you sure you want to unpublish this code?
Are you sure you want to autogenerate the summary + description for this code?
xxxxxxxxxx
(* Generated by tptp2coqp *)
Require Import Setoid.
From Completion Require Import Plugin.
(* axioms *)
Parameter G : Set.
Parameter a2 : G.
Parameter b2 : G.
Parameter inverse : G -> G.
Parameter multiply : G -> G -> G.
(* HACK: for coq-completion *)
Hint Resolve a2 : hint_hack_compl.
Axiom ax_single_axiom : forall A B C D : G, (multiply A (inverse (multiply B (multiply C (multiply (multiply (inverse C) (inverse (multiply D B))) A))))) = D.
Complete ax_single_axiom : a2 b2 inverse multiply : hint
for ((multiply (multiply (inverse b2) b2) a2) = a2).
(* Goal *)
Theorem check : (multiply (multiply (inverse b2) b2) a2) = a2.
Proof.
lpo_autorewrite with hint.
reflexivity.
Qed.
Check check.
