public BoolExpr add_sorted_theorem(Context ctx, HashMap<String, Expr> symbolTable) throws Z3Exception{
		// a, begin, end
		
		Expr a = this.a_inputs.get(0).to_smt(ctx, symbolTable );
		Expr a_begin = this.a_inputs.get(1).to_smt(ctx, symbolTable );
		Expr a_end = this.a_inputs.get(2).to_smt(ctx, symbolTable );
		
		
        //g.Assert(ctx.MkLt((ArithExpr) a_begin, (ArithExpr) a_end));
		String array_name="";
		if(this.a_inputs.get(0).leaf!=null && this.a_inputs.get(0).leaf.type.equals("string") && symbolTable.containsKey(((a_string)this.a_inputs.get(0).leaf).s))
			array_name = ((a_string)this.a_inputs.get(0).leaf).s;
		else if (this.a_inputs.get(0).leaf!=null && this.a_inputs.get(0).leaf.type.equals("a_expression") &&
				((a_expressionT)this.a_inputs.get(0).leaf).e.leaf!=null && ((a_expressionT)this.a_inputs.get(0).leaf).e.leaf.type.equals("string")
				&& symbolTable.containsKey(((a_string)((a_expressionT)this.a_inputs.get(0).leaf).e.leaf).s))
			array_name = ((a_string)((a_expressionT)this.a_inputs.get(0).leaf).e.leaf).s;
		else
			System.out.println("array not defined!");
		
		Expr i = ctx.MkConst(array_name+"_i", ctx.IntSort());
        Expr j = ctx.MkConst(array_name+"_j", ctx.IntSort());
        Expr alength = ctx.MkConst(array_name + "_lastIndex", ctx.IntSort());
        
		
		//BoolExpr instance_bound = ctx.MkAnd(new BoolExpr[]{ctx.MkLe(ctx.MkInt(0), (ArithExpr)a_begin), ctx.MkLe((ArithExpr)a_begin, (ArithExpr)alength), 
				 						//ctx.MkLe(ctx.MkInt(0), (ArithExpr)a_end), ctx.MkLe((ArithExpr)a_end, (ArithExpr)alength), ctx.MkLe((ArithExpr)a_begin, (ArithExpr)a_end)});
		
        BoolExpr instance_bound = ctx.MkLe((ArithExpr)a_begin, (ArithExpr)a_end);
        
        BoolExpr sorted_expr1 = ctx.MkAnd(new BoolExpr[]{ctx.MkLe((ArithExpr) a_begin, (ArithExpr) i), ctx.MkLe((ArithExpr) i, (ArithExpr) a_end),
        												  ctx.MkLe((ArithExpr) a_begin, (ArithExpr) j), ctx.MkLe((ArithExpr) j, (ArithExpr) a_end),
        												  ctx.MkLe((ArithExpr)i, (ArithExpr)j)});
        BoolExpr sorted_expr = ctx.MkImplies(sorted_expr1, ctx.MkLe((ArithExpr)ctx.MkSelect((ArrayExpr)a, i), (ArithExpr)ctx.MkSelect((ArrayExpr)a, j)));
       // BoolExpr sorted_expr = ctx.MkAnd(new BoolExpr[]{sorted_expr1, ctx.MkLe((ArithExpr)ctx.MkSelect((ArrayExpr)a, i), (ArithExpr)ctx.MkSelect((ArrayExpr)a, j))});
        
        BoolExpr  sorted= ctx.MkForall(new Expr[]{i, j}, /* names of quantified variables */
                sorted_expr, 1, null, null, null, null);
        
        
        //g.Assert(sorted);
        //return ctx.MkAnd(new BoolExpr[]{instance_bound, sorted});
        return ctx.MkImplies(instance_bound, sorted);
        //return sorted;
        
	}