for doing multiplicative binary introduction rules:
wkI_der - weakening based on iila, iila, not mra
del1/2_I, like del1/2_atoms, good for using wkI_der to get premises
of logical ands/ora_rep rules
Now, how to do binary rules ands/ora_rep?
Define lseqrepm, relation between premises and conclusion,
preserved by manipulation by display postulates
Look at [mlogA_ldip, mlogS_ldip]
these are multi-premise analogues of [logA_ldip, logS_ldip]
need to prove that any rearrangement of I and non-I structures in ands_rep,
on either side, also with shifting the logical formulae, is derivable,
analogous to [strrep_mderA, strrep_mderS]
(easier, look at [msdA1, msdA2, msdS1, msdS2] )
First part of this is that, using ands_rep,
X |- A Y |- B
----------------
Z |- A && B
where (Z, [X, Y]) : lstrrepnI (this is ands_mix - DONE)
Then ands_mix_gen DONE
Then SF_some1sub needs to be adapted to lseqrepm,
showing that display postulates in
the conclusion can be used on the premises
Have got equivalents of mseqExSub1 (repm_seq_sub) and
mextSubs (mrextSubs), now repm_rule1sub and repm_some1sub in IrepI.ML
Then [lseqrep_interpA, lseqrep_interpS]
which say that if premises of logical rule, after manipulated by dps,
ie satisfying the lseqrep relation, have interpolants,
then so does the conclusion
Need to adapt these to where manipulated premises and conclusion satisfy the
lseqrepm relation
DONE: [lseqrepm_interp_orF, lseqrepm_interp_andT]
PROBLEM: definition of interpolant is wrt lrules (ie containing the logical
rules - proving conclusion from premises) using derivableR - ie assuming rules
closed under rulefs - whereas our rules ands_rep are not so closed;
NEED to redefine interp to not involve rulefs (DONE, interpn)
therefore will need to redefine edi, ldi
Then [mlogA_ldi, mlogS_ldi] - getting from this to ldi property - using
SF_some1sub.
TRY doing this by (1) anything satisfying lseqrepm satisfies ldin
so DONE [lseqrepm_ldi_orF, lseqrepm_ldi_andT]
and use [ands_rep_cond, ora_rep_cond]
NEXT, showing ands, ora derivable from ands_rep, ora_rep - so as to
get ldi property for ands, ora.
DONE - [ora_from_rep, ands_from_rep]
Then ldi_lil_adds - showing all logical rules have ldi property.
Require to show ands, ora have ldin property.
DON"T quite get this - need to use cldin_ex_interp
Then show that ands_rep, ora_rep are derivable from the multiplicative
ands and ora rules
ie need a converse to [ora_from_rep, ands_from_rep]
DONE - [rep_from_ora, rep_from_ands]
ldi_add_equiv - equivalence of ldi_add and rlscf_nw