Changes

| style="width:2%;  border-top:1px solid black" |  

| style="width:2%;  border-top:1px solid black" |  

| style="width:14%; border-top:1px solid black" | <math>\operatorname{F1a.}</math>

| style="width:14%; border-top:1px solid black" | <math>\operatorname{F1a.}</math>

| style="width:64%; border-top:1px solid black" | <math>s \quad \Leftrightarrow \quad P ~=~ Q</math>

| style="width:64%; border-top:1px solid black" | <math>s \quad \Leftrightarrow \quad (P ~=~ Q)</math>

| style="width:20%; border-top:1px solid black; border-left:1px solid black; text-align:center" |

| style="width:20%; border-top:1px solid black; border-left:1px solid black; text-align:center" |

<math>\operatorname{F1a~:~R9a}</math>

<math>\operatorname{F1a~:~R9a}</math>

| &nbsp;

| &nbsp;

| <math>\operatorname{F1b.}</math>

| <math>\operatorname{F1b.}</math>

| <math>s \quad \Leftrightarrow \quad \upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright</math>

| <math>s \quad \Leftrightarrow \quad (\upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright)</math>

| style="border-left:1px solid black; text-align:center" |

| style="border-left:1px solid black; text-align:center" |

<math>\operatorname{F1b~:~R9b}</math>

<math>\operatorname{F1b~:~R9b}</math>

| <math>\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright ~\underline{))}^\$ (x)</math>

| <math>\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright ~\underline{))}^\$ (x)</math>

| style="border-left:1px solid black; text-align:center" |

| style="border-left:1px solid black; text-align:center" |

<math>\operatorname{F1g~:~~\_\_?\_\_}</math>

<math>\operatorname{F1h~:~~\_\_?\_\_}</math>

|}

|}

|}

|}