*int:*∧ (::Ord int) ⊢t0:k0->t1:k1 = t2:k2 ∧ t2:k2 = int:ka->int:kb ∧ (::Ord t1)*

It then proves that (roughly) likes this

*int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4:* ∧ int:*= t3:k3 ∧ int:* = t4:k4 ∧*

*k0 = ka =* ∧ t0: = int:*∧ k1 = kb=* ∧ t1:* = int:**

*⊢*

*-----------------------------------------------------------*

*int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4:* ∧ int:*= t3:k3 ∧ int:* = t4:k4*

*∧*

*k0 = ka =* ∧ t0:* = int:*∧ k1= kb = * ∧ t1:* = int:**

*⊢ (::Ord int)*

*----------------------------------------------------------*

*int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4:* ∧ int:*= t3:k3 ∧ t1:k1 = t4:k4*

*∧ k0 = ka =* ∧ t0:* = int:**

*⊢ t1:k1:* = int:kb ∧ (::Ord t1)*

*-----------------------------------------------------------*

*int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4:* ∧ t0:k0= t3:k3 ∧ t1:k1 = t4:k4*

*⊢ t0:k0 = int:ka ∧ t1:k1 = int:kb ∧ (::Ord t1)*

*----------------------------------------------------------*

*int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4:* ∧ t0:k0= t3:k3 ∧ t1:k1 = t4:k4*

*⊢ t0:k0->t1:k1 = int:ka->int:kb ∧ (::Ord t1)*

*---------------------------------------------------------*

*int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4 ∧ t0:k0= t3:k3*

*⊢ t1:k1 = t4:k4 ∧ t0:k0->t4:k4 = int:ka->int:kb ∧ (::Ord t1)*

*-----------------------------------------------------*

*int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4*

*⊢ t0:k0= t3:k3 ∧ t1:k1 = t4:k4 ∧ t3:k3->t4:k4 = int:ka->int:kb ∧ (::Ord t1)*

*----------------------------------------------------*

*int:*∧ (::Ord int) ⊢ t0:k0->t1:k1 = t2:k2 ∧ t2:k2 = int:ka->int:kb ∧ (::Ord t1)*

It doesn't seem to handle intermediaries well, though. Guess I need to check it with the algorithm. (Hmm. Intermediaries should remain on the left-hand side of the equation?)

## No comments:

## Post a Comment