∧，∨に関わる inference rules

∧の導入（INTRO）と消去（ELIM）の推論には，以下の４通りがあります．

　|-　|-　∧|-　　　　 　|-∧
−−−−−−−−　　　−−−−−
　　　 |- 　　　　　　　|-　|-
LCE 　　　　  　　　　CONJUNCT1,CONJUNCT2,CONJ_PAIR,CONJUNCTS

　|-　または　|-　　　　|-　|-
−−−−−−−−−　　−−−−−
　　　∧|-　　　　　　　 |-∧
ADD_ASSUM,LCI　　 　　CONJ

# let LCE th1 th2 th12 = PROVE_HYP (CONJ th1 th2) th12 ;;
val ( LCE ) : thm -> thm -> thm -> thm = <fun>
...
val thx : thm = x + y = 0 |- x = 0
val thy : thm = x + y = 0 |- y = 0
val thxy : thm = x = 0 /\ y = 0 |- x * y = 0
# LCE thx thy thxy;;
val it : thm = x + y = 0 |- x * y = 0
# LCE thy thx thxy;;
val it : thm = x = 0 /\ y = 0 |- x * y = 0

∨の導入（INTRO）と消去（ELIM）の推論には，以下の４通りがあります．

　 ∨|- 　　　　　　　　　　　　　|-∨　|-　|-
−−−−−　　　　　　　　　　　−−−−−−−−
　|-　|- 　　　　　　　　　　　　　　　|-
SIMPLE_DISJ_PAIR　　　　　　　　DISJ_CASES
in derive_nonschematic_inductive_relations

　|-　|-　　　　　　　　　　　　　|-　または　|-
−−−−−　　　　　　　　　　　−−−−−−−−−
　 ∨|- 　　　　　　　　　　　　　　　　|-∨
DISJ_CASES,SIMPLE_DISJ_CASES　　DISJ1,DISJ2

古典論理では，∀，∃の推論と同じく，次の双対性があります．
・対角の推論どうしはPROVE_HYPで書き換えられます．
・ドモルガン則により∧の左右が，それぞれ∨の右左と書き換えられます．