DISP	j_class_df	J( < f:f:* > ; < s:spec:* > ; < t:jtype:* > )== J( < t > ) J( < t:jtype:* > )== J( < t > )
ABS	j_class	J(t) == @t
THM	j_class_wf	f:Atom . s:Spec. t:Type. J(t)
DISP	j_nil_obj_df	< t:jtype:* > == < t >
ABS	j_nil_obj	t == (t)
THM	j_nil_obj_wf	f:Atom . t:Type. s:Spec. t J(t)
DISP	j_c_update_df	[cor( < x:jobj:* > ):= < c:jcor:* > @ < y:jobj:* > ]== [cor( < x > ):= < c > @ < y > ]
ABS	j_c_update	[cor(x):=c@y] == [cor(x):=c@y]
THM	j_c_update_wf	f:Atom . s:Spec. t,r:Type. x:J(t). c:JCor(t). y:J(r). [cor(x):=c@y] J(r)
DISP	j_r_update_df	[ < x:jobj:* > . < i:jidx:* > := < z:jobj:* > @ < y:jobj:* > ]== [ < x > . < i > := < z > @ < y > ]
ABS	j_r_update	[x.i:=z@y] == [x.i:=z@y]
THM	j_r_update_wf	f:Atom . s:Spec. t,r:Type. x:J(t). i:JIdx(t). z:J(Jfld(t.i)). y:J(r). [x.i:=z@y] J(r)
DISP	j_cor_const_df	JCorConst( < c:jcor:* > ; < t:jtype:* > )== JCorConst( < c > ; < t > )
ABS	j_cor_const	JCorConst(c;t) == [cor(t):=c@t]
THM	j_cor_const_wf	f:Atom . s:Spec. t:Type. c:JCor(t). JCorConst(c;t) J(t)
DISP	j_const_df	JConst( < c:c:* > ; < t:t:* > )== JConst( < c > ; < t > )
ABS	j_const	JConst(c;t) == JCorConst(Jac(c);t)
THM	j_const_wf	f:Atom . s:Spec. t:Type. c:JActCor(t). JConst(c;t) J(t)
DISP	j_cor_oper2_df	j_cor_oper2( < u:var > , < v:var > . < op:op:* > ; < x:x:* > ; < y:y:* > ) == j_cor_oper2( < u > , < v > . < op > ; < x > ; < y > )
ABS	j_cor_oper2	j_cor_oper2(u,v.op[u; v];x;y) == case x of Jc - > Jc | Jac(ax) - > case y of Jc - > Jc | Jac(ay) - > Jac(op[ax; ay])
THM	j_cor_oper2_wf	f:Atom . t:Type. op:JActCor(t) JActCor(t) JActCor(t). x,y:JCor(t). j_cor_oper2(u,v.op[u;v];x;y) JCor(t)
DISP	get_j_cor_df	get_j_cor( < x:x:* > ; < f:f:* > ; < s:s:* > )== get_j_cor( < x > ; < f > ; < s > )
ABS	get_j_cor	get_j_cor(x;f;s) == cor(x)
THM	get_j_cor_wf	f:Atom . s:Spec. t:Type. o:J(t). get_j_cor(o;f;s) JCor(t)
DISP	simple_obj_oper2_df	simple_obj_oper2( < u:var > , < v:var > . < op:op:* > ; < x:x:* > ; < y:y:* > ; < f:f:* > ; < s:s:* > ; < t:t:* > ) == simple_obj_oper2( < u > , < v > . < op > ; < x > ; < y > ; < f > ; < s > ; < t > )
ABS	simple_obj_oper2	simple_obj_oper2(u,v.op[u; v];x;y;f;s;t) == JCorConst(j_cor_oper2(u,v.op[u; v];get_j_cor(x;f;s);get_j_cor(x;f;s) );t)
THM	simple_obj_oper2_wf	f:Atom . s:Spec. t:Type. x,y:J(t). op:JActCor(t) JActCor(t) JActCor(t). simple_obj_oper2(u,v.op[u;v];x;y;f;s;t) J(t)
DISP	get_type_df	get_type( < x:x:* > )== get_type( < x > )
ABS	get_type	get_type(x) == nam(x)
THM	get_type_wf	f:Atom . s:Spec. t:Type. x:J(t). get_type(x) Type
ML	get_type_eval	let get_type_of_j_c_updateC = MacroC `get_type_of_j_c_updateC` (UnfoldsC ``get_type j_c_update`` ANDTHENC AbRedexC ANDTHENC FoldC `get_type`) get_type([cor(x):=t@y]) IdC get_type(y) ;; let get_type_of_j_r_updateC = MacroC `get_type_of_j_r_updateC` (UnfoldsC ``get_type j_r_update`` ANDTHENC AbRedexC ANDTHENC FoldC `get_type`) get_type([x.i:=z@y]) IdC get_type(y) ;; let get_type_of_j_nil_objC = MacroC `get_type_of_j_nil_objC` (UnfoldsC ``get_type j_nil_obj`` ANDTHENC AbRedexC) get_type(t) IdC t ;; let get_type_of_j_constC = MacroC `get_type_of_j_constC` (UnfoldC `j_const` ANDTHENC UnfoldC `j_cor_const` ANDTHENC get_type_of_j_c_updateC ANDTHENC get_type_of_j_nil_objC) get_type(JConst(c;t)) IdC t ;; let get_typeC = get_type_of_j_c_updateC ORELSEC get_type_of_j_r_updateC ORELSEC get_type_of_j_nil_objC ORELSEC get_type_of_j_constC ;; add_AbReduce_conv `get_type` get_typeC;;
THM	get_type_sound	f:Atom . s:Spec. t:Type. x:J(t). get_type(x) = t
THM	get_type_sound_mem	f:Atom . s:Spec. t:Type. x:J(t). x J(get_type(x))
DISP	get_j_ref_df	( < x:jobj:* > . < i:i:* > wrt < f:f:* > ; < s:spec:* > )== ( < x > . < i > ) ( < x:jobj:* > . < i:i:* > )== ( < x > . < i > )
ABS	get_j_ref	(x.i) == get_ref(x;i;JSign(f;s))
THM	get_j_ref_wf	f:Atom . s:Spec. t:Type. x:J(t). i:JIdx(t). (x.i) J(Jfld(t.i))
DISP	eq_j_df	eq_j( < x:x:* > ; < y:y:* > ; < f:f:* > ; < s:s:* > )== eq_j( < x > ; < y > ; < f > ; < s > )
ABS	eq_j	eq_j(x;y;f;s) == (x=y)
THM	eq_j_wf	f:Atom . s:Spec. t,r:Type. x:J(t). y:J(r). eq_j(x;y;f;s)

the other theories