THM	example_1	f:Atom . s:Spec. {True} ( " x " :int) := (27) {en " x " int = JConst(27;int)}
THM	example_2	f:Atom . s:Spec. o:J(int). {en " y " int = o} ( " x " :int) := (27) {en " y " int = o}
THM	example_3	f:Atom . s:Spec. {True} ( " y " :int) := (27); ( " x " :int) := (27) {en " x " int = en " y " int}
THM	example_4	f:Atom . s:Spec. {True} ( " y " :int) := ( " x " :int); ( " z " :int) := ( " y " :int) {en " x " int = en " z " int}

the other theories