Notebook[List[Cell[BoxData[FormBox[RowBox[List["t", "\[Element]", RowBox[List[RowBox[List["\[ScriptCapitalT]", "(", "c", ")"]], "\[DoubleLeftRightArrow]", RowBox[List["{", GridBox[List[List[RowBox[List["t", "\[Element]", RowBox[List["dom", "(", "\[Phi]", ")"]]]], RowBox[List[RowBox[List[StyleBox["if", Rule[FontSlant, "Plain"]], "   ", "c"]], "\[Congruent]", "\[Phi]"]]], List[RowBox[List[RowBox[List["(", RowBox[List[StyleBox["\[Exists]", Rule[LineSpacing, List[1., Inherited]]], RowBox[List[RowBox[List[StyleBox["i", Rule[LineSpacing, List[1., Inherited]]], Cell[TextData[StyleBox[":", Rule[LineSpacing, List[1, 0]]]]], "   ", "t"]], "\[Element]", RowBox[List["\[ScriptCapitalT]", "(", SubscriptBox["c", "i"], ")"]]]]]], ")"]], "\[Wedge]", RowBox[List["(", RowBox[List[RowBox[List[Cell[TextData[List[StyleBox["\[ForAll]", Rule[LineSpacing, List[1, 0]]], StyleBox["i", Rule[LineSpacing, List[1, 0]], Rule[FontSlant, "Italic"]]]]], Cell[TextData[StyleBox[":", Rule[LineSpacing, List[1, 0]]]]], "   ", RowBox[List["\[ScriptCapitalE]", "(", RowBox[List[SubscriptBox["c", "i"], ",", "t"]], ")"]]]], "\[NotEqual]", "\[UpTee]"]]]]]], RowBox[List[RowBox[List[StyleBox["if", Rule[FontSlant, "Plain"]], "   ", "c"]], "\[Congruent]", RowBox[List["op", "(", RowBox[List[SubscriptBox["c", "1"], ",", "\[Ellipsis]", "   ", ",", SubscriptBox["c", "n"]]], ")"]]]]], List[RowBox[List["t", "\[Element]", RowBox[List["\[ScriptCapitalT]", "(", SubscriptBox["c", "1"], ")"]]]], RowBox[List[RowBox[List[StyleBox["if", Rule[FontSlant, "Plain"]], "   ", "c"]], "\[Congruent]", RowBox[List[StyleBox["latch", Rule[FontSlant, "Plain"]], "(", RowBox[List[SubscriptBox["c", "0"], ",", SubscriptBox["c", "1"]]], ")"]]]]], List[RowBox[List[RowBox[List["t", "\[Element]", RowBox[List[RowBox[List["\[ScriptCapitalT]", "(", SubscriptBox["c", "0"], ")"]], "\[Wedge]", RowBox[List["\[ScriptCapitalE]", "(", RowBox[List[SubscriptBox["c", "0"], ",", "t"]], ")"]]]]]], "=", StyleBox["true", Rule[FontSlant, "Plain"]]]], RowBox[List[RowBox[List[StyleBox["if", Rule[FontSlant, "Plain"]], "   ", "c"]], "\[Congruent]", RowBox[List[StyleBox["when", Rule[FontSlant, "Plain"]], "(", SubscriptBox["c", "0"], ")"]]]]], List[RowBox[List["t", "\[Element]", RowBox[List[RowBox[List[RowBox[List["\[ScriptCapitalT]", "(", SubscriptBox["c", "1"], ")"]], "\[Wedge]", RowBox[List["\[ScriptCapitalE]", "(", SubscriptBox["c", "0"], ")"]]]], "\[NotEqual]", "\[UpTee]"]]]], RowBox[List[RowBox[List[StyleBox["if", Rule[FontSlant, "Plain"]], "   ", "c"]], "\[Congruent]", RowBox[List[SubscriptBox["c", "0"], "@", SubscriptBox["c", "1"]]]]]]], Rule[ColumnAlignments, List[Left, Left, Center]]]]]]]]], TraditionalForm]], "Input"]]]