SeLFiE: avoid expensive syntax sugars.

[yutakang]

For Something_Or_Below_Somethings, we probably do not need to introduce a new variable. Just introduce a new atomic assertion Is_Below.

• [x] Is_A_Meta_Premise: way too expensive.
• [x] Is_A_Meta_Premise_Or_Below: way too expensive.
• [x] Is_A_Meta_Conclusion: way too expensive.
• [x] Is_A_Meta_Conclusion_Or_Below: way too expensive.
• [X] Unode_Has_As_Subprint (Probably the existential quantifier is even not necessary. -> It is necessary as long as we treat it as syntactic sugar.) 12e1ed73a366452c367fccc83fb275cee8bba0dc
• [x] Is_Parent_Of: unnecessarily expensive.
• [X] Are_In_Same_Location
• [x] Is_Nth_Child_Or_Below_Nth_Child_Of: unnecessarily expensive.
• [x] Is_Below_N_Plus_One_th_Child_Ofef795c2aaef6d722c10e62f96dfc99f5038a805d
• [x] Is_An_Arg_Of: unnecessarily expensive.
• [x] Is_An_Arg_Or_Below_Arg_Of: probably the existential quantifier is even not necessary.
• [x] Is_Nth_Arg_Of.
• [x] Is_Nth_Arg_Or_Below_Nth_Arg_Of: probably the existential quantifier is even not necessary.
• [ ] Is_At_Deepest_In_A_Location
• ~[ ] Some_Of -> Use Print_To_Paths~
• ~[ ] All_Of -> Use Print_To_Paths~

Probably the followings are difficult to improve further

• [ ] Is_Case_Distinct_Of_Trm_With_A_Case
• [ ] Is_Let_X_Be_Y_In_X

[yutakang]

Some_Of and All_Of pose a tricky problem. I extended qtyp in Util.ML and domains in Quantifier_Domain.ML with QPrint_To_Paths of string and print_to_paths: Eval_Parameter.non_path_literal -> Eval_Parameter.literals to compute them efficiently.

This means, I have to bridge the gap between string and Eval_Parameter.literal In Eval_Unary by evaluating the value of Eval_Parameter.literal.

So, I think I need one more definition of qtyp that has QPrint_To_Paths2 of Eval_Parameter.non_path_literal.

[yutakang]

NO... this "optimisation" caused code-clutter and actually exacerbated the performance.

I am not going to keep Some_Of and All_Of as syntactic sugars.