% Import "rels".
Kind atm, form type.
Type atom atm -> form.
Type tens, par form -> form -> form.
Type one, bot form.
Define $form : form -> prop by
; $form (atom A)
; $form (tens F G) := $form F /\ $form G
; $form one
; $form (par F G) := $form F /\ $form G
; $form bot.
Define $list : list form -> prop by
; $list nil
; $list (F :: L) := $form F /\ $list L.
Define adj : list form -> form -> list form -> prop by
; adj L X (X :: L) := $form X /\ $list L
; adj (Y :: L) X (Y :: K) := $form Y /\ adj L X K.
Suspend adj L _ _ := L.
Theorem $adj : forall K E L, adj K E L -> $list K /\ $form E /\ $list L.
induction on 1. intros. case H1.
search.
apply IH to *H3. search.
Define perm : list form -> list form -> prop by
; perm nil nil
; perm L1 L2 := exists E K1 K2, adj K1 E L1 /\ adj K2 E L2 /\ perm K1 K2.
Suspend perm J _ := J.
Theorem $perm : forall K L, perm K L -> $list K /\ $list L.
induction on 1. intros. case H1.
search.
apply $adj to *H2. apply $adj to *H3. apply IH to *H4. search.
Theorem perm_refl : forall L, $list L -> perm L L.
induction on 1. intros. case H1.
search.
apply IH to *H3. apply $perm to H4. search.
Theorem perm_sym : forall K L, perm K L -> perm L K.
induction on 1. intros. case H1.
search.
apply IH to H4. search.
Theorem adj_swap : forall E F J K L, adj J E K -> adj K F L ->
exists U, adj J F U /\ adj U E L.
induction on 2. intros. case H2.
case H1. search.
apply $adj to H6. search.
case H1.
apply $adj to H4. search.
apply IH to H6 H4. search.
Theorem perm_cons_1 : forall E J L, perm (E :: J) L ->
exists K, adj K E L /\ perm J K.
induction on 1. intros. case H1.
case H2. search.
apply IH to *H4. apply adj_swap to *H7 *H3. search.
Theorem perm_cons_2 : forall E L K, perm L (E :: K) ->
exists J, adj J E L /\ perm J K.
induction on 1. intros. case H1.
case H3. search.
apply IH to *H4. apply adj_swap to *H7 *H2. search.
Theorem perm_trans_lem : forall J K L, $list K ->
perm J K -> perm K L -> perm J L.
induction on 1. intros. case H1.
compute H2 H3. search. case H6.
apply perm_cons_2 to *H2. apply perm_cons_1 to *H3.
apply IH to H5 H7 H9. search.
Theorem perm_trans : forall J K L, perm J K -> perm K L -> perm J L.
intros. apply $perm to H1. backchain perm_trans_lem with K = K.
