Show:
(<=>
 (exists ?Y
  (and
   (forall ?X
    (<=>
     (f ?X)
     (= ?X ?Y)))
   (g ?Y)))
 (and
  (exists ?Y
   (forall ?X
    (<=>
     (f ?X)
     (= ?X ?Y))))
  (forall ?X
   (=>
    (f ?X)
    (g ?X)))))

Proof Trace

Proof Steps
1   2   3   4   5   6   7  
1: To prove:
(<=>
 (exists ?Y
  (and
   (forall ?X
    (<=>
     (f ?X)
     (= ?X ?Y)))
   (g ?Y)))
 (and
  (exists ?Y-1
   (forall ?X-2
    (<=>
     (f ?X-2)
     (= ?X-2 ?Y-1))))
  (forall ?X-3
   (=>
    (f ?X-3)
    (g ?X-3)))))
 Split the equivalence, yielding:

2:
(=>
 (exists ?Y
  (and
   (forall ?X
    (<=>
     (f ?X)
     (= ?X ?Y)))
   (g ?Y)))
 (and
  (exists ?Y-1
   (forall ?X-2
    (<=>
     (f ?X-2)
     (= ?X-2 ?Y-1))))
  (forall ?X-3
   (=>
    (f ?X-3)
    (g ?X-3)))))

3:
(=>
 (and
  (exists ?Y-1
   (forall ?X-2
    (<=>
     (f ?X-2)
     (= ?X-2 ?Y-1))))
  (forall ?X-3
   (=>
    (f ?X-3)
    (g ?X-3))))
 (exists ?Y
  (and
   (forall ?X
    (<=>
     (f ?X)
     (= ?X ?Y)))
   (g ?Y))))
2: To prove:
(=>
 (exists ?Y
  (and
   (forall ?X
    (<=>
     (f ?X)
     (= ?X ?Y)))
   (g ?Y)))
 (and
  (exists ?Y-1
   (forall ?X-2
    (<=>
     (f ?X-2)
     (= ?X-2 ?Y-1))))
  (forall ?X-3
   (=>
    (f ?X-3)
    (g ?X-3)))))
 Assume the antecedent and prove: 
4:
(and
 (exists ?Y-1
  (forall ?X-2
   (<=>
    (f ?X-2)
    (= ?X-2 ?Y-1))))
 (forall ?X-3
  (=>
   (f ?X-3)
   (g ?X-3))))

4: To prove:
(and
 (exists ?Y-1
  (forall ?X-2
   (<=>
    (f ?X-2)
    (= ?X-2 ?Y-1))))
 (forall ?X-3
  (=>
   (f ?X-3)
   (g ?X-3))))
 Split the conjunction and prove both: 
6:
(exists ?Y-1
 (forall ?X-2
  (<=>
   (f ?X-2)
   (= ?X-2 ?Y-1))))

7:
(forall ?X-3
 (=>
  (f ?X-3)
  (g ?X-3)))

6: Using the Model Elimination prover,

Show: 

(exists ?Y-1
 (forall ?X-2
  (<=>
   (f ?X-2)
   (= ?X-2 ?Y-1))))

Assuming:

  • (exists ?Y
 (and
  (forall ?X
   (<=>
    (f ?X)
    (= ?X ?Y)))
  (g ?Y)))
The Model Elimination proof succeeded.
Proved in 3 ME inference steps creating 23 clauses taking 0.087 seconds.

7: Using the Model Elimination prover,

Show: 

(forall ?X-3
 (=>
  (f ?X-3)
  (g ?X-3)))

Assuming:

  • (exists ?Y
 (and
  (forall ?X
   (<=>
    (f ?X)
    (= ?X ?Y)))
  (g ?Y)))
The Model Elimination proof succeeded.
Proved in 3 ME inference steps creating 13 clauses taking 0.021 seconds.

3: To prove:
(=>
 (and
  (exists ?Y-1
   (forall ?X-2
    (<=>
     (f ?X-2)
     (= ?X-2 ?Y-1))))
  (forall ?X-3
   (=>
    (f ?X-3)
    (g ?X-3))))
 (exists ?Y
  (and
   (forall ?X
    (<=>
     (f ?X)
     (= ?X ?Y)))
   (g ?Y))))
 Assume the antecedent and prove: 
5:
(exists ?Y
 (and
  (forall ?X
   (<=>
    (f ?X)
    (= ?X ?Y)))
  (g ?Y)))

5: Using the Model Elimination prover,

Show: 

(exists ?Y
 (and
  (forall ?X
   (<=>
    (f ?X)
    (= ?X ?Y)))
  (g ?Y)))

Assuming:

  • (and
 (exists ?Y-1
  (forall ?X-2
   (<=>
    (f ?X-2)
    (= ?X-2 ?Y-1))))
 (forall ?X-3
  (=>
   (f ?X-3)
   (g ?X-3))))
The Model Elimination proof succeeded.
Proved in 7 ME inference steps creating 50 clauses taking 0.154 seconds.
Conclusion
Proved creating 86 clauses taking 0.262 seconds.
Proof Steps
1   2   3   4   5   6   7  

Result: proved