Abduction.md

|- typ1 + <typA> = typ2  |- o1 + <oA> = o2  |- p1 + <pA> = p2
—————————————————————————————————————————————————————————————
|- (typ1,o1)::p2 + <(typA,oA)::pA> = (typ2,o2)::p2

|- notOpt + <notOpt> = notOpt

|- notOpt + <opt(p)> = opt(p) 

|- opt(p) + <notOpt> = opt(p)

             p2 > p1
-----------------------------------
|- opt(p1) + <opt(p2-p1)> = opt(p2)

|- empty + <typ> = typ

|- number + <empty> = number

|- string + <empty> = string

|- boolean + <empty> = boolean

|- {G1} + <{GA}> = {G2}  |- styp1 + <stypA> = styp2
———————————————————————————————————————————————————
|- {G1, x:styp1} + <{GA, x:stypA}> = {G2, x:styp2}

|- {G1} + <{GA}> = {G2}  (x not in G1)
—————————————————————————————————————————
|- {G1} + <{GA, x:styp2}> = {G2, x:styp2}

|- {G1} + <{GA}> = {}  |- typ1 + <typA> = typ1  |- o1 + <oA> = notOpt
—————————————————————————————————————————————————————————————————————
|- {G1, x:((typ1,o1)::p1)} + <{GA, x:((typA,oA)::(-p1))}> = {}

|- typ1 + <{G, x:(empty, notOpt)::0> = typ2
———————————————————————————————————————
|- typ1 + <{G}> = typ2

|- typ1 + <{}> = typ2
————————————————————
|- typ1 + <empty> = typ2

|- styp1 + <stypA> = styp2
————————————————————————————————
|- [styp1] + <[stypA]> = [styp2]

|- typ1 + <[(empty, notOpt)::0]> = typ2
———————————————————————————————————
|- typ1 + <empty> = typ2