How to use Z3 SMT-LIB to prove theorems for the group D3

Question

The table of products for the group D3 is :

Using the following Z3 SMT-LIB code is possible to obtain a representation:

(set-option :mbqi true)
(declare-sort S)
(declare-fun f (S S) S)
(declare-fun g (S) S)
(declare-const E S)
(declare-const R1 S)
(declare-const R2 S)
(declare-const R3 S)
(declare-const R4 S)
(declare-const R5 S)
(assert (forall ((x S))
            (= (f x E) x)))
(assert (forall ((x S))
            (= (f E x) x)))               
(assert (= (f R1 R1) R2))
(assert (= (f R1 R2) E))
(assert (= (f R1 R3) R4))
(assert (= (f R1 R4) R5))
(assert (= (f R1 R5) R3))
(assert (= (f R2 R1) E))
(assert (= (f R2 R2) R1))
(assert (= (f R2 R3) R5))
(assert (= (f R2 R4) R3))
(assert (= (f R2 R5) R4))
(assert (= (f R3 R1) R5))
(assert (= (f R3 R2) R4))
(assert (= (f R3 R3) E))
(assert (= (f R3 R4) R2))
(assert (= (f R3 R5) R1))
(assert (= (f R4 R1) R3))
(assert (= (f R4 R2) R5))
(assert (= (f R4 R3) R1))
(assert (= (f R4 R4) E))
(assert (= (f R4 R5) R2))
(assert (= (f R5 R1) R4))
(assert (= (f R5 R2) R3))
(assert (= (f R5 R3) R2))
(assert (= (f R5 R4) R1))
(assert (= (f R5 R5) E))
(assert (= (g E) E))
(assert (= (g R1) R2))
(assert (= (g R2) R1))
(assert (= (g R3) R3))
(assert (= (g R4) R4))
(assert (= (g R5) R5))
(check-sat)
(get-model)

In this code the function f gives the product and the function g gives the inverse. The corresponding output is:

sat 
(model 
;; universe for S: 
;; S!val!1 S!val!3 S!val!5 S!val!4 S!val!0 S!val!2 
;; -----------
;; definitions for universe elements: 
(declare-fun S!val!1 () S) 
(declare-fun S!val!3 () S) 
(declare-fun S!val!5 () S) 
(declare-fun S!val!4 () S) 
(declare-fun S!val!0 () S) 
(declare-fun S!val!2 () S) 
;; cardinality constraint: 
(forall ((x S)) (or (= x S!val!1) (= x
  S!val!3) (= x S!val!5) (= x S!val!4) (= x S!val!0) (= x S!val!2)))
;; ----------- 
(define-fun R1 () S S!val!0) 
(define-fun R3 () S S!val!3) 
(define-fun R2 () S S!val!1) 
(define-fun R4 () S S!val!4) 
(define-fun R5 () S S!val!5) 
(define-fun E () S S!val!2) 
(define-fun g ((x!1 S)) S 
 (ite (= x!1 S!val!0) S!val!1 
 (ite (= x!1 S!val!1) S!val!0 
 (ite (= x!1 S!val!3) S!val!3 
 (ite (= x!1 S!val!4) S!val!4 
 (ite (= x!1 S!val!5) S!val!5 S!val!2)))))) 
(define-fun f ((x!1 S) (x!2 S)) S 
 (ite (and (= x!1 S!val!0) (= x!2 S!val!0)) S!val!1 
 (ite (and (= x!1 S!val!0) (= x!2 S!val!1)) S!val!2 
 (ite (and (= x!1 S!val!0) (= x!2 S!val!3)) S!val!4 
 (ite (and (= x!1 S!val!0) (= x!2 S!val!4)) S!val!5 
 (ite (and (= x!1 S!val!0) (= x!2 S!val!5)) S!val!3 
 (ite (and (= x!1 S!val!1) (= x!2 S!val!0)) S!val!2 
 (ite (and (= x!1 S!val!1) (= x!2 S!val!1)) S!val!0 
 (ite (and (= x!1 S!val!1) (= x!2 S!val!3)) S!val!5 
 (ite (and (= x!1 S!val!1) (= x!2 S!val!4)) S!val!3 
 (ite (and (= x!1 S!val!1) (= x!2 S!val!5)) S!val!4 
 (ite (and (= x!1 S!val!3) (= x!2 S!val!0)) S!val!5 
 (ite (and (= x!1 S!val!3) (= x!2 S!val!1)) S!val!4 
 (ite (and (= x!1 S!val!3) (= x!2 S!val!3)) S!val!2 
 (ite (and (= x!1 S!val!3) (= x!2 S!val!4)) S!val!1 
 (ite (and (= x!1 S!val!3) (= x!2 S!val!5)) S!val!0 
 (ite (and (= x!1 S!val!4) (= x!2 S!val!0)) S!val!3 
 (ite (and (= x!1 S!val!4) (= x!2 S!val!1)) S!val!5 
 (ite (and (= x!1 S!val!4) (= x!2 S!val!3)) S!val!0 
 (ite (and (= x!1 S!val!4) (= x!2 S!val!4)) S!val!2 
 (ite (and (= x!1 S!val!4) (= x!2 S!val!5)) S!val!1 
 (ite (and (= x!1 S!val!5) (= x!2 S!val!0)) S!val!4 
 (ite (and (= x!1 S!val!5) (= x!2 S!val!1)) S!val!3 
 (ite (and (= x!1 S!val!5) (= x!2 S!val!3)) S!val!1 
 (ite (and (= x!1 S!val!5) (= x!2 S!val!4)) S!val!0 
 (ite (and (= x!1 S!val!5) (= x!2 S!val!5)) S!val!2 
 (ite (= x!1 S!val!2) x!2 x!1))))))))))))))))))))))))))) 
 )

Using this representation is possible to prove the following theorem:

The proof is:

(eval (f (f R3 R1) (g R3)))
(eval R2)

with the output

S!val!1 
S!val!1

Run the full code here

The question is: It is possible to get a more elegant proof of this theorem?

Answer 1

You want to check whether the assertions imply that (f (f R3 R1) (g R3)) and R2 are equal. You can accomplish that by showing that the the assertions above plus the assertion

    (assert (not (= (f (f R3 R1) (g R3)) R2)))

are unsatisfiable. You can add the following additional assertion before the (check-sat). Here is the updated example.

You may also use the following command sequence after your original set of assertions

    (check-sat) ; check if the set of assertions is consistent
    (get-model) ; display the model
    ; assert the negation of the conjecture
    (assert (not (= (f (f R3 R1) (g R3)) R2))) 
    (check-sat) 

Here is the updated example with this command sequence.