include('Axioms/sptree_2.ax').
tff(tp_c_2EEncodeVar_2Efixed__width,type,(c_2EEncodeVar_2Efixed__width:del > $i)).
tff(mem_c_2EEncodeVar_2Efixed__width,axiom,( ! [A_27a:del] : mem(c_2EEncodeVar_2Efixed__width(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(A_27a,ty_2Elist_2Elist(bool)),arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool)))))),bool))))).
tff(tp_c_2EEncodeVar_2Eof__length,type,(c_2EEncodeVar_2Eof__length:del > $i)).
tff(mem_c_2EEncodeVar_2Eof__length,axiom,( ! [A_27a:del] : mem(c_2EEncodeVar_2Eof__length(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(A_27a),bool))))).
tff(ax_thm_2EEncodeVar_2Efixed__width__def,axiom,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1c:$i] : (mem(V1c,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(A_27a,ty_2Elist_2Elist(bool)),arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))))))) => (p(ap(ap(c_2EEncodeVar_2Efixed__width(A_27a),inj__ty_2Enum_2Enum(V0n)),V1c)) <=> ( ! [V2x:$i] : (mem(V2x,A_27a) => (p(ap(ap(c_2ECoder_2Edomain(A_27a),V1c),V2x)) => (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(bool),ap(ap(c_2ECoder_2Eencoder(A_27a),V1c),V2x))) = V0n)))))))))).
tff(ax_thm_2EEncodeVar_2Eof__length__def,axiom,( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(ty_2Elist_2Elist(A_27a)),V0l),ap(c_2EEncodeVar_2Eof__length(A_27a),inj__ty_2Enum_2Enum(V1n)))) <=> (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l)) = V1n))))))).
tff(conj_thm_2EEncodeVar_2Efixed__width__univ,lemma,(( ! [A_27a:del]: ( ! [V0phi:$i] : (mem(V0phi,arr(A_27a,bool)) => ( ! [V1c:$i] : (mem(V1c,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(A_27a,ty_2Elist_2Elist(bool)),arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))))))) => ( ! [V2n:tp__ty_2Enum_2Enum] : ((p(ap(c_2ECoder_2Ewf__coder(A_27a),V1c)) & p(ap(ap(c_2EEncodeVar_2Efixed__width(A_27a),inj__ty_2Enum_2Enum(V2n)),V1c))) => (( ! [V3x:$i] : (mem(V3x,A_27a) => (p(ap(ap(c_2ECoder_2Edomain(A_27a),V1c),V3x)) => p(ap(V0phi,V3x))))) <=> p(ap(ap(c_2Ebool_2ERES__FORALL(ty_2Elist_2Elist(bool)),ap(c_2EEncodeVar_2Eof__length(bool),inj__ty_2Enum_2Enum(V2n))),f2440(A_27a,V1c,V0phi))))))))))))).
tff(conj_thm_2EEncodeVar_2Eof__length__univ__suc,lemma,(( ! [A_27a:del]: ( ! [V0phi:$i] : (mem(V0phi,arr(ty_2Elist_2Elist(A_27a),bool)) => ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2ERES__FORALL(ty_2Elist_2Elist(A_27a)),ap(c_2EEncodeVar_2Eof__length(A_27a),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n)))),f2441(A_27a,V0phi))) <=> ( ! [V3x:$i] : (mem(V3x,A_27a) => p(ap(ap(c_2Ebool_2ERES__FORALL(ty_2Elist_2Elist(A_27a)),ap(c_2EEncodeVar_2Eof__length(A_27a),inj__ty_2Enum_2Enum(V1n))),f2442(A_27a,V3x,V0phi)))))))))))).
tff(conj_thm_2EEncodeVar_2Eof__length__univ__zero,lemma,(( ! [A_27a:del]: ( ! [V0phi:$i] : (mem(V0phi,arr(ty_2Elist_2Elist(A_27a),bool)) => (p(ap(ap(c_2Ebool_2ERES__FORALL(ty_2Elist_2Elist(A_27a)),ap(c_2EEncodeVar_2Eof__length(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),f2443(A_27a,V0phi))) <=> p(ap(V0phi,c_2Elist_2ENIL(A_27a))))))))).
tff(conj_thm_2EEncodeVar_2Efixed__width__exists,lemma,(( ! [A_27a:del]: ( ! [V0phi:$i] : (mem(V0phi,arr(A_27a,bool)) => ( ! [V1c:$i] : (mem(V1c,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(A_27a,ty_2Elist_2Elist(bool)),arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))))))) => ( ! [V2n:tp__ty_2Enum_2Enum] : ((p(ap(c_2ECoder_2Ewf__coder(A_27a),V1c)) & p(ap(ap(c_2EEncodeVar_2Efixed__width(A_27a),inj__ty_2Enum_2Enum(V2n)),V1c))) => ((? [V3x:$i] : (mem(V3x,A_27a) & (p(ap(ap(c_2ECoder_2Edomain(A_27a),V1c),V3x)) & p(ap(V0phi,V3x))))) <=> p(ap(ap(c_2Ebool_2ERES__EXISTS(ty_2Elist_2Elist(bool)),ap(c_2EEncodeVar_2Eof__length(bool),inj__ty_2Enum_2Enum(V2n))),f2440(A_27a,V1c,V0phi))))))))))))).
tff(conj_thm_2EEncodeVar_2Eof__length__exists__suc,lemma,(( ! [A_27a:del]: ( ! [V0phi:$i] : (mem(V0phi,arr(ty_2Elist_2Elist(A_27a),bool)) => ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2ERES__EXISTS(ty_2Elist_2Elist(A_27a)),ap(c_2EEncodeVar_2Eof__length(A_27a),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n)))),f2441(A_27a,V0phi))) <=> (? [V3x:$i] : (mem(V3x,A_27a) & p(ap(ap(c_2Ebool_2ERES__EXISTS(ty_2Elist_2Elist(A_27a)),ap(c_2EEncodeVar_2Eof__length(A_27a),inj__ty_2Enum_2Enum(V1n))),f2442(A_27a,V3x,V0phi)))))))))))).
tff(conj_thm_2EEncodeVar_2Eof__length__exists__zero,lemma,(( ! [A_27a:del]: ( ! [V0phi:$i] : (mem(V0phi,arr(ty_2Elist_2Elist(A_27a),bool)) => (p(ap(ap(c_2Ebool_2ERES__EXISTS(ty_2Elist_2Elist(A_27a)),ap(c_2EEncodeVar_2Eof__length(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),f2443(A_27a,V0phi))) <=> p(ap(V0phi,c_2Elist_2ENIL(A_27a))))))))).
tff(conj_thm_2EEncodeVar_2Efixed__width__unit,conjecture,(( ! [V0p:$i] : (mem(V0p,arr(ty_2Eone_2Eone,bool)) => p(ap(ap(c_2EEncodeVar_2Efixed__width(ty_2Eone_2Eone),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2ECoder_2Eunit__coder,V0p))))))).