Miscellany

void lista<T> :: sacar(const T &){
    int i = 0;
	Lista<T> listaAux;
		//Estado inicial: 
		//Vale: i == 0  &&   listaAux == []  && this == pre(this);
	while(i < this.length()){
			//invariante: this == pre(This) && 0 <= i <= |pre(this)| &&  listaAux = [ this[x] | x <- [0..i), this[x] != e];
			//variante: |this| - i;
			//Estado AntesIf: Vale I;
		if(this.iesimo(i) != e){
		    listaAux.agregar(this.iesimo(i));
		}
		//Estado DespuesIf
		//Qc: (this[i] == e && listaAux == listaAux@AntesIf) || (this[i] != e && listaAux == listaAux@AntesIf ++ this[i])
		//se acepta Qc como verdadero, se demustra al final
		i++;
		//estado b
	}
		//Q:  this == pre(This) && listaAux = [ this[x] | x <- [0..|this|), this[x] != e]  /*la demostracion del ciclo a 	continuacion */
		//Estado luegoDelCiclo:
		//vale this == pre(This) && listaAux ==[ this[x] | x <- [0..|this|), this[x] != e]
		//implica: listaAux == [pre(this)[x] | x <-[0..|pre(this)|), pre(this)[x] != e]
	this = listaAux;
		//estado asignacion:
	// vale this == listaAux@luegoDelCiclo
	//implica this == [pre(this)[x] | x <-[0..|pre(this)|),pre(this)[x] != e]

/*demostracion del ciclo mediante teorema del invariante*/

// 1. P -> I
//Supongo q vale p:
//Vale: i == 0  &&   listaAux == []  && this == pre(this)
//como this == pre(this) se satisface.
//como |this| >= 0 && i == 0,
//vale 0 <= i <= |this|
//como i==0, [0..i)  es [0..0) q es []
//implica [ this[x] | x <-[o..i), this[x] != e ]  == [ this[x] | x <-[], this[x] != e ] == [] 
//implica listaAux == [ this[x] | x <-[o..i), this[x] != e ]
//luego vale I

//2. Vale B & I /cuerpo/Vale I
//estado AntesIf
//vale B & I
//vale  i < |this| &&  this == pre(This) && 0 <= i <= |this| &&  listaAux = [ this[x] | x <- [0..i), this[x] != e]
//implica 0 <= i < |this| &&  listaAux = [pre(this)[x] | x <- [0..i), pre(this)[x] != e]
//notando que 0<= i <= |this| satisface la precondicion de iesimo
if(this.iesimo(i) != e){
	 listaAux.agregar(this.iesimo(i));
}
// Estado DespuesIf
// vale Qc: (this[i] == e && listaAux == listaAux@AntesIf) || (this[i] != e && listaAux == listaAux@AntesIf ++ this[i])
//como solo se modifica(o se podria modificar) listaAux, se puede deducir que lo demas se mantiene, es decir
//implica: 0 <= i < |this| &&  this == pre(This)
//claramente, los miembros de la disyuncion de Qc, son excluyentes, luego como vale Qc es porque uno de los dos miembros vale.

//analizo el caso en que vale que (this[i] == e && listaAux == listaAux@AntesIf)
//como this[i] es igual a e, es falso que this[i] != e, luego como no pasaria el filtro, vale que listaAux = [pre(this)[x] | x <- [0..i], pre(this)[x] != e]
//luego vale 0 <= i < |this| &&  this == pre(This) &&  listaAux = [pre(this)[x] | x <- [0..i], pre(this)[x] != e]

//en el caso en que vale  (this[i] != e && listaAux == listaAux@AntesIf ++ this[i])
//implica listaAux == [pre(this)[x] | x <- [0..i), pre(this)[x] != e] ++ this[i] && this[i] == pre(this)[i] != e
//implica listaAux [pre(this)[x] | x <- [0..i], pre(this)[x] != e]
//implica 0 <= i < |this| &&  this == pre(This) &&  listaAux = [pre(this)[x] | x <- [0..i], pre(this)[x] != e]

//conclusion: en cualquiera de las dos ramas se llega a:
//vale: 0 <= i < |this| &&  this == pre(This) &&  listaAux = [pre(this)[x] | x <- [0..i], pre(this)[x] != e]

i++;

//estado b
//vale i = i@AntesIf + 1
//como no se modifico ninguno de los arreglos,
// vale: 0 <= i@AntesIf < |this| &&  this == pre(This) &&  listaAux = [pre(this)[x] | x <- [0..i@AntesIf], pre(this)[x] != e]
//implica this == pre(this)
//implica 0 <= 1 <= 1 + i@AntesIf <= |this|
//implica 0 <= i <= |this|
//implica listaAux = [pre(this)[x] | x <- [0..i), pre(this)[x] != e] pues [0..i@AntesIf] == [0..i@AntesIf + 1) == [0..i)

//implica I, que era lo que se queria probar