LiFtEr: Change 'All_Sub_Trm_Occ' and 'Some_Sub_Trm_Occ'

[yutakang]

Probably either All_Sub_Trm_Occ or Some_Sub_Trm_Occ does not have to take subtrm as an argument. Instead, it would be better if we

• implement All_Sub_Trm_Occ as All_Sub_Trm_Occ of (subtrm_occ * assrt),
• implement Some_Sub_Trm_Occ as Sub_Trm_Occ_Is_Of_Sub_Trm of (subtrm_occ * assrt), and
• introduce Sub_Trm_Occ_Is_Of_Sub_Trm of (subtrm_occ * subtrm).

... because sometime we want to specify an occurrence of a term without specifying a term (e.g. Is_In_Prems).

[yutakang]

• Some_Sub_Trm_Occ_Of_Sub_Trm (subtrm_occ, subtrm, assrt) =
• Some_Sub_Trm_Occ (subtrm_occ,
  • And -(Sub_Trm_Occ_Is_Of_Sub_Trm (subtrm_occ, subtrm), -assrt)

[yutakang]

I also have to change All_Ind_Occ, All_Arb_Occ, Some_Ind_Occ, and Some_Arb_Occ.

[yutakang]

To implement new versions of

• All_Ind_Occ,
• All_Arb_Occ,
• Some_Ind_Occ, and
• Some_Arb_Occ

without introducing fresh variables, I need to re-define

• All_Ind,
• All_Arb,
• Some_Ind, and
• Some_Arb.

Basically, All_Ind, All_Arb, Some_Ind, and Some_Arb should be syntactic sugars for All_Ind_Occ, All_Arb_Occ, Some_Ind_Occ, and Some_Arb_Occ, respectively. Not the other way around.

[yutakang]

No, either way, I have to introduce fresh variables if I consider them as syntactic sugars.

[yutakang]

We can simply give up having

• All_Ind_Occ,
• All_Arb_Occ,
• Some_Ind_Occ, and
• Some_Arb_Occ all together.

We can write it manually as

• All_Ind (subtrm,
  • All_Sub_Trm_Occ_Of_Sub_Trm (subtrm_occ , subtrm
  • assrt))

[yutakang]

c58404c149322de2111a1965e31598392ff6db07