Selector_TCC2.4 :
[-1] (1 <= p_Data_Type_Conversion)
|-------
[1] p_Data_Type_Conversion - 1 >= 0
Rule? (both-sides "+" "1" 1)
Applying + 1 to both sides of an inequality/equality conjunction,
this yields 3 subgoals:
Selector_TCC2.4.1 :
[-1] (1 <= p_Data_Type_Conversion)
|-------
{1} p_Data_Type_Conversion - 1 + 1 >= 0 + 1
Rule? (grind)
Trying repeated skolemization, instantiation, and if-lifting,
This completes the proof of Selector_TCC2.4.1.
Selector_TCC2.4.2 :
[-1] (1 <= p_Data_Type_Conversion)
|-------
{1} p_Data_Type_Conversion - 1 >= 0 =
p_Data_Type_Conversion - 1 + 1 >= 0 + 1
[2] p_Data_Type_Conversion - 1 >= 0
Rule? (assert)
Simplifying, rewriting, and recording with decision procedures,
this simplifies to:
Selector_TCC2.4.2 :
[-1] (1 <= p_Data_Type_Conversion)
|-------
{1} FALSE = TRUE
[2] p_Data_Type_Conversion - 1 >= 0
At this point, since {1} is clearly false, I’m back to where I started (notwithstanding an additional TCC to prove that real_pred(p_Data_Type_Conversion - 1), which can be proved with (lemma "reals.closed_minus" ("x" "p_Data_Type_Conversion" "y" "1"))).