-
:
the goal become %20%5Csubseteq%20sort(0))
,In this case by inversion precedence in goal with respect to rule Prefix we can know, 
can only be 0 and at this time claim holds
-
:
by rewriting the second definition of sort, then the goal become:
%20%5Csubseteq%20(%5C%7B%5Calpha%5C%7D%20-%5C%7B*%5C%7D)%20%5Ccup%20sort(P))
.
by rule Prefix we can know, can only be 
and we can always find exists 
. And )
union something is always larger than itself so claim holds
-
Similar operation to before, the goal become:
%20%5Csubseteq%20sort(P_2)%20%5Ccup%20sort(P_1))
.
by rule Choice1 and Choice2 we can see, we can always find a 
to let precedence hold, and can become either 
or 
. union of set is monotonic, of course larger. Clearly claim holds.
-
The goal become:
%20%5Csubseteq%20sort(P_1)%20%5Ccup%20sort(P_2))
similar inversion, this time we have 3 interesting case
- by rule
Par1 : we can have 
, which means by 4th rule of sort we can have %20%3D%20sort(P_1')%20%5Ccup%20sort%20(P_2))
. By inductive hypothesis we can know if 
is the derivation of then we will have %20%5Csubseteq%20sort(P_1))
so clearly final goal is true
-
Par2 and Par3 are similar. the only difference in Par3 is both and 
cause a shrink the size of set.
-
The goal become:
%20%5Csubseteq%20sort(P)%20-%20X)
By rule Restrict we can know can become 
, according to the last rule of sort we can rewrite )
in the goal as %20-%20X)
. And according to inductive hypothesis, we can know %20%5Csubseteq%20sort(P))
. So clearly claim hold.
All inductive cases is proved.
