write-up.txt

Notation: |> is matching. <= is precision.

Example 1:
λx : * . x (succ (x True)) 

Mappings: 
0. [λx : * . x (succ (x True))] 
1. x
2. [x (succ (x True))]
3. [x]
4. [(succ (x True))]
5. [succ] 
6. [(x True)]
7. [x]
8. [True]
9. <True>
10. <(x True)>
11. <(succ (x True))>

STEP 1 gen:
 0 = 1 -> 2
 * <= 1
 3 |> 11 -> 2
 11 ~ 4
 3 = 1
 5 |> 10 -> 4
 10 ~ 6
 5 = int -> int
 7 |> 9 -> 6
 9 ~ 8
 7 = 1
 8 = bool

STEP 2 SimPrec:
0 = 1 -> 2
3 |> 11 -> 2
11 ~ 4
3 = 1
5 |> 10 -> 4
10 ~ 6
5 = int -> int
7 |> 9 -> 6
9 ~ 8
7 = 1
8 = bool


STEP 3 simMatch:
s1: (we have 7 more possibilities which we emit for now)
 0 = 1 -> 2
 3 = 11 -> 2
 11 ~ 4
 3 = 1
 5 = 10 -> 4
 10 ~ 6
 5 = int -> int
 7 = 9 -> 6
 9 ~ 8
 7 = 1
 8 = bool


STEP 4: Unify
Unifies to:
(0,(11 -> 2) -> 2)
(1,11 -> 2)
(3,11 -> 2)
(4,int)
(5,int -> int)
(6,2)
(7,11 -> 2)
(8,bool)
(9,11)
(10,int)


So from our mapping, we can have:
 [λx : * . x (succ (x True))] : (<(succ (x True))> -> [x (succ (x True))])
                                                  -> [x (succ (x True))]
                            x : <(succ (x True))> -> [x (succ (x True))]
                          [x] : <(succ (x True))> -> [x (succ (x True))]
            [(succ (x True))] : int
                       [succ] : int -> int
                   [(x True)] : [x (succ (x True))]
                          [x] : <(succ (x True))> -> [x (succ (x True))]
                       [True] : bool
                       <True> :  <(succ (x True))>
                   <(x True)> : int

-----

RETURN TO SIMPREC

0 = 1 -> 2
3 = *
11 = *
2 = *
11 ~ 4
3 = 1
5 = 10 -> 4
10 ~ 6
5 = int -> int
7 = *
9 = *
6 = *
9 ~ 8
7 = 1
8 = bool


UNIFY AGAIN

(0,* -> *)
(1,*)
(2,*)
(3,*)
(4,int)
(5,int -> int)
(6,*)
(7,*)
(8,bool)
(9,*)
(10,int)
(11,*)


SIMMATCH (s= 2,3)

0 = 1 -> 2
3 = *
11 = *
2 = *
11 ~ 4
3 = 1
5 = 10 -> 4
10 ~ 6
5 = int -> int
7 = 9 -> 6
9 ~ 8
7 = 1
8 = bool

UNSAT.