stan/WLP2024
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Add Substitution rule

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-06-15 15:36:51 +02:00
parent 71ffb2c766
commit 0a1644617a
1 changed files with 8 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
aspUnify.tex
View File

@ -225,6 +225,14 @@ Result:
\sigma(\tv{a}) = \type{N} \sigma(\tv{a}) = \type{N}
} }
\and \and
\inferrule[Solution-Sub]{
\tv{a} \lessdot \exptype{C_1}{\ol{T_1}}, \ldots, \tv{a} \lessdot \exptype{C_n}{\ol{T_n}} \\
\forall i: \type{C_m} << \type{C_i} \\
\text{not}\ \tv{a} \doteq \type{N}
}{
\Delta(\type{A}) = \exptype{C_m}{\ol{T_m}} \\ \tv{a} \mapsto \type{A}
}
\and
\inferrule[Solution-Sub]{ \inferrule[Solution-Sub]{
\tv{a} \lessdot \exptype{C_1}{\ol{T_1}}, \ldots, \tv{a} \lessdot \exptype{C_n}{\ol{T_n}} \\ \tv{a} \lessdot \exptype{C_1}{\ol{T_1}}, \ldots, \tv{a} \lessdot \exptype{C_n}{\ol{T_n}} \\
\forall i: \type{C_m} << \type{C_i} \\ \forall i: \type{C_m} << \type{C_i} \\