;;;============================================================
;;;
;;; Subject: Generator of simplicial complexes
;;;
;;;------------------------------------------------------------
;;;
;;; Jónathan Heras Vicente
;;; Beginning date: 19-05-09
;;; End date: 21-10-09
;;;
;;;============================================================

(in-package "ACL2")

(set-verify-guards-eagerness 0)




;;;============================================================
;;;
;;; Definitions 
;;;
;;;============================================================

;;;------------------------------------------------------------
;;;
;;; Characterization functions
;;;
;;;------------------------------------------------------------


(defun simplex-p (simplex)
  (if (endp simplex)
      (equal simplex nil)
    (if (endp (cdr simplex))
	(and (equal (cdr simplex) nil) (natp (car simplex)))
      (and (natp (car simplex)) (natp (cadr simplex))
	   (< (car simplex) (cadr simplex)) 
	   (simplex-p (cdr simplex))))))

(defun list-of-simplex-p (ls)
  (if (endp ls)
      (equal ls nil)
    (and (simplex-p (car ls))
	 (list-of-simplex-p (cdr ls)))))

   

;;;--------------------------------------------------------------
;;;
;;; Generator function from a simplex
;;;
;;;--------------------------------------------------------------

(defun map-cons (x s)
  (if (endp s)
      nil
    (cons (cons x (car s))
	  (map-cons x (cdr s)))))

(defun subconjuntos (l)
  (if (endp l)
      (list nil)
    (append (subconjuntos (cdr l))
	    (map-cons (car l) (subconjuntos (cdr l))))))





;;;==============================================================
;;;
;;; Properties for the generator function from a simplex
;;;
;;;==============================================================

;;;--------------------------------------------------------------
;;;
;;; The generator function from a simplex returns a list of 
;;; simplices
;;;
;;;--------------------------------------------------------------

(defthm append-list-of-simplex-p-is-list-of-simplex-p
  (implies (and (list-of-simplex-p ls1)
		(list-of-simplex-p ls2))
	   (list-of-simplex-p (append ls1 ls2))))


(defthm list-of-simplex-p-cons-simplex-list-of-simplex-p
  (implies (and (simplex-p a)
		(list-of-simplex-p ls))
	   (list-of-simplex-p (cons a ls))))

(defthm consp-simplex=>consp-list-of-simplex-p-subconjuntos
  (implies (consp s)
	   (consp (subconjuntos s))))

(defthm simplex-p=>true-listp
  (implies (simplex-p x)
	   (true-listp x)))

(defthm true-listp-simplex=>true-listp-list-of-simplex-p-subconjuntos
  (implies (true-listp s)
	   (true-listp (subconjuntos s))))


(defthm append-map-cons
  (equal (map-cons a (append b c))
	 (append (map-cons a b) (map-cons a c))))

(defthm list-of-simplex-p-map-cons-map-cons
  (implies (and (list-of-simplex-p (map-cons b c))
		(< a b)
		(natp a)
		(natp b))
	   (list-of-simplex-p (map-cons a
					(map-cons b c)))))


(defthm list-of-simplex-p-append-1
  (implies (list-of-simplex-p (append a b))
	   (list-of-simplex-p b)))

(defthm list-of-simplex-p-append-2
  (implies (and (list-of-simplex-p (append a b))
		(true-listp a))
	   (list-of-simplex-p a)))

(defthm not-list-of-simplex-p-not-list-of-simplex-p-append-1
  (implies (and (not (list-of-simplex-p ls1))
		(consp ls1)
		(not (simplex-p (car ls1))))		
	   (not (list-of-simplex-p (append ls1 ls2)))))

(defthm car-subconjuntos-equal-nil
  (equal (car (subconjuntos ls))
	 nil))


(defthm list-of-simplex-p-map-cons-help
  (implies (and (natp a)
		(< a (car ls))
		(list-of-simplex-p (subconjuntos ls))
		(simplex-p ls)
		(consp ls))
	   (list-of-simplex-p (map-cons a (subconjuntos ls))))
)

(defthm list-of-simplex-p-subconjuntos 
  (implies (simplex-p simplex)
	   (list-of-simplex-p (subconjuntos simplex))))


;;;--------------------------------------------------------------
;;;
;;; Correction of subcojuntos
;;; 
;;;--------------------------------------------------------------


(defthm subconjuntos-member-lema1
  (implies (and (consp m)
		(not (member-equal (car m) l)))
	   (not (member-equal m (subconjuntos l)))))


(defthm member-equal-append
  (iff (member-equal x (append l m))
       (or (member-equal x l) (member-equal x m))))


(defthm member-equal-cdr-map-cons
  (implies (and (consp m)
		(not (member-equal (cdr m) l)))
	   (not (member-equal m (map-cons x l)))))

(defthm subconjunto-cerrado-por-cdr
  (implies (and (consp m)
		(member-equal m (subconjuntos l)))
	   (member-equal (cdr m) (subconjuntos l))))

(defthm subconjuntos-correccion
  (implies (member-equal m (subconjuntos l))
	   (subsetp-equal m l)))




;--------------------------------------------------------------
; Properties of subsetp-equal
;--------------------------------------------------------------

(defthm subsetp-equal-transitive
  (implies (and (subsetp-equal a b)
		(subsetp-equal b c))
	   (subsetp-equal a c)))


(defthm subsetp-equal-append
  (subsetp-equal a (append a b)))


(defthm subset-subconjuntos
  (implies (simplex-p s1)
	   (subsetp-equal (subconjuntos (cdr s1))
		     (subconjuntos s1))))


(defthm member-equal-subset-subconjuntos
  (implies (and (subsetp-equal a b)
		(member-equal c a))
	   (member-equal c b)))


(defthm simplex-p-cdr
  (implies (simplex-p a)
	   (simplex-p (cdr a))))

(defthm member-equal-car
  (implies (member-equal (car s1) s2)
	   (or (equal (car s1) (car s2))
	       (member-equal (car s1) (cdr s2))))
:rule-classes nil)

(defthm not-implies-not-subset
  (implies (and (not (consp s2))
		(consp s1))
	   (not (subsetp-equal s1 s2))))


(defthm map-cons-member-equal-consp
  (implies (and (member-equal a b)
	   (consp a))
	   (member-equal (cons c a) (map-cons c b))))

(defthm map-cons-car
  (implies (and (member-equal a (map-cons c b))
		(consp a))
	   (equal (car a) c)))


(defthm subsetp-equal-def1
  (implies (and (not (endp a))
		(subsetp-equal a b))
	   (member-equal (car a) b)))


(defthm subsetp-equal-def2
  (implies (subsetp-equal (append a b) c)
	   (subsetp-equal a c)))


(defthm subsetp-equal-def3
  (implies (and (subsetp-equal a b)
		(member-equal x a))
	   (member-equal x b)))

(defthm subsetp-equal-def4
  (implies (and (subsetp-equal a b)
		(member-equal x (cdr a)))
	   (member-equal x b)))

(defthm subsetp-equal-def5
  (implies (subsetp-equal c d)
	   (subsetp-equal (append a c) (append a d))))


(defthm subsetp-equal-def9
  (implies (and (not (endp a)) 
		(subsetp-equal a b))
	   (and (member-equal (car a) b)
		(subsetp-equal (cdr a) b))))


(defthm subsetp-equal-def10
  (implies (subsetp-equal a b)
	   (subsetp-equal (member-equal x a) b)))


(defthm append-cdr
  (implies (not (endp a))
	   (equal (append (list (car a)) (cdr a))
		  a)))


(defthm subsetp-equal-def12
  (implies (subsetp-equal a b)
	   (subsetp-equal a (cons c b)))
)

(defthm subsetp-equal-def13
  (implies (and (not (endp a))
		(subsetp-equal a c))
	   (subsetp-equal (cdr a) c))
)


(defthm subsetp-equal-property
  (implies (simplex-p a)
	   (subsetp-equal (cdr a) a)))


(defthm subsetp-equal-property2
  (subsetp-equal a a))


(defthm subsetp-equal-property3
  (implies (subsetp-equal a b)
	   (subsetp-equal (cdr a) b)))

(defthm subsetp-equal-property4
  (implies (and (simplex-p a)
		(simplex-p b)
		(subsetp-equal a b))
	   (subsetp-equal (cdr a) (cdr b))))

(defun subsetp-equal-def8-schema (a b)
  (if (not (subsetp-equal a b))
      nil
    (if (endp a)
        t
      (subsetp-equal-def8-schema (cdr a)
                            (cdr b)))))

(defthm subsetp-equal-def8
  (implies (and (simplex-p a)
		(simplex-p b)
		(subsetp-equal a b))
	   (<= (len a) (len b)))
:hints (("Goal" :induct (subsetp-equal-def8-schema a b))))


(defthm member-equal-subsetp-equal-simplex-p
  (implies (and (simplex-p s1)
		(simplex-p s2)
		(member-equal (car s1) s2)
		(subsetp-equal (cdr s1) s2))
	   (subsetp-equal s1 s2)))

(defun subsetp-equal-and-same-len=>equal-schema (s1 s2)
  (if (or (not (consp s1)) (not (simplex-p s1))
	  (not (consp s2)) (not (simplex-p s2))
	  (not (subsetp-equal s1 s2)) (not (equal (len s1) (len s2))))
      nil
    (if (endp s1)
	t
      (subsetp-equal-and-same-len=>equal-schema (cdr s1) (cdr s2)))))

(defthm subsetp-equal-and-same-len=>equal
  (implies (and (simplex-p s1)
		(simplex-p s2)
		(consp s1)
		(consp s2)
		(subsetp-equal s1 s2)
		(equal (len s1) (len s2)))
	   (equal s1 s2))
  :hints (("Goal" :induct (subsetp-equal-and-same-len=>equal-schema s1 s2)))
  :rule-classes nil)


(defthm subsetp-equal=><=len
  (implies (and (simplex-p s1)
		(simplex-p s2)
		(consp s1)
		(consp s2)
		(subsetp-equal s1 s2))
	   (<= (len s1) (len s2))))

(defthm subsetp-equal=><=len-1
  (implies (and (simplex-p s1)
		(simplex-p s2)
		(consp s1)
		(consp s2)
		(not (cdr s2))
		(subsetp-equal s1 s2))
	   (= (len s1) 1)))

(defthm subsetp-equal=><=len-2
  (implies (and (consp s2)
              (consp s1)
              (simplex-p s1)
              (not (cdr s2))
              (integerp (car s2))
              (<= 0 (car s2))
              (subsetp-equal s1 s2))
         (equal s1 (list (car s2))))
:rule-classes nil)



;--------------------------------------------------------------
; Properties of simplex-p
;--------------------------------------------------------------

(defthm <-car=>not-member-equal
  (implies (and (natp a)
		(< a (car s2))
		(simplex-p s2))
	   (not (member-equal a s2))))


(defthm equal-cadr-car=>not-member-equal
  (implies (and (simplex-p s1)
		(consp s1)
		(simplex-p s2)
		(equal (car (cdr s1)) (car s2)))
	   (not (member-equal (car s1) s2))))


(defthm simplex-p-simplex-p-cdr-subset-cdr
  (implies (and (simplex-p s1)
		(simplex-p s2)
		(subsetp-equal s1 s2))
	   (subsetp-equal (cdr s1) (cdr s2))))

;--------------------------------------------------------------
; The vertices of \sigma are in V
;--------------------------------------------------------------


(defthm vertice-subconjuntos-lemma
  (implies (and (list-of-simplex-p b)
		(consp b)
		(equal (car b) nil)
		(natp a))
	   (equal (list a)
		  (car (map-cons a b))
		  )
  ))


(defthm vertice-subconjuntos-lemma-2
  (implies (and (list-of-simplex-p b)
		(consp b)
		(equal (car b) nil)
		(natp a))
	   (member-equal (list a)
		 (map-cons a b)
		  )
  ))

(defthm vertice-subconjuntos
  (implies (and (member-equal a s)
		(natp a) ;; tambien vale (not (equal a nil))
		(simplex-p s))
	   (member-equal (list a) (subconjuntos s))))

(defthm vertice-subconjuntos2
  (implies (and (member-equal a s)
		(not (equal a nil))
		(simplex-p s))
	   (member-equal (list a) (subconjuntos s))))

(defthm vertice-subconjuntos2-al-reves
  (implies (and (not (member-equal (list a) (subconjuntos s)))
		(not (equal a nil))
		(simplex-p s))
	   (not (member-equal a s))))



(defthm subconjuntos-cdr-subconjuntos-lemma-1
  (implies (and (simplex-p s1)
		(simplex-p s2)
		(consp s1)
		(consp s2)
		(consp (cdr s1))
		(member-equal (cdr s1) (subconjuntos s2))
		(member-equal (cdr s1) (map-cons (car s2)
				       (subconjuntos (cdr s2))))
		)
	   (equal (car (cdr s1)) (car s2))))

(defthm subconjuntos-cdr-subconjuntos-lemma-2
  (implies (and (equal (car (cdr s1)) (car s2))
		(simplex-p s1)
		(simplex-p s2)
		(consp s1)
		(consp s2)
		(consp (cdr s1))				
		)
	   (not (member-equal (car s1) s2))))


(defthm subconjuntos-cdr-subconjuntos-lemma-3
  (implies (and (simplex-p s1)
		(simplex-p s2)
		(consp s1)
		(consp s2)
		(consp (cdr s1))
		(member-equal (car s1) s2)
		(member-equal (cdr s1) (subconjuntos s2))
		)
	  (not (member-equal (cdr s1) (map-cons (car s2)
				       (subconjuntos (cdr s2))))) ))

(defthm subconjuntos-cdr-subconjuntos-lemma-4
  (implies (and (simplex-p s1)
		(simplex-p s2)
		(consp s1)
		(consp s2)
		(consp (cdr s1))
		(member-equal (car s1) s2)
		(member-equal (cdr s1) (subconjuntos s2))
		)
	  (or (member-equal (cdr s1) (subconjuntos (cdr s2)))
	   (member-equal (cdr s1) (map-cons (car s2)
				       (subconjuntos (cdr s2)))) ))
  :rule-classes nil)

(defthm subconjuntos-cdr-subconjuntos
  (implies (and (simplex-p s1)
		(simplex-p s2)
		(consp s1)
		(consp s2)
		(consp (cdr s1))
		(member-equal (car s1) s2)
		(member-equal (cdr s1) (subconjuntos s2))
		)
	   (member-equal (cdr s1) (subconjuntos (cdr s2))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance subconjuntos-cdr-subconjuntos-lemma-4)
	       (:instance subconjuntos-cdr-subconjuntos-lemma-3)
	       ))))

(in-theory (disable subconjuntos-cdr-subconjuntos
		    subconjuntos-cdr-subconjuntos-lemma-3
		    subconjuntos-cdr-subconjuntos-lemma-2
		    subconjuntos-cdr-subconjuntos-lemma-1))

;--------------------------------------------------------------
; Lemmas for subconjuntos-completitud
;--------------------------------------------------------------

(defthm member-equal-subconjuntos-cdr=>member-equal-subconjuntos
  (implies (and (simplex-p s1)
		(member-equal a (subconjuntos (cdr s1))))
	   (member-equal a (subconjuntos s1))))

(defthm not-member-equal-subconjuntos-cdr=>not-member-equal-subconjuntos
  (implies (and (simplex-p s1)
		(not (member-equal a (subconjuntos s1)))
		)
	  (not (member-equal a (subconjuntos (cdr s1))))))



;;;--------------------------------------------------------------
;;;
;;; Completeness of subcojuntos
;;; 
;;;--------------------------------------------------------------

(defthm consp-a-subconjuntos-a
  (implies (consp a)
	   (subconjuntos a)))

(defthm simplex-p=>consp-subconjuntos
  (implies (simplex-p a)
	   (consp (subconjuntos a))))



(defthm a-binsubconjuntos=>a+binsubconjuntos-lemma-1
  (implies (and (consp s1)
              (consp (cdr s1))
              (integerp (car s1))
              (<= 0 (car s1))
              (integerp (cadr s1))
              (<= 0 (cadr s1))
              (< (car s1) (cadr s1))
              (implies (and (member-equal (list a)
                                          (subconjuntos (cdr s1)))
                            (natp a)
                            (simplex-p (cdr s1))
                            (simplex-p s2)
                            (member-equal s2 (subconjuntos (cdr s1)))
                            (< a (car s2)))
                       (member-equal (cons a s2)
                                     (subconjuntos (cdr s1))))
              (member-equal (list a)
                            (subconjuntos s1))
              (integerp a)
              (<= 0 a)
              (simplex-p s1)
              (simplex-p s2)
              (member-equal s2 (subconjuntos s1))
              (< a (car s2))
	      (member-equal (list a)
                            (subconjuntos (cdr s1)))
	      (member-equal s2
                            (subconjuntos (cdr s1)))
	      )
         (member-equal (cons a s2)
                       (subconjuntos s1))))


(defthm a-binsubconjuntos=>a+binsubconjuntos-lemma-2
  (implies (and (consp s1)
              (consp (cdr s1))
              (integerp (car s1))
              (<= 0 (car s1))
              (integerp (cadr s1))
              (<= 0 (cadr s1))
              (< (car s1) (cadr s1))
              (implies (and (member-equal (list a)
                                          (subconjuntos (cdr s1)))
                            (natp a)
                            (simplex-p (cdr s1))
                            (simplex-p s2)
                            (member-equal s2 (subconjuntos (cdr s1)))
                            (< a (car s2)))
                       (member-equal (cons a s2)
                                     (subconjuntos (cdr s1))))
              (member-equal (list a)
                            (subconjuntos s1))
              (integerp a)
              (<= 0 a)
              (simplex-p s1)
              (simplex-p s2)
              (member-equal s2 (subconjuntos s1))
              (< a (car s2))
	      (member-equal (list a)
                            (subconjuntos (cdr s1)))
	      (member-equal s2 (map-cons (car s1)
                            (subconjuntos (cdr s1))))
	      )
         (member-equal (cons a s2)
                       (subconjuntos s1))))

(defthm a-binsubconjuntos=>a+binsubconjuntos-lemma3-help1
  (implies (and (natp a)
		(simplex-p s1)
		(member-equal (list a) (map-cons (car s1)
						 (subconjuntos (cdr s1))))
		)
	   (= a (car s1)))
:rule-classes nil)

(defthm map-simplex-car
    (implies (and (member-equal a (map-cons c b))
                  (simplex-p a))
             (equal (car a) c)))


(defthm a-binsubconjuntos=>a+binsubconjuntos-lemma-3
  (implies (and (consp s1)
              (consp (cdr s1))
              (integerp (car s1))
              (<= 0 (car s1))
              (integerp (cadr s1))
              (<= 0 (cadr s1))
              (< (car s1) (cadr s1))
              (implies (and (member-equal (list a)
                                          (subconjuntos (cdr s1)))
                            (natp a)
                            (simplex-p (cdr s1))
                            (simplex-p s2)
                            (member-equal s2 (subconjuntos (cdr s1)))
                            (< a (car s2)))
                       (member-equal (cons a s2)
                                     (subconjuntos (cdr s1))))
              (member-equal (list a)
                            (subconjuntos s1))
              (integerp a)
              (<= 0 a)
              (simplex-p s1)
              (simplex-p s2)
              (member-equal s2 (subconjuntos s1))
              (< a (car s2))
	      (member-equal (list a) (map-cons (car s1)
                            (subconjuntos (cdr s1)))
                            )
	      (member-equal s2 (map-cons (car s1)
                            (subconjuntos (cdr s1))))
	      )
         (member-equal (cons a s2)
                       (subconjuntos s1)))
:hints (("Goal" :do-not-induct t
	 :use ((:instance map-simplex-car (a s2)
			  (c (car s1))
			  (b (subconjuntos (cdr s1))))
	       (:instance a-binsubconjuntos=>a+binsubconjuntos-lemma3-help1
			  (a a)
			  (s1 s1))))))



(defthm map-cons-member-equal-simplex-p
  (implies (and (member-equal a b)
	   (simplex-p a))
	   (member-equal (cons c a) (map-cons c b))))

(defthm a-binsubconjuntos=>a+binsubconjuntos-lemma-4
  (implies (and (consp s1)
              (consp (cdr s1))
              (integerp (car s1))
              (<= 0 (car s1))
              (integerp (cadr s1))
              (<= 0 (cadr s1))
              (< (car s1) (cadr s1))
              (implies (and (member-equal (list a)
                                          (subconjuntos (cdr s1)))
                            (natp a)
                            (simplex-p (cdr s1))
                            (simplex-p s2)
                            (member-equal s2 (subconjuntos (cdr s1)))
                            (< a (car s2)))
                       (member-equal (cons a s2)
                                     (subconjuntos (cdr s1))))
              (member-equal (list a)
                            (subconjuntos s1))
              (integerp a)
              (<= 0 a)
              (simplex-p s1)
              (simplex-p s2)
              (member-equal s2 (subconjuntos s1))
              (< a (car s2))
	      (member-equal (list a) (map-cons (car s1)
                            (subconjuntos (cdr s1)))
                            )
	      (member-equal s2 (subconjuntos (cdr s1)))
	      )
         (member-equal (cons a s2)
                       (subconjuntos s1)))
:hints (("Goal" :do-not-induct t
	 :use ((:instance a-binsubconjuntos=>a+binsubconjuntos-lemma3-help1
			  (a a)
			  (s1 s1))
	       (:instance map-cons-member-equal-simplex-p
			  (a s2)
			  (b (subconjuntos (cdr s1)))
			  (c a))
	       )))
)

(defthm member-equal-append-subconjuntos
  (implies (member-equal x (subconjuntos s))
       (or (member-equal x (subconjuntos (cdr s))) 
	   (member-equal x (map-cons (car s) (subconjuntos (cdr s))))))
  :rule-classes nil)

(defthm a-binsubconjuntos=>a+binsubconjuntos-lemma-5
  (implies (and (consp s1)
              (consp (cdr s1))
              (integerp (car s1))
              (<= 0 (car s1))
              (integerp (cadr s1))
              (<= 0 (cadr s1))
              (< (car s1) (cadr s1))
              (implies (and (member-equal (list a)
                                          (subconjuntos (cdr s1)))
                            (natp a)
                            (simplex-p (cdr s1))
                            (simplex-p s2)
                            (member-equal s2 (subconjuntos (cdr s1)))
                            (< a (car s2)))
                       (member-equal (cons a s2)
                                     (subconjuntos (cdr s1))))
              (member-equal (list a)
                            (subconjuntos s1))
              (integerp a)
              (<= 0 a)
              (simplex-p s1)
              (simplex-p s2)
              (member-equal s2 (subconjuntos s1))
              (< a (car s2))
	      )
         (member-equal (cons a s2)
                       (subconjuntos s1)))
:hints (("Goal" :do-not-induct t
	 :use ((:instance member-equal-append-subconjuntos (x (list a))
			  (s s1))
	       (:instance member-equal-append-subconjuntos (x s2)
			  (s s1))
	       (:instance a-binsubconjuntos=>a+binsubconjuntos-lemma-1)
	       (:instance a-binsubconjuntos=>a+binsubconjuntos-lemma-2)
	       (:instance a-binsubconjuntos=>a+binsubconjuntos-lemma-3)
	       (:instance a-binsubconjuntos=>a+binsubconjuntos-lemma-4)
	       )))
)


(defthm a-binsubconjuntos=>a+binsubconjuntos
  (implies (and (member-equal (list a) (subconjuntos s1))
		(natp a)
		(simplex-p s1)
		(simplex-p s2)
		(member-equal s2 (subconjuntos s1))
		(< a (car s2)))
	   (member-equal (cons a s2) (subconjuntos s1)))
:hints (("Subgoal *1/4'" :do-not-induct t
	 :use ((:instance a-binsubconjuntos=>a+binsubconjuntos-lemma-5)	       
	       ))))




(defthm subconjuntos-completitud-lemma-a-0
  (implies (and (consp s2)
		(member-equal (cdr s1) (subconjuntos (cdr s2)))
		(simplex-p s1)
		(simplex-p s2)
		(subsetp-equal s1 s2)
		(subsetp-equal s1 (cdr s2)))
         (member-equal s1 (subconjuntos s2))))



(defthm subconjuntos-completitud-lemma-a
  (implies (and (consp s2)
              (implies (and (simplex-p (cdr s1))
                            (simplex-p (cdr s2))
                            (subsetp-equal (cdr s1) (cdr s2)))
                       (member-equal (cdr s1) (subconjuntos (cdr s2))))
              (simplex-p s1)
              (simplex-p s2)
              (subsetp-equal s1 s2)
	      (subsetp-equal s1 (cdr s2)))
         (member-equal s1 (subconjuntos s2))))



(defthm subconjuntos-completitud-lemma-b
  (implies (and (consp s2)
              (implies (and (simplex-p (cdr s1))
                            (simplex-p (cdr s2))
                            (subsetp-equal (cdr s1) (cdr s2)))
                       (member-equal (cdr s1) (subconjuntos (cdr s2))))
              (simplex-p s1)
              (simplex-p s2)
              (subsetp-equal s1 s2)
	      (not (subsetp-equal s1 (cdr s2))))
         (member-equal s1 (subconjuntos s2))))


(defthm subconjuntos-completitud-lemma
  (implies (and (consp s2)
              (implies (and (simplex-p (cdr s1))
                            (simplex-p (cdr s2))
                            (subsetp-equal (cdr s1) (cdr s2)))
                       (member-equal (cdr s1) (subconjuntos (cdr s2))))
              (simplex-p s1)
              (simplex-p s2)
              (subsetp-equal s1 s2)
	      )
         (member-equal s1 (subconjuntos s2)))
:hints (("Goal" :do-not-induct t
	 :use ((:instance subconjuntos-completitud-lemma-a)
	       (:instance subconjuntos-completitud-lemma-b)))))



(defun subconjuntos-completitud-schema2 (s1 s2)
  (declare (xargs :measure (acl2-count s2)))
  (if (or (not (simplex-p s1))
	  (not (simplex-p s2))
	  (not (subsetp-equal s1 s2)))
      nil
    (if (endp s2)
	t
      (subconjuntos-completitud-schema2 (cdr s1) (cdr s2)))))

(defthm subconjuntos-completitud
  (implies (and (simplex-p s1)
		(simplex-p s2)
		(subsetp-equal s1 s2))
	   (member-equal s1 (subconjuntos s2)))
:hints (("Goal" :induct (subconjuntos-completitud-schema2 s1 s2))
	("Subgoal *1/2" :do-not-induct t
	 :use ((:instance subconjuntos-completitud-lemma))
	 )
	)) 





;;;--------------------------------------------------------------
;;;
;;; For every \sigma \in V then \sigma' \subset \sigma implies
;;; \sigma' \in V
;;;
;;;--------------------------------------------------------------


(defthm simplicial-complex-result
  (implies (and (simplex-p s1)
		(simplex-p s2)
		(simplex-p s3)
		(member-equal s1 (subconjuntos s2))
		(subsetp-equal s3 s1))
	   (member-equal s3 (subconjuntos s2))))




;;;==============================================================
;;;
;;; Theorems for genera-simplicial-complex
;;; This function generates from a list of simplices a simplicial
;;; complex but with duplicates
;;;
;;;--------------------------------------------------------------
;;;
;;; To be a simplicial complex the genera-simplicial-complex must:
;;;     1. return a list of simplices
;;;     2. The vertices of the initial list of simplices must be
;;;        in the generated simplicial complex
;;;     3. Any face of a simplex from the generated simplicial
;;;        complex is also in the generated simplicial complex
;;;
;;;==============================================================


(defun genera-simplicial-complex (ls)
  (if (endp ls)
      nil
    (append (subconjuntos (car ls))
	    (genera-simplicial-complex (cdr ls)))))



(defthm genera-simplicial-complex-is-a-list-of-simplex-p
  (implies (list-of-simplex-p s2)
	   (list-of-simplex-p (genera-simplicial-complex s2))))

(defthm simplicial-complex-result-full
  (implies (and (simplex-p s1)
		(simplex-p s3)
		(list-of-simplex-p s2)
		(member-equal s1 (genera-simplicial-complex s2))
		(subsetp-equal s3 s1))
	   (member-equal s3 (genera-simplicial-complex s2))))

(defthm vertices-genera-simplicial-complex
  (implies (and (member-equal a s)
		(natp a) 
		(member-equal s ls)
		(list-of-simplex-p ls))
	   (member-equal (list a) (genera-simplicial-complex ls)))
  )


;;;===========================================================================
;;;
;;; remove-duplicates does not have duplicates
;;;
;;;===========================================================================


(defun without-duplicates (ls)
  (if (or (endp ls)
	  (endp (cdr ls)))
      t
    (and (not (member-equal (car ls) (cdr ls)))
	 (without-duplicates (cdr ls)))))


(defthm not-member=>not-member-remove
  (implies (not (member-equal a b))
	   (not (member-equal a (remove-duplicates-equal b)))))

(defthm without-duplicates-remove-duplicates
  (implies (list-of-simplex-p ls)
	   (without-duplicates (remove-duplicates-equal ls))))





;;;==============================================================
;;;
;;; Theorems for simplicial-complex-generator
;;; This function generates from a list of simplices a simplicial
;;; complex but without duplicates
;;;
;;;--------------------------------------------------------------
;;;
;;; To be a simplicial complex the simplicial-complex-generator
;;; must:
;;;     1. return a list of simplices
;;;     2. The vertices of the initial list of simplices must be
;;;        in the generated simplicial complex
;;;     3. Any face of a simplex from the generated simplicial
;;;        complex is also in the generated simplicial complex
;;;
;;;==============================================================

(defun simplicial-complex-generator (ls)
  (remove-duplicates-equal (genera-simplicial-complex ls)))


;;;===========================================================================
;;;
;;; correccion del algoritmo
;;;
;;;===========================================================================

(encapsulate

 ()

 (local (defthm not-endp-not-endp-remove-duplicates
  (implies (not (endp a))
	   (not (endp (remove-duplicates a))))))

 (local(defthm subsetp-equal=>subsetp-equal-append
  (implies (subsetp-equal a b)
	   (subsetp-equal a (append c b)))))


 (local (defthm endp-cdr-list-of-simplex
  (implies (and (list-of-simplex-p a)
		(not (consp (cdr a))))
	   (endp (cdr a)))))

 (local (defthm consp-subconjuntos
  (implies (simplex-p a)
	   (consp (subconjuntos a)))))

 (local(defthm consp-append
  (implies (consp a) (consp (append a b)))))


 (local(defthm not-endp=>not-endp-genera-simplicial-comples
  (implies (and (list-of-simplex-p facets)
		(not (endp facets)))
	   (not (endp (genera-simplicial-complex facets))))))

 (local(defthm facets-in-genera-simplicial-complex
  (implies (list-of-simplex-p facets)
	   (subsetp-equal facets
		     (genera-simplicial-complex facets)))))


 (local(defthm remove-duplicates-equal-lemma-1
  (implies (member-equal a b)
	   (member-equal a (remove-duplicates-equal b)))))

 (local(defthm subsetp-equal-subsetp-equal-remove-duplicates
  (implies (subsetp-equal a b)
	   (subsetp-equal a (remove-duplicates-equal b)))))


 (local(defthm facets-in-simplicial-complex-generator
  (implies (list-of-simplex-p facets)
	   (subsetp-equal facets
		     (simplicial-complex-generator facets))))
  )


 (defun subset-of-some-p (m l)
  (cond ((endp l) nil)
	((subsetp-equal m (car l)) t)
	(t (subset-of-some-p m (cdr l)))))



 (local(defthm genera-simplicial-complex-correccion
  (implies (member-equal m (genera-simplicial-complex facets))
	   (subset-of-some-p m facets))))


 (defthm simplicial-complex-generator-correccion
  (implies (member-equal m (simplicial-complex-generator facets))
	   (subset-of-some-p m facets))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance remove-duplicates-equal-lemma-1
			    (a m)
			    (b (genera-simplicial-complex facets)))
		 (:instance genera-simplicial-complex-correccion)))))

)



(defthm simplicial-complex-generator-theorem-1-lemma
  (implies (list-of-simplex-p s2)
	   (list-of-simplex-p (remove-duplicates-equal s2))))

(defthm remove-duplicates-equal-lemma-1
  (implies (member-equal a b)
	   (member-equal a (remove-duplicates-equal b))))


(defthm remove-duplicates-equal-lemma-2
  (implies (member-equal a (remove-duplicates-equal b))
	   (member-equal a b)))



(defthm simplicial-complex-generator-lemma-1
  (implies (and (simplex-p s1)
		(list-of-simplex-p s2)
		(member-equal s1 (simplicial-complex-generator s2))
		)
	   (member-equal s1 (genera-simplicial-complex s2))))


(defthm simplicial-complex-generator-lemma-2
  (implies (and (simplex-p s1)		
		(list-of-simplex-p s2)
		(member-equal s1 (genera-simplicial-complex s2))
		)
	   (member-equal s1 (simplicial-complex-generator s2))
	   ))

(defthm list-natp-is-simplex-p
  (implies (natp a)
	   (simplex-p (list a))))


(defthm simplicial-complex-generator-theorem-1
  (implies (list-of-simplex-p ls)
	   (and (list-of-simplex-p (simplicial-complex-generator ls))
		(without-duplicates (simplicial-complex-generator ls))))
  :hints (("Goal" :in-theory (disable remove-duplicates-equal-lemma-1
		    remove-duplicates-equal-lemma-2
		    genera-simplicial-complex))))
  

(defthm simplicial-complex-generator-theorem-2
  (implies (and (member-equal a s)
		(natp a) 
		(member-equal s ls)
		(list-of-simplex-p ls))
	   (member-equal (list a) (simplicial-complex-generator ls)))
 :hints (("Goal" :do-not-induct t
	  :use ((:instance list-natp-is-simplex-p)
		(:instance vertices-genera-simplicial-complex)
		(:instance simplicial-complex-generator-lemma-2
			   (s1 (list a))
			   (s2 ls))))))

(defthm simplicial-complex-generator-theorem-3
  (implies (and (simplex-p s1)
		(simplex-p s3)
		(list-of-simplex-p ls)
		(member-equal s1 (simplicial-complex-generator ls))
		(subsetp-equal s3 s1))
	   (member-equal s3 (simplicial-complex-generator ls))))




;;;==============================================================
;;;
;;; Propiedad de la intersección
;;;
;;;--------------------------------------------------------------
;;;
;;; The intersection of any two simplices \sigma_1, \sigma_2 \in 
;;; \mathcal{K} is a face of both \sigma_1 and \sigma_2.
;;;
;;;==============================================================


(defun intersect (x y)
  (cond ((endp x) nil)
	((member-equal (car x) y) (cons (car x) 
					(intersect (cdr x) y)))
	(t (intersect (cdr x) y))))



(defthm simplex-simplex-subsetp-equal-intersect-1
  (implies (and (simplex-p x)
		(simplex-p y))
	   (subsetp-equal (intersect x y) x))
  :hints (("Goal" :in-theory (disable remove-duplicates-equal))))


(defthm simplex-simplex-subsetp-equal-intersect-2
  (implies (and (simplex-p x)
		(simplex-p y))
	   (subsetp-equal (intersect x y) y))
  :hints (("Goal" :in-theory (disable remove-duplicates-equal))))


(defthm simplex-p-member-equal-list-of-simplex
  (implies (and (list-of-simplex-p ls)
		(member-equal s ls))
	   (simplex-p s)))

(defthm simplex-p-member-equal-simplicial-complex-generator
  (implies (and (list-of-simplex-p ls)
		(member-equal s (simplicial-complex-generator ls)))
	   (simplex-p s))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance simplicial-complex-generator-theorem-1)
		 (:instance simplex-p-member-equal-list-of-simplex
			    (ls (simplicial-complex-generator ls)))))))

(defthm property-intersection
  (implies (and (list-of-simplex-p ls)
		(member-equal s1 (simplicial-complex-generator ls))
		(member-equal s2 (simplicial-complex-generator ls)))
	   (and (subsetp-equal (intersect s1 s2) s1)
		(subsetp-equal (intersect s1 s2) s2)))
  :hints (("Goal" :in-theory (disable simplicial-complex-generator))))





;;;===========================================================================
;;;
;;; Property about the faces of a simplex
;;;
;;;---------------------------------------------------------------------------
;;;
;;; The number of faces of a simplex is 2^len simplex
;;;
;;;===========================================================================


(defthm len-append 
  (equal (len (append a b))
	 (+ (len a) (len b))))

(defthm len-map-cons
  (equal (len (map-cons a b))
	 (len b)))

(encapsulate
 ()

 (local (include-book "arithmetic-4/top" :dir :system))
 
 
 (defthm expt-2-2-n
   (implies (natp n)
	    (equal (+ (expt 2 n) (expt 2 n))
		   (expt 2 (1+ n))))
   :hints (("Goal" :in-theory (enable expt))))

)


(defthm faces-of-a-simplex
  (implies (simplex-p x)
	   (equal (len (subconjuntos x))
		  (expt 2 (len x)))))