include('Axioms/indexedLists_2.ax').
tff(tp_c_2ETemporal__Logic_2EALWAYS,type,(c_2ETemporal__Logic_2EALWAYS:$i)).
tff(mem_c_2ETemporal__Logic_2EALWAYS,axiom,mem(c_2ETemporal__Logic_2EALWAYS,arr(arr(ty_2Enum_2Enum,bool),arr(ty_2Enum_2Enum,bool)))).
tff(tp_c_2ETemporal__Logic_2EBEFORE,type,(c_2ETemporal__Logic_2EBEFORE:$i)).
tff(mem_c_2ETemporal__Logic_2EBEFORE,axiom,mem(c_2ETemporal__Logic_2EBEFORE,arr(arr(ty_2Enum_2Enum,bool),arr(arr(ty_2Enum_2Enum,bool),arr(ty_2Enum_2Enum,bool))))).
tff(tp_c_2ETemporal__Logic_2EEVENTUAL,type,(c_2ETemporal__Logic_2EEVENTUAL:$i)).
tff(mem_c_2ETemporal__Logic_2EEVENTUAL,axiom,mem(c_2ETemporal__Logic_2EEVENTUAL,arr(arr(ty_2Enum_2Enum,bool),arr(ty_2Enum_2Enum,bool)))).
tff(tp_c_2ETemporal__Logic_2ENEXT,type,(c_2ETemporal__Logic_2ENEXT:$i)).
tff(mem_c_2ETemporal__Logic_2ENEXT,axiom,mem(c_2ETemporal__Logic_2ENEXT,arr(arr(ty_2Enum_2Enum,bool),arr(ty_2Enum_2Enum,bool)))).
tff(tp_c_2ETemporal__Logic_2ESBEFORE,type,(c_2ETemporal__Logic_2ESBEFORE:$i)).
tff(mem_c_2ETemporal__Logic_2ESBEFORE,axiom,mem(c_2ETemporal__Logic_2ESBEFORE,arr(arr(ty_2Enum_2Enum,bool),arr(arr(ty_2Enum_2Enum,bool),arr(ty_2Enum_2Enum,bool))))).
tff(tp_c_2ETemporal__Logic_2ESUNTIL,type,(c_2ETemporal__Logic_2ESUNTIL:$i)).
tff(mem_c_2ETemporal__Logic_2ESUNTIL,axiom,mem(c_2ETemporal__Logic_2ESUNTIL,arr(arr(ty_2Enum_2Enum,bool),arr(arr(ty_2Enum_2Enum,bool),arr(ty_2Enum_2Enum,bool))))).
tff(tp_c_2ETemporal__Logic_2ESWHEN,type,(c_2ETemporal__Logic_2ESWHEN:$i)).
tff(mem_c_2ETemporal__Logic_2ESWHEN,axiom,mem(c_2ETemporal__Logic_2ESWHEN,arr(arr(ty_2Enum_2Enum,bool),arr(arr(ty_2Enum_2Enum,bool),arr(ty_2Enum_2Enum,bool))))).
tff(tp_c_2ETemporal__Logic_2EUNTIL,type,(c_2ETemporal__Logic_2EUNTIL:$i)).
tff(mem_c_2ETemporal__Logic_2EUNTIL,axiom,mem(c_2ETemporal__Logic_2EUNTIL,arr(arr(ty_2Enum_2Enum,bool),arr(arr(ty_2Enum_2Enum,bool),arr(ty_2Enum_2Enum,bool))))).
tff(tp_c_2ETemporal__Logic_2EUPTO,type,(c_2ETemporal__Logic_2EUPTO:$i)).
tff(mem_c_2ETemporal__Logic_2EUPTO,axiom,mem(c_2ETemporal__Logic_2EUPTO,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))),bool))).
tff(tp_c_2ETemporal__Logic_2EWATCH,type,(c_2ETemporal__Logic_2EWATCH:$i)).
tff(mem_c_2ETemporal__Logic_2EWATCH,axiom,mem(c_2ETemporal__Logic_2EWATCH,arr(arr(ty_2Enum_2Enum,bool),arr(arr(ty_2Enum_2Enum,bool),arr(ty_2Enum_2Enum,bool))))).
tff(tp_c_2ETemporal__Logic_2EWHEN,type,(c_2ETemporal__Logic_2EWHEN:$i)).
tff(mem_c_2ETemporal__Logic_2EWHEN,axiom,mem(c_2ETemporal__Logic_2EWHEN,arr(arr(ty_2Enum_2Enum,bool),arr(arr(ty_2Enum_2Enum,bool),arr(ty_2Enum_2Enum,bool))))).
tff(ax_thm_2ETemporal__Logic_2ENEXT,axiom,( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2ENEXT,V0P) = f878(V0P))))).
tff(ax_thm_2ETemporal__Logic_2EALWAYS,axiom,( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2ETemporal__Logic_2EALWAYS,V0P),inj__ty_2Enum_2Enum(V1t0))) <=> ( ! [V2t:tp__ty_2Enum_2Enum] : p(ap(V0P,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2t)),inj__ty_2Enum_2Enum(V1t0)))))))))).
tff(ax_thm_2ETemporal__Logic_2EEVENTUAL,axiom,( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2ETemporal__Logic_2EEVENTUAL,V0P),inj__ty_2Enum_2Enum(V1t0))) <=> (? [V2t:tp__ty_2Enum_2Enum] : p(ap(V0P,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2t)),inj__ty_2Enum_2Enum(V1t0)))))))))).
tff(ax_thm_2ETemporal__Logic_2EWATCH,axiom,( ! [V0q:$i] : (mem(V0q,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EWATCH,V0q),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> ( ! [V3t:tp__ty_2Enum_2Enum] : ((p(ap(V0q,inj__ty_2Enum_2Enum(V2t0))) <=> $false) & (p(ap(V0q,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V3t)),inj__ty_2Enum_2Enum(V2t0))))) <=> (p(ap(V0q,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V3t)),inj__ty_2Enum_2Enum(V2t0)))) | p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V3t)),inj__ty_2Enum_2Enum(V2t0))))))))))))))).
tff(ax_thm_2ETemporal__Logic_2EUPTO,axiom,( ! [V0t0:tp__ty_2Enum_2Enum] : ( ! [V1t1:tp__ty_2Enum_2Enum] : ( ! [V2a:$i] : (mem(V2a,arr(ty_2Enum_2Enum,bool)) => (p(ap(c_2ETemporal__Logic_2EUPTO,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))),inj__ty_2Enum_2Enum(V0t0)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)),inj__ty_2Enum_2Enum(V1t1)),V2a)))) <=> ( ! [V3t2:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0t0)),inj__ty_2Enum_2Enum(V3t2))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3t2)),inj__ty_2Enum_2Enum(V1t1)))) => p(ap(V2a,inj__ty_2Enum_2Enum(V3t2))))))))))).
tff(ax_thm_2ETemporal__Logic_2EWHEN,axiom,( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EWHEN,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> (? [V3q:$i] : (mem(V3q,arr(ty_2Enum_2Enum,bool)) & (p(ap(ap(ap(c_2ETemporal__Logic_2EWATCH,V3q),V1b),inj__ty_2Enum_2Enum(V2t0))) & ( ! [V4t:tp__ty_2Enum_2Enum] : (p(ap(V3q,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))) | (p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))) => p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))))))))))))))).
tff(ax_thm_2ETemporal__Logic_2EUNTIL,axiom,( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EUNTIL,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> (? [V3q:$i] : (mem(V3q,arr(ty_2Enum_2Enum,bool)) & (p(ap(ap(ap(c_2ETemporal__Logic_2EWATCH,V3q),V1b),inj__ty_2Enum_2Enum(V2t0))) & ( ! [V4t:tp__ty_2Enum_2Enum] : (p(ap(V3q,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))) | (p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))) | p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))))))))))))))).
tff(ax_thm_2ETemporal__Logic_2EBEFORE,axiom,( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EBEFORE,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> (? [V3q:$i] : (mem(V3q,arr(ty_2Enum_2Enum,bool)) & (p(ap(ap(ap(c_2ETemporal__Logic_2EWATCH,V3q),V1b),inj__ty_2Enum_2Enum(V2t0))) & ((? [V4t:tp__ty_2Enum_2Enum] : ((~~ p(ap(V3q,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))) & ((~~ p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))) & p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))))) | ( ! [V5t:tp__ty_2Enum_2Enum] : (~~ p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V5t)),inj__ty_2Enum_2Enum(V2t0))))))))))))))))).
tff(ax_thm_2ETemporal__Logic_2ESWHEN,axiom,( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2ESWHEN,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> (? [V3q:$i] : (mem(V3q,arr(ty_2Enum_2Enum,bool)) & (p(ap(ap(ap(c_2ETemporal__Logic_2EWATCH,V3q),V1b),inj__ty_2Enum_2Enum(V2t0))) & (? [V4t:tp__ty_2Enum_2Enum] : ((~~ p(ap(V3q,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))) & (p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))) & p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))))))))))))))).
tff(ax_thm_2ETemporal__Logic_2ESUNTIL,axiom,( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2ESUNTIL,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> (? [V3q:$i] : (mem(V3q,arr(ty_2Enum_2Enum,bool)) & (p(ap(ap(ap(c_2ETemporal__Logic_2EWATCH,V3q),V1b),inj__ty_2Enum_2Enum(V2t0))) & (( ! [V4t:tp__ty_2Enum_2Enum] : (p(ap(V3q,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))) | (p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))) | p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))))) & (? [V5t:tp__ty_2Enum_2Enum] : p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V5t)),inj__ty_2Enum_2Enum(V2t0)))))))))))))))).
tff(ax_thm_2ETemporal__Logic_2ESBEFORE,axiom,( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2ESBEFORE,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> (? [V3q:$i] : (mem(V3q,arr(ty_2Enum_2Enum,bool)) & (p(ap(ap(ap(c_2ETemporal__Logic_2EWATCH,V3q),V1b),inj__ty_2Enum_2Enum(V2t0))) & (? [V4t:tp__ty_2Enum_2Enum] : ((~~ p(ap(V3q,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))) & ((~~ p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))) & p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2EWATCH__EXISTS,lemma,(( ! [V0b:$i] : (mem(V0b,arr(ty_2Enum_2Enum,bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : (? [V2q:$i] : (mem(V2q,arr(ty_2Enum_2Enum,bool)) & p(ap(ap(ap(c_2ETemporal__Logic_2EWATCH,V2q),V0b),inj__ty_2Enum_2Enum(V1t0)))))))))).
tff(conj_thm_2ETemporal__Logic_2EWELL__ORDER,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,bool)) => ((? [V1n:tp__ty_2Enum_2Enum] : p(ap(V0P,inj__ty_2Enum_2Enum(V1n)))) <=> (? [V2m:tp__ty_2Enum_2Enum] : (p(ap(V0P,inj__ty_2Enum_2Enum(V2m))) & ( ! [V3n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3n)),inj__ty_2Enum_2Enum(V2m))) => (~~ p(ap(V0P,inj__ty_2Enum_2Enum(V3n))))))))))))).
tff(conj_thm_2ETemporal__Logic_2EWELL__ORDER__UNIQUE,lemma,(( ! [V0m2:tp__ty_2Enum_2Enum] : ( ! [V1m1:tp__ty_2Enum_2Enum] : ( ! [V2P:$i] : (mem(V2P,arr(ty_2Enum_2Enum,bool)) => (((p(ap(V2P,inj__ty_2Enum_2Enum(V1m1))) & ( ! [V3n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3n)),inj__ty_2Enum_2Enum(V1m1))) => (~~ p(ap(V2P,inj__ty_2Enum_2Enum(V3n))))))) & (p(ap(V2P,inj__ty_2Enum_2Enum(V0m2))) & ( ! [V4n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V4n)),inj__ty_2Enum_2Enum(V0m2))) => (~~ p(ap(V2P,inj__ty_2Enum_2Enum(V4n)))))))) => (V1m1 = V0m2)))))))).
tff(conj_thm_2ETemporal__Logic_2EDELTA__CASES,lemma,(( ! [V0b:$i] : (mem(V0b,arr(ty_2Enum_2Enum,bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : ((? [V2d:tp__ty_2Enum_2Enum] : (( ! [V3t:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3t)),inj__ty_2Enum_2Enum(V2d))) => (~~ p(ap(V0b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V3t)),inj__ty_2Enum_2Enum(V1t0))))))) & p(ap(V0b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2d)),inj__ty_2Enum_2Enum(V1t0)))))) | ( ! [V4d:tp__ty_2Enum_2Enum] : (~~ p(ap(V0b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4d)),inj__ty_2Enum_2Enum(V1t0)))))))))))).
tff(conj_thm_2ETemporal__Logic_2EWHEN__IMP,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EWHEN,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> ( ! [V3q:$i] : (mem(V3q,arr(ty_2Enum_2Enum,bool)) => (p(ap(ap(ap(c_2ETemporal__Logic_2EWATCH,V3q),V1b),inj__ty_2Enum_2Enum(V2t0))) => ( ! [V4t:tp__ty_2Enum_2Enum] : (p(ap(V3q,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))) | (p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))) => p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2EUNTIL__IMP,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EUNTIL,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> ( ! [V3q:$i] : (mem(V3q,arr(ty_2Enum_2Enum,bool)) => (p(ap(ap(ap(c_2ETemporal__Logic_2EWATCH,V3q),V1b),inj__ty_2Enum_2Enum(V2t0))) => ( ! [V4t:tp__ty_2Enum_2Enum] : (p(ap(V3q,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))) | (p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))) | p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2EBEFORE__IMP,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EBEFORE,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> ( ! [V3q:$i] : (mem(V3q,arr(ty_2Enum_2Enum,bool)) => (p(ap(ap(ap(c_2ETemporal__Logic_2EWATCH,V3q),V1b),inj__ty_2Enum_2Enum(V2t0))) => ((? [V4t:tp__ty_2Enum_2Enum] : ((~~ p(ap(V3q,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))) & ((~~ p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))) & p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))))) | ( ! [V5t:tp__ty_2Enum_2Enum] : (~~ p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V5t)),inj__ty_2Enum_2Enum(V2t0)))))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2ESWHEN__IMP,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2ESWHEN,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> ( ! [V3q:$i] : (mem(V3q,arr(ty_2Enum_2Enum,bool)) => (p(ap(ap(ap(c_2ETemporal__Logic_2EWATCH,V3q),V1b),inj__ty_2Enum_2Enum(V2t0))) => (? [V4t:tp__ty_2Enum_2Enum] : ((~~ p(ap(V3q,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))) & (p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))) & p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2ESUNTIL__IMP,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2ESUNTIL,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> ( ! [V3q:$i] : (mem(V3q,arr(ty_2Enum_2Enum,bool)) => (p(ap(ap(ap(c_2ETemporal__Logic_2EWATCH,V3q),V1b),inj__ty_2Enum_2Enum(V2t0))) => (( ! [V4t:tp__ty_2Enum_2Enum] : (p(ap(V3q,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))) | (p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))) | p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))))) & (? [V5t:tp__ty_2Enum_2Enum] : p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V5t)),inj__ty_2Enum_2Enum(V2t0))))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2ESBEFORE__IMP,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2ESBEFORE,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> ( ! [V3q:$i] : (mem(V3q,arr(ty_2Enum_2Enum,bool)) => (p(ap(ap(ap(c_2ETemporal__Logic_2EWATCH,V3q),V1b),inj__ty_2Enum_2Enum(V2t0))) => (? [V4t:tp__ty_2Enum_2Enum] : ((~~ p(ap(V3q,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))) & ((~~ p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))) & p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2EALWAYS__SIGNAL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2ETemporal__Logic_2EALWAYS,V0a),inj__ty_2Enum_2Enum(V1t0))) <=> ( ! [V2t:tp__ty_2Enum_2Enum] : p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2t)),inj__ty_2Enum_2Enum(V1t0))))))))))).
tff(conj_thm_2ETemporal__Logic_2EEVENTUAL__SIGNAL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2ETemporal__Logic_2EEVENTUAL,V0a),inj__ty_2Enum_2Enum(V1t0))) <=> (? [V2t:tp__ty_2Enum_2Enum] : p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2t)),inj__ty_2Enum_2Enum(V1t0))))))))))).
tff(conj_thm_2ETemporal__Logic_2EWATCH__SIGNAL,lemma,(( ! [V0q:$i] : (mem(V0q,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EWATCH,V0q),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> ((( ! [V3t:tp__ty_2Enum_2Enum] : (~~ p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V3t)),inj__ty_2Enum_2Enum(V2t0)))))) => ( ! [V4t:tp__ty_2Enum_2Enum] : (~~ p(ap(V0q,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))))) & ( ! [V5d:tp__ty_2Enum_2Enum] : ((p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V5d)),inj__ty_2Enum_2Enum(V2t0)))) & ( ! [V6t:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V6t)),inj__ty_2Enum_2Enum(V5d))) => (~~ p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V6t)),inj__ty_2Enum_2Enum(V2t0)))))))) => (( ! [V7t:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V7t)),inj__ty_2Enum_2Enum(V5d))) => (~~ p(ap(V0q,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V7t)),inj__ty_2Enum_2Enum(V2t0))))))) & ( ! [V8t:tp__ty_2Enum_2Enum] : p(ap(V0q,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V8t)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V5d)),inj__ty_2Enum_2Enum(V2t0))))))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2EWHEN__SIGNAL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EWHEN,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> ( ! [V3delta:tp__ty_2Enum_2Enum] : ((( ! [V4t:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V3delta))) => (~~ p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))))) & p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V3delta)),inj__ty_2Enum_2Enum(V2t0))))) => p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V3delta)),inj__ty_2Enum_2Enum(V2t0)))))))))))))).
tff(conj_thm_2ETemporal__Logic_2EUNTIL__SIGNAL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EUNTIL,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> ((( ! [V3t:tp__ty_2Enum_2Enum] : (~~ p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V3t)),inj__ty_2Enum_2Enum(V2t0)))))) => ( ! [V4t:tp__ty_2Enum_2Enum] : p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))))) & ( ! [V5d:tp__ty_2Enum_2Enum] : ((( ! [V6t:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V6t)),inj__ty_2Enum_2Enum(V5d))) => (~~ p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V6t)),inj__ty_2Enum_2Enum(V2t0))))))) & p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V5d)),inj__ty_2Enum_2Enum(V2t0))))) => ( ! [V7t:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V7t)),inj__ty_2Enum_2Enum(V5d))) => p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V7t)),inj__ty_2Enum_2Enum(V2t0))))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2EBEFORE__SIGNAL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EBEFORE,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> ( ! [V3delta:tp__ty_2Enum_2Enum] : ((( ! [V4t:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V3delta))) => (~~ p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))))) & p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V3delta)),inj__ty_2Enum_2Enum(V2t0))))) => (? [V5t:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V5t)),inj__ty_2Enum_2Enum(V3delta))) & p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V5t)),inj__ty_2Enum_2Enum(V2t0)))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2ESWHEN__SIGNAL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2ESWHEN,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> (? [V3delta:tp__ty_2Enum_2Enum] : (( ! [V4t:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V3delta))) => (~~ p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))))) & (p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V3delta)),inj__ty_2Enum_2Enum(V2t0)))) & p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V3delta)),inj__ty_2Enum_2Enum(V2t0))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2ESUNTIL__SIGNAL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2ESUNTIL,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> (? [V3delta:tp__ty_2Enum_2Enum] : (( ! [V4t:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V3delta))) => (p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))) & (~~ p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))))))) & p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V3delta)),inj__ty_2Enum_2Enum(V2t0)))))))))))))).
tff(conj_thm_2ETemporal__Logic_2ESBEFORE__SIGNAL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2ESBEFORE,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> (? [V3delta:tp__ty_2Enum_2Enum] : (p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V3delta)),inj__ty_2Enum_2Enum(V2t0)))) & ( ! [V4t:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V3delta))) => (~~ p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2ENEXT__LINORD,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2ETemporal__Logic_2ENEXT,V0a),inj__ty_2Enum_2Enum(V1t0))) <=> (? [V2t1:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1t0)),inj__ty_2Enum_2Enum(V2t1))) & (( ! [V3t3:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1t0)),inj__ty_2Enum_2Enum(V3t3))) => p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V2t1)),inj__ty_2Enum_2Enum(V3t3))))) & p(ap(V0a,inj__ty_2Enum_2Enum(V2t1)))))))))))).
tff(conj_thm_2ETemporal__Logic_2EALWAYS__LINORD,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2ETemporal__Logic_2EALWAYS,V0a),inj__ty_2Enum_2Enum(V1t0))) <=> ( ! [V2t1:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1t0)),inj__ty_2Enum_2Enum(V2t1))) => p(ap(V0a,inj__ty_2Enum_2Enum(V2t1))))))))))).
tff(conj_thm_2ETemporal__Logic_2EEVENTUAL__LINORD,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2ETemporal__Logic_2EEVENTUAL,V0a),inj__ty_2Enum_2Enum(V1t0))) <=> (? [V2t1:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1t0)),inj__ty_2Enum_2Enum(V2t1))) & p(ap(V0a,inj__ty_2Enum_2Enum(V2t1))))))))))).
tff(conj_thm_2ETemporal__Logic_2ESUNTIL__LINORD,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2ESUNTIL,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> (? [V3t1:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V2t0)),inj__ty_2Enum_2Enum(V3t1))) & (p(ap(V1b,inj__ty_2Enum_2Enum(V3t1))) & p(ap(c_2ETemporal__Logic_2EUPTO,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))),inj__ty_2Enum_2Enum(V2t0)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)),inj__ty_2Enum_2Enum(V3t1)),V0a))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2EUNTIL__LINORD,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EUNTIL,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> ( ! [V3t1:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V2t0)),inj__ty_2Enum_2Enum(V3t1))) & ((~~ p(ap(V1b,inj__ty_2Enum_2Enum(V3t1)))) & p(ap(c_2ETemporal__Logic_2EUPTO,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))),inj__ty_2Enum_2Enum(V2t0)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)),inj__ty_2Enum_2Enum(V3t1)),f879(V1b))))))) => p(ap(V0a,inj__ty_2Enum_2Enum(V3t1))))))))))))).
tff(conj_thm_2ETemporal__Logic_2ESBEFORE__LINORD,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2ESBEFORE,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> (? [V3t1:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V2t0)),inj__ty_2Enum_2Enum(V3t1))) & (p(ap(V0a,inj__ty_2Enum_2Enum(V3t1))) & ((~~ p(ap(V1b,inj__ty_2Enum_2Enum(V3t1)))) & p(ap(c_2ETemporal__Logic_2EUPTO,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))),inj__ty_2Enum_2Enum(V2t0)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)),inj__ty_2Enum_2Enum(V3t1)),f879(V1b))))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2EBEFORE__LINORD,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EBEFORE,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> ( ! [V3t1:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V2t0)),inj__ty_2Enum_2Enum(V3t1))) & p(ap(c_2ETemporal__Logic_2EUPTO,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))),inj__ty_2Enum_2Enum(V2t0)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)),inj__ty_2Enum_2Enum(V3t1)),f880(V0a)))))) => (~~ p(ap(V1b,inj__ty_2Enum_2Enum(V3t1)))))))))))))).
tff(conj_thm_2ETemporal__Logic_2ESWHEN__LINORD,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2ESWHEN,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> (? [V3t1:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V2t0)),inj__ty_2Enum_2Enum(V3t1))) & (p(ap(V0a,inj__ty_2Enum_2Enum(V3t1))) & (p(ap(V1b,inj__ty_2Enum_2Enum(V3t1))) & p(ap(c_2ETemporal__Logic_2EUPTO,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))),inj__ty_2Enum_2Enum(V2t0)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)),inj__ty_2Enum_2Enum(V3t1)),f879(V1b))))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2EWHEN__LINORD,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EWHEN,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> ( ! [V3t1:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V2t0)),inj__ty_2Enum_2Enum(V3t1))) & (p(ap(V1b,inj__ty_2Enum_2Enum(V3t1))) & p(ap(c_2ETemporal__Logic_2EUPTO,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))),inj__ty_2Enum_2Enum(V2t0)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)),inj__ty_2Enum_2Enum(V3t1)),f879(V1b))))))) => p(ap(V0a,inj__ty_2Enum_2Enum(V3t1))))))))))))).
tff(conj_thm_2ETemporal__Logic_2EALWAYS__AS__WHEN,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2EALWAYS,V0a) = ap(ap(c_2ETemporal__Logic_2EWHEN,k(ty_2Enum_2Enum,c_2Ebool_2EF)),f881(V0a))))))).
tff(conj_thm_2ETemporal__Logic_2EEVENTUAL__AS__WHEN,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2EEVENTUAL,V0a) = f882(V0a)))))).
tff(conj_thm_2ETemporal__Logic_2EUNTIL__AS__WHEN,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EUNTIL,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2EWHEN,V1b),f883(V0a,V1b))))))))).
tff(conj_thm_2ETemporal__Logic_2EBEFORE__AS__WHEN,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EBEFORE,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2EWHEN,f884(V1b)),f885(V0a,V1b))))))))).
tff(conj_thm_2ETemporal__Logic_2ESWHEN__AS__WHEN,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2ESWHEN,V0a),V1b) = f886(V0a,V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2ESWHEN__AS__NOT__WHEN,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2ESWHEN,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> (~~ p(ap(ap(ap(c_2ETemporal__Logic_2EWHEN,f887(V0a)),V1b),inj__ty_2Enum_2Enum(V2t0)))))))))))).
tff(conj_thm_2ETemporal__Logic_2ESUNTIL__AS__WHEN,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2ESUNTIL,V0a),V1b) = f889(V0a,V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2ESBEFORE__AS__WHEN,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2ESBEFORE,V0a),V1b) = f892(V1b,V0a)))))))).
tff(conj_thm_2ETemporal__Logic_2EBEFORE__AS__WHEN__UNTIL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EBEFORE,V0a),V1b) = f893(V0a,V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2EBEFORE__HW,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EBEFORE,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> (? [V3q:$i] : (mem(V3q,arr(ty_2Enum_2Enum,bool)) & (p(ap(ap(ap(c_2ETemporal__Logic_2EWATCH,V3q),V0a),inj__ty_2Enum_2Enum(V2t0))) & ( ! [V4t:tp__ty_2Enum_2Enum] : (p(ap(V3q,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))) | (~~ p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2EALWAYS__AS__UNTIL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2EALWAYS,V0a) = ap(ap(c_2ETemporal__Logic_2EUNTIL,V0a),k(ty_2Enum_2Enum,c_2Ebool_2EF))))))).
tff(conj_thm_2ETemporal__Logic_2EEVENTUAL__AS__UNTIL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2EEVENTUAL,V0a) = f894(V0a)))))).
tff(conj_thm_2ETemporal__Logic_2EWHEN__AS__UNTIL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EWHEN,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2EUNTIL,f884(V1b)),f895(V0a,V1b))))))))).
tff(conj_thm_2ETemporal__Logic_2EBEFORE__AS__UNTIL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EBEFORE,V0a),V1b) = f896(V0a,V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2ESWHEN__AS__UNTIL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2ESWHEN,V0a),V1b) = f898(V0a,V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2ESUNTIL__AS__UNTIL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2ESUNTIL,V0a),V1b) = f899(V0a,V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2ESBEFORE__AS__UNTIL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2ESBEFORE,V0a),V1b) = f900(V0a,V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2EALWAYS__AS__BEFORE,lemma,(( ! [V0b:$i] : (mem(V0b,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2EALWAYS,V0b) = ap(ap(c_2ETemporal__Logic_2EBEFORE,k(ty_2Enum_2Enum,c_2Ebool_2EF)),f901(V0b))))))).
tff(conj_thm_2ETemporal__Logic_2EEVENTUAL__AS__BEFORE,lemma,(( ! [V0b:$i] : (mem(V0b,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2EEVENTUAL,V0b) = f902(V0b)))))).
tff(conj_thm_2ETemporal__Logic_2EWHEN__AS__BEFORE,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EWHEN,V0a),V1b) = f903(V0a,V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2EUNTIL__AS__BEFORE,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EUNTIL,V0a),V1b) = f904(V1b,V0a)))))))).
tff(conj_thm_2ETemporal__Logic_2ESWHEN__AS__BEFORE,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2ESWHEN,V0a),V1b) = f905(V0a,V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2ESUNTIL__AS__BEFORE,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2ESUNTIL,V0a),V1b) = f906(V0a,V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2ESBEFORE__AS__BEFORE,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2ESBEFORE,V0a),V1b) = f907(V1b,V0a)))))))).
tff(conj_thm_2ETemporal__Logic_2EWHEN__SWHEN__LEMMA,lemma,(( ! [V0b:$i] : (mem(V0b,arr(ty_2Enum_2Enum,bool)) => ( ! [V1a:$i] : (mem(V1a,arr(ty_2Enum_2Enum,bool)) => p(ap(ap(ap(c_2Ebool_2ECOND(bool),ap(c_2Ebool_2E_21(ty_2Enum_2Enum),f909(V0b))),ap(c_2Ebool_2E_21(ty_2Enum_2Enum),f910(V0b,V1a))),ap(c_2Ebool_2E_3F(ty_2Enum_2Enum),f912(V0b,V1a)))))))))).
tff(conj_thm_2ETemporal__Logic_2EALWAYS__AS__SWHEN,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2EALWAYS,V0a) = f913(V0a)))))).
tff(conj_thm_2ETemporal__Logic_2EEVENTUAL__AS__SWHEN,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2EEVENTUAL,V0a) = ap(ap(c_2ETemporal__Logic_2ESWHEN,k(ty_2Enum_2Enum,c_2Ebool_2ET)),V0a)))))).
tff(conj_thm_2ETemporal__Logic_2EWHEN__AS__SWHEN,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EWHEN,V0a),V1b) = f914(V0a,V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2EWHEN__AS__NOT__SWHEN,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EWHEN,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> (~~ p(ap(ap(ap(c_2ETemporal__Logic_2ESWHEN,f887(V0a)),V1b),inj__ty_2Enum_2Enum(V2t0)))))))))))).
tff(conj_thm_2ETemporal__Logic_2EUNTIL__AS__SWHEN,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EUNTIL,V0a),V1b) = f915(V1b,V0a)))))))).
tff(conj_thm_2ETemporal__Logic_2EBEFORE__AS__SWHEN,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EBEFORE,V0a),V1b) = f917(V0a,V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2EBEFORE__AS__NOT__SWHEN,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EBEFORE,V0a),V1b) = f918(V0a,V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2ESUNTIL__AS__SWHEN,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2ESUNTIL,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2ESWHEN,V1b),f883(V0a,V1b))))))))).
tff(conj_thm_2ETemporal__Logic_2ESBEFORE__AS__SWHEN,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2ESBEFORE,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2ESWHEN,f884(V1b)),f885(V0a,V1b))))))))).
tff(conj_thm_2ETemporal__Logic_2EALWAYS__AS__SUNTIL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2EALWAYS,V0a) = f919(V0a)))))).
tff(conj_thm_2ETemporal__Logic_2EEVENTUAL__AS__SUNTIL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2EEVENTUAL,V0a) = ap(ap(c_2ETemporal__Logic_2ESUNTIL,k(ty_2Enum_2Enum,c_2Ebool_2ET)),V0a)))))).
tff(conj_thm_2ETemporal__Logic_2EWHEN__AS__SUNTIL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EWHEN,V0a),V1b) = f921(V0a,V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2EUNTIL__AS__SUNTIL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EUNTIL,V0a),V1b) = f922(V1b,V0a)))))))).
tff(conj_thm_2ETemporal__Logic_2EBEFORE__AS__SUNTIL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EBEFORE,V0a),V1b) = f923(V0a,V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2ESWHEN__AS__SUNTIL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2ESWHEN,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2ESUNTIL,f884(V1b)),f895(V0a,V1b))))))))).
tff(conj_thm_2ETemporal__Logic_2ESBEFORE__AS__SUNTIL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2ESBEFORE,V0a),V1b) = f924(V1b,V0a)))))))).
tff(conj_thm_2ETemporal__Logic_2EALWAYS__AS__SBEFORE,lemma,(( ! [V0b:$i] : (mem(V0b,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2EALWAYS,V0b) = f925(V0b)))))).
tff(conj_thm_2ETemporal__Logic_2EEVENTUAL__AS__SBEFORE,lemma,(( ! [V0b:$i] : (mem(V0b,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2EEVENTUAL,V0b) = ap(ap(c_2ETemporal__Logic_2ESBEFORE,V0b),k(ty_2Enum_2Enum,c_2Ebool_2EF))))))).
tff(conj_thm_2ETemporal__Logic_2EWHEN__AS__SBEFORE,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EWHEN,V0a),V1b) = f927(V0a,V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2EUNTIL__AS__SBEFORE,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EUNTIL,V0a),V1b) = f928(V0a,V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2ESWHEN__AS__SBEFORE,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2ESWHEN,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2ESBEFORE,V1b),f929(V0a,V1b))))))))).
tff(conj_thm_2ETemporal__Logic_2ESUNTIL__AS__SBEFORE,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2ESUNTIL,V0a),V1b) = f930(V0a,V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2EBEFORE__AS__SBEFORE,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EBEFORE,V0a),V1b) = f931(V0a,V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2EWHEN__SIMP,lemma,(( ! [V0b:$i] : (mem(V0b,arr(ty_2Enum_2Enum,bool)) => ( ! [V1a:$i] : (mem(V1a,arr(ty_2Enum_2Enum,bool)) => ((ap(ap(c_2ETemporal__Logic_2EWHEN,k(ty_2Enum_2Enum,c_2Ebool_2EF)),V0b) = ap(c_2ETemporal__Logic_2EALWAYS,f932(V0b))) & ((ap(ap(c_2ETemporal__Logic_2EWHEN,k(ty_2Enum_2Enum,c_2Ebool_2ET)),V0b) = k(ty_2Enum_2Enum,c_2Ebool_2ET)) & ((ap(ap(c_2ETemporal__Logic_2EWHEN,V1a),k(ty_2Enum_2Enum,c_2Ebool_2EF)) = k(ty_2Enum_2Enum,c_2Ebool_2ET)) & ((ap(ap(c_2ETemporal__Logic_2EWHEN,V1a),k(ty_2Enum_2Enum,c_2Ebool_2ET)) = f933(V1a)) & (ap(ap(c_2ETemporal__Logic_2EWHEN,V1a),V1a) = k(ty_2Enum_2Enum,c_2Ebool_2ET)))))))))))).
tff(conj_thm_2ETemporal__Logic_2EUNTIL__SIMP,lemma,(( ! [V0b:$i] : (mem(V0b,arr(ty_2Enum_2Enum,bool)) => ( ! [V1a:$i] : (mem(V1a,arr(ty_2Enum_2Enum,bool)) => ((ap(ap(c_2ETemporal__Logic_2EUNTIL,k(ty_2Enum_2Enum,c_2Ebool_2EF)),V0b) = f934(V0b)) & ((ap(ap(c_2ETemporal__Logic_2EUNTIL,k(ty_2Enum_2Enum,c_2Ebool_2ET)),V0b) = k(ty_2Enum_2Enum,c_2Ebool_2ET)) & ((ap(ap(c_2ETemporal__Logic_2EUNTIL,V1a),k(ty_2Enum_2Enum,c_2Ebool_2EF)) = ap(c_2ETemporal__Logic_2EALWAYS,V1a)) & ((ap(ap(c_2ETemporal__Logic_2EUNTIL,V1a),k(ty_2Enum_2Enum,c_2Ebool_2ET)) = k(ty_2Enum_2Enum,c_2Ebool_2ET)) & (ap(ap(c_2ETemporal__Logic_2EUNTIL,V1a),V1a) = f933(V1a)))))))))))).
tff(conj_thm_2ETemporal__Logic_2EBEFORE__SIMP,lemma,(( ! [V0b:$i] : (mem(V0b,arr(ty_2Enum_2Enum,bool)) => ( ! [V1a:$i] : (mem(V1a,arr(ty_2Enum_2Enum,bool)) => ((ap(ap(c_2ETemporal__Logic_2EBEFORE,k(ty_2Enum_2Enum,c_2Ebool_2EF)),V0b) = ap(c_2ETemporal__Logic_2EALWAYS,f932(V0b))) & ((ap(ap(c_2ETemporal__Logic_2EBEFORE,k(ty_2Enum_2Enum,c_2Ebool_2ET)),V0b) = f935(V0b)) & ((ap(ap(c_2ETemporal__Logic_2EBEFORE,V1a),k(ty_2Enum_2Enum,c_2Ebool_2EF)) = k(ty_2Enum_2Enum,c_2Ebool_2ET)) & ((ap(ap(c_2ETemporal__Logic_2EBEFORE,V1a),k(ty_2Enum_2Enum,c_2Ebool_2ET)) = k(ty_2Enum_2Enum,c_2Ebool_2EF)) & (ap(ap(c_2ETemporal__Logic_2EBEFORE,V1a),V1a) = ap(c_2ETemporal__Logic_2EALWAYS,f936(V1a))))))))))))).
tff(conj_thm_2ETemporal__Logic_2ESWHEN__SIMP,lemma,(( ! [V0b:$i] : (mem(V0b,arr(ty_2Enum_2Enum,bool)) => ( ! [V1a:$i] : (mem(V1a,arr(ty_2Enum_2Enum,bool)) => ((ap(ap(c_2ETemporal__Logic_2ESWHEN,k(ty_2Enum_2Enum,c_2Ebool_2EF)),V0b) = k(ty_2Enum_2Enum,c_2Ebool_2EF)) & ((ap(ap(c_2ETemporal__Logic_2ESWHEN,k(ty_2Enum_2Enum,c_2Ebool_2ET)),V0b) = ap(c_2ETemporal__Logic_2EEVENTUAL,V0b)) & ((ap(ap(c_2ETemporal__Logic_2ESWHEN,V1a),k(ty_2Enum_2Enum,c_2Ebool_2EF)) = k(ty_2Enum_2Enum,c_2Ebool_2EF)) & ((ap(ap(c_2ETemporal__Logic_2ESWHEN,V1a),k(ty_2Enum_2Enum,c_2Ebool_2ET)) = f937(V1a)) & (ap(ap(c_2ETemporal__Logic_2ESWHEN,V1a),V1a) = ap(c_2ETemporal__Logic_2EEVENTUAL,V1a)))))))))))).
tff(conj_thm_2ETemporal__Logic_2ESUNTIL__SIMP,lemma,(( ! [V0b:$i] : (mem(V0b,arr(ty_2Enum_2Enum,bool)) => ( ! [V1a:$i] : (mem(V1a,arr(ty_2Enum_2Enum,bool)) => ((ap(ap(c_2ETemporal__Logic_2ESUNTIL,k(ty_2Enum_2Enum,c_2Ebool_2EF)),V0b) = f934(V0b)) & ((ap(ap(c_2ETemporal__Logic_2ESUNTIL,k(ty_2Enum_2Enum,c_2Ebool_2ET)),V0b) = ap(c_2ETemporal__Logic_2EEVENTUAL,V0b)) & ((ap(ap(c_2ETemporal__Logic_2ESUNTIL,V1a),k(ty_2Enum_2Enum,c_2Ebool_2EF)) = k(ty_2Enum_2Enum,c_2Ebool_2EF)) & ((ap(ap(c_2ETemporal__Logic_2ESUNTIL,V1a),k(ty_2Enum_2Enum,c_2Ebool_2ET)) = k(ty_2Enum_2Enum,c_2Ebool_2ET)) & (ap(ap(c_2ETemporal__Logic_2ESUNTIL,V1a),V1a) = f933(V1a)))))))))))).
tff(conj_thm_2ETemporal__Logic_2ESBEFORE__SIMP,lemma,(( ! [V0b:$i] : (mem(V0b,arr(ty_2Enum_2Enum,bool)) => ( ! [V1a:$i] : (mem(V1a,arr(ty_2Enum_2Enum,bool)) => ((ap(ap(c_2ETemporal__Logic_2ESBEFORE,k(ty_2Enum_2Enum,c_2Ebool_2EF)),V0b) = k(ty_2Enum_2Enum,c_2Ebool_2EF)) & ((ap(ap(c_2ETemporal__Logic_2ESBEFORE,k(ty_2Enum_2Enum,c_2Ebool_2ET)),V0b) = f935(V0b)) & ((ap(ap(c_2ETemporal__Logic_2ESBEFORE,V1a),k(ty_2Enum_2Enum,c_2Ebool_2EF)) = ap(c_2ETemporal__Logic_2EEVENTUAL,V1a)) & ((ap(ap(c_2ETemporal__Logic_2ESBEFORE,V1a),k(ty_2Enum_2Enum,c_2Ebool_2ET)) = k(ty_2Enum_2Enum,c_2Ebool_2EF)) & (ap(ap(c_2ETemporal__Logic_2ESBEFORE,V1a),V1a) = k(ty_2Enum_2Enum,c_2Ebool_2EF)))))))))))).
tff(conj_thm_2ETemporal__Logic_2EWHEN__EVENT,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EWHEN,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2EWHEN,f938(V0a,V1b)),V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2EUNTIL__EVENT,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EUNTIL,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2EUNTIL,f939(V0a,V1b)),V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2EBEFORE__EVENT,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EBEFORE,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2EBEFORE,f939(V0a,V1b)),V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2ESWHEN__EVENT,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2ESWHEN,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2ESWHEN,f938(V0a,V1b)),V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2ESUNTIL__EVENT,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2ESUNTIL,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2ESUNTIL,f939(V0a,V1b)),V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2ESBEFORE__EVENT,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2ESBEFORE,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2ESBEFORE,f939(V0a,V1b)),V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2EIMMEDIATE__EVENT,lemma,(( ! [V0b:$i] : (mem(V0b,arr(ty_2Enum_2Enum,bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : (p(ap(V0b,inj__ty_2Enum_2Enum(V1t0))) => (( ! [V2a:$i] : (mem(V2a,arr(ty_2Enum_2Enum,bool)) => (p(ap(ap(ap(c_2ETemporal__Logic_2EWHEN,V2a),V0b),inj__ty_2Enum_2Enum(V1t0))) <=> p(ap(V2a,inj__ty_2Enum_2Enum(V1t0)))))) & (( ! [V3a:$i] : (mem(V3a,arr(ty_2Enum_2Enum,bool)) => (p(ap(ap(ap(c_2ETemporal__Logic_2EUNTIL,V3a),V0b),inj__ty_2Enum_2Enum(V1t0))) <=> $true))) & (( ! [V4a:$i] : (mem(V4a,arr(ty_2Enum_2Enum,bool)) => (p(ap(ap(ap(c_2ETemporal__Logic_2EBEFORE,V4a),V0b),inj__ty_2Enum_2Enum(V1t0))) <=> $false))) & (( ! [V5a:$i] : (mem(V5a,arr(ty_2Enum_2Enum,bool)) => (p(ap(ap(ap(c_2ETemporal__Logic_2ESWHEN,V5a),V0b),inj__ty_2Enum_2Enum(V1t0))) <=> p(ap(V5a,inj__ty_2Enum_2Enum(V1t0)))))) & (( ! [V6a:$i] : (mem(V6a,arr(ty_2Enum_2Enum,bool)) => (p(ap(ap(ap(c_2ETemporal__Logic_2ESUNTIL,V6a),V0b),inj__ty_2Enum_2Enum(V1t0))) <=> $true))) & ( ! [V7a:$i] : (mem(V7a,arr(ty_2Enum_2Enum,bool)) => (p(ap(ap(ap(c_2ETemporal__Logic_2ESBEFORE,V7a),V0b),inj__ty_2Enum_2Enum(V1t0))) <=> $false)))))))))))))).
tff(conj_thm_2ETemporal__Logic_2ENO__EVENT,lemma,(( ! [V0b:$i] : (mem(V0b,arr(ty_2Enum_2Enum,bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2ETemporal__Logic_2EALWAYS,f901(V0b)),inj__ty_2Enum_2Enum(V1t0))) => (( ! [V3a:$i] : (mem(V3a,arr(ty_2Enum_2Enum,bool)) => (p(ap(ap(ap(c_2ETemporal__Logic_2EWHEN,V3a),V0b),inj__ty_2Enum_2Enum(V1t0))) <=> $true))) & (( ! [V4a:$i] : (mem(V4a,arr(ty_2Enum_2Enum,bool)) => (p(ap(ap(ap(c_2ETemporal__Logic_2EUNTIL,V4a),V0b),inj__ty_2Enum_2Enum(V1t0))) <=> p(ap(ap(c_2ETemporal__Logic_2EALWAYS,V4a),inj__ty_2Enum_2Enum(V1t0)))))) & (( ! [V5a:$i] : (mem(V5a,arr(ty_2Enum_2Enum,bool)) => (p(ap(ap(ap(c_2ETemporal__Logic_2EBEFORE,V5a),V0b),inj__ty_2Enum_2Enum(V1t0))) <=> $true))) & (( ! [V6a:$i] : (mem(V6a,arr(ty_2Enum_2Enum,bool)) => (p(ap(ap(ap(c_2ETemporal__Logic_2ESWHEN,V6a),V0b),inj__ty_2Enum_2Enum(V1t0))) <=> $false))) & (( ! [V7a:$i] : (mem(V7a,arr(ty_2Enum_2Enum,bool)) => (p(ap(ap(ap(c_2ETemporal__Logic_2ESUNTIL,V7a),V0b),inj__ty_2Enum_2Enum(V1t0))) <=> $false))) & ( ! [V8a:$i] : (mem(V8a,arr(ty_2Enum_2Enum,bool)) => (p(ap(ap(ap(c_2ETemporal__Logic_2ESBEFORE,V8a),V0b),inj__ty_2Enum_2Enum(V1t0))) <=> p(ap(ap(c_2ETemporal__Logic_2EEVENTUAL,V8a),inj__ty_2Enum_2Enum(V1t0))))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2ESOME__EVENT,lemma,(( ! [V0b:$i] : (mem(V0b,arr(ty_2Enum_2Enum,bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2ETemporal__Logic_2EEVENTUAL,V0b),inj__ty_2Enum_2Enum(V1t0))) <=> ( ! [V2a:$i] : (mem(V2a,arr(ty_2Enum_2Enum,bool)) => (p(ap(ap(ap(c_2ETemporal__Logic_2EWHEN,V2a),V0b),inj__ty_2Enum_2Enum(V1t0))) <=> p(ap(ap(ap(c_2ETemporal__Logic_2ESWHEN,V2a),V0b),inj__ty_2Enum_2Enum(V1t0))))))) & ((p(ap(ap(c_2ETemporal__Logic_2EEVENTUAL,V0b),inj__ty_2Enum_2Enum(V1t0))) <=> ( ! [V3a:$i] : (mem(V3a,arr(ty_2Enum_2Enum,bool)) => (p(ap(ap(ap(c_2ETemporal__Logic_2EUNTIL,V3a),V0b),inj__ty_2Enum_2Enum(V1t0))) <=> p(ap(ap(ap(c_2ETemporal__Logic_2ESUNTIL,V3a),V0b),inj__ty_2Enum_2Enum(V1t0))))))) & (p(ap(ap(c_2ETemporal__Logic_2EEVENTUAL,V0b),inj__ty_2Enum_2Enum(V1t0))) <=> ( ! [V4a:$i] : (mem(V4a,arr(ty_2Enum_2Enum,bool)) => (p(ap(ap(ap(c_2ETemporal__Logic_2EBEFORE,V4a),V0b),inj__ty_2Enum_2Enum(V1t0))) <=> p(ap(ap(ap(c_2ETemporal__Logic_2ESBEFORE,V4a),V0b),inj__ty_2Enum_2Enum(V1t0)))))))))))))).
tff(conj_thm_2ETemporal__Logic_2EMORE__EVENT,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ((ap(ap(c_2ETemporal__Logic_2EWHEN,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2EWHEN,f938(V0a,V1b)),V1b)) & ((ap(ap(c_2ETemporal__Logic_2EUNTIL,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2EUNTIL,f940(V0a,V1b)),V1b)) & ((ap(ap(c_2ETemporal__Logic_2EBEFORE,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2EBEFORE,f941(V0a,V1b)),V1b)) & ((ap(ap(c_2ETemporal__Logic_2ESWHEN,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2ESWHEN,f942(V0a,V1b)),V1b)) & ((ap(ap(c_2ETemporal__Logic_2ESUNTIL,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2ESUNTIL,f943(V0a,V1b)),V1b)) & (ap(ap(c_2ETemporal__Logic_2ESBEFORE,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2ESBEFORE,f944(V0a,V1b)),V1b))))))))))))).
tff(conj_thm_2ETemporal__Logic_2ENOT__NEXT,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2ENEXT,f945(V0P)) = f946(V0P)))))).
tff(conj_thm_2ETemporal__Logic_2EAND__NEXT,lemma,(( ! [V0Q:$i] : (mem(V0Q,arr(ty_2Enum_2Enum,bool)) => ( ! [V1P:$i] : (mem(V1P,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2ENEXT,f947(V1P,V0Q)) = f948(V1P,V0Q)))))))).
tff(conj_thm_2ETemporal__Logic_2EOR__NEXT,lemma,(( ! [V0Q:$i] : (mem(V0Q,arr(ty_2Enum_2Enum,bool)) => ( ! [V1P:$i] : (mem(V1P,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2ENEXT,f949(V1P,V0Q)) = f950(V1P,V0Q)))))))).
tff(conj_thm_2ETemporal__Logic_2EIMP__NEXT,lemma,(( ! [V0Q:$i] : (mem(V0Q,arr(ty_2Enum_2Enum,bool)) => ( ! [V1P:$i] : (mem(V1P,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2ENEXT,f951(V1P,V0Q)) = f952(V1P,V0Q)))))))).
tff(conj_thm_2ETemporal__Logic_2EEQUIV__NEXT,lemma,(( ! [V0Q:$i] : (mem(V0Q,arr(ty_2Enum_2Enum,bool)) => ( ! [V1P:$i] : (mem(V1P,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2ENEXT,f953(V1P,V0Q)) = f954(V1P,V0Q)))))))).
tff(conj_thm_2ETemporal__Logic_2EALWAYS__NEXT,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2ENEXT,ap(c_2ETemporal__Logic_2EALWAYS,V0a)) = ap(c_2ETemporal__Logic_2EALWAYS,ap(c_2ETemporal__Logic_2ENEXT,V0a))))))).
tff(conj_thm_2ETemporal__Logic_2EEVENTUAL__NEXT,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2ENEXT,ap(c_2ETemporal__Logic_2EEVENTUAL,V0a)) = ap(c_2ETemporal__Logic_2EEVENTUAL,ap(c_2ETemporal__Logic_2ENEXT,V0a))))))).
tff(conj_thm_2ETemporal__Logic_2EWHEN__NEXT,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2ENEXT,ap(ap(c_2ETemporal__Logic_2EWHEN,V0a),V1b)) = ap(ap(c_2ETemporal__Logic_2EWHEN,ap(c_2ETemporal__Logic_2ENEXT,V0a)),ap(c_2ETemporal__Logic_2ENEXT,V1b))))))))).
tff(conj_thm_2ETemporal__Logic_2EUNTIL__NEXT,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2ENEXT,ap(ap(c_2ETemporal__Logic_2EUNTIL,V0a),V1b)) = ap(ap(c_2ETemporal__Logic_2EUNTIL,ap(c_2ETemporal__Logic_2ENEXT,V0a)),ap(c_2ETemporal__Logic_2ENEXT,V1b))))))))).
tff(conj_thm_2ETemporal__Logic_2EBEFORE__NEXT,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2ENEXT,ap(ap(c_2ETemporal__Logic_2EBEFORE,V0a),V1b)) = ap(ap(c_2ETemporal__Logic_2EBEFORE,ap(c_2ETemporal__Logic_2ENEXT,V0a)),ap(c_2ETemporal__Logic_2ENEXT,V1b))))))))).
tff(conj_thm_2ETemporal__Logic_2ESWHEN__NEXT,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2ENEXT,ap(ap(c_2ETemporal__Logic_2ESWHEN,V0a),V1b)) = ap(ap(c_2ETemporal__Logic_2ESWHEN,ap(c_2ETemporal__Logic_2ENEXT,V0a)),ap(c_2ETemporal__Logic_2ENEXT,V1b))))))))).
tff(conj_thm_2ETemporal__Logic_2ESUNTIL__NEXT,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2ENEXT,ap(ap(c_2ETemporal__Logic_2ESUNTIL,V0a),V1b)) = ap(ap(c_2ETemporal__Logic_2ESUNTIL,ap(c_2ETemporal__Logic_2ENEXT,V0a)),ap(c_2ETemporal__Logic_2ENEXT,V1b))))))))).
tff(conj_thm_2ETemporal__Logic_2ESBEFORE__NEXT,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2ENEXT,ap(ap(c_2ETemporal__Logic_2ESBEFORE,V0a),V1b)) = ap(ap(c_2ETemporal__Logic_2ESBEFORE,ap(c_2ETemporal__Logic_2ENEXT,V0a)),ap(c_2ETemporal__Logic_2ENEXT,V1b))))))))).
tff(conj_thm_2ETemporal__Logic_2EALWAYS__REC,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2ETemporal__Logic_2EALWAYS,V0P),inj__ty_2Enum_2Enum(V1t0))) <=> (p(ap(V0P,inj__ty_2Enum_2Enum(V1t0))) & p(ap(ap(c_2ETemporal__Logic_2ENEXT,ap(c_2ETemporal__Logic_2EALWAYS,V0P)),inj__ty_2Enum_2Enum(V1t0)))))))))).
tff(conj_thm_2ETemporal__Logic_2EEVENTUAL__REC,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2ETemporal__Logic_2EEVENTUAL,V0P),inj__ty_2Enum_2Enum(V1t0))) <=> (p(ap(V0P,inj__ty_2Enum_2Enum(V1t0))) | p(ap(ap(c_2ETemporal__Logic_2ENEXT,ap(c_2ETemporal__Logic_2EEVENTUAL,V0P)),inj__ty_2Enum_2Enum(V1t0)))))))))).
tff(conj_thm_2ETemporal__Logic_2EWATCH__REC,lemma,(( ! [V0q:$i] : (mem(V0q,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EWATCH,V0q),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> ((~~ p(ap(V0q,inj__ty_2Enum_2Enum(V2t0)))) & p(ap(ap(ap(c_2Ebool_2ECOND(bool),ap(V1b,inj__ty_2Enum_2Enum(V2t0))),ap(ap(c_2ETemporal__Logic_2ENEXT,ap(c_2ETemporal__Logic_2EALWAYS,V0q)),inj__ty_2Enum_2Enum(V2t0))),ap(ap(c_2ETemporal__Logic_2ENEXT,ap(ap(c_2ETemporal__Logic_2EWATCH,V0q),V1b)),inj__ty_2Enum_2Enum(V2t0))))))))))))).
tff(conj_thm_2ETemporal__Logic_2EWHEN__REC,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EWHEN,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> p(ap(ap(ap(c_2Ebool_2ECOND(bool),ap(V1b,inj__ty_2Enum_2Enum(V2t0))),ap(V0a,inj__ty_2Enum_2Enum(V2t0))),ap(ap(c_2ETemporal__Logic_2ENEXT,ap(ap(c_2ETemporal__Logic_2EWHEN,V0a),V1b)),inj__ty_2Enum_2Enum(V2t0)))))))))))).
tff(conj_thm_2ETemporal__Logic_2EUNTIL__REC,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EUNTIL,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> ((~~ p(ap(V1b,inj__ty_2Enum_2Enum(V2t0)))) => (p(ap(V0a,inj__ty_2Enum_2Enum(V2t0))) & p(ap(ap(c_2ETemporal__Logic_2ENEXT,ap(ap(c_2ETemporal__Logic_2EUNTIL,V0a),V1b)),inj__ty_2Enum_2Enum(V2t0))))))))))))).
tff(conj_thm_2ETemporal__Logic_2EBEFORE__REC,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EBEFORE,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> ((~~ p(ap(V1b,inj__ty_2Enum_2Enum(V2t0)))) & (p(ap(V0a,inj__ty_2Enum_2Enum(V2t0))) | p(ap(ap(c_2ETemporal__Logic_2ENEXT,ap(ap(c_2ETemporal__Logic_2EBEFORE,V0a),V1b)),inj__ty_2Enum_2Enum(V2t0))))))))))))).
tff(conj_thm_2ETemporal__Logic_2ESWHEN__REC,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2ESWHEN,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> p(ap(ap(ap(c_2Ebool_2ECOND(bool),ap(V1b,inj__ty_2Enum_2Enum(V2t0))),ap(V0a,inj__ty_2Enum_2Enum(V2t0))),ap(ap(c_2ETemporal__Logic_2ENEXT,ap(ap(c_2ETemporal__Logic_2ESWHEN,V0a),V1b)),inj__ty_2Enum_2Enum(V2t0)))))))))))).
tff(conj_thm_2ETemporal__Logic_2ESUNTIL__REC,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2ESUNTIL,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> ((~~ p(ap(V1b,inj__ty_2Enum_2Enum(V2t0)))) => (p(ap(V0a,inj__ty_2Enum_2Enum(V2t0))) & p(ap(ap(c_2ETemporal__Logic_2ENEXT,ap(ap(c_2ETemporal__Logic_2ESUNTIL,V0a),V1b)),inj__ty_2Enum_2Enum(V2t0))))))))))))).
tff(conj_thm_2ETemporal__Logic_2ESBEFORE__REC,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2ESBEFORE,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> ((~~ p(ap(V1b,inj__ty_2Enum_2Enum(V2t0)))) & (p(ap(V0a,inj__ty_2Enum_2Enum(V2t0))) | p(ap(ap(c_2ETemporal__Logic_2ENEXT,ap(ap(c_2ETemporal__Logic_2ESBEFORE,V0a),V1b)),inj__ty_2Enum_2Enum(V2t0))))))))))))).
tff(conj_thm_2ETemporal__Logic_2EALWAYS__FIX,lemma,(( ! [V0y:$i] : (mem(V0y,arr(ty_2Enum_2Enum,bool)) => ( ! [V1a:$i] : (mem(V1a,arr(ty_2Enum_2Enum,bool)) => ((V0y = f955(V1a,V0y)) <=> ((V0y = ap(c_2ETemporal__Logic_2EALWAYS,V1a)) | (V0y = k(ty_2Enum_2Enum,c_2Ebool_2EF)))))))))).
tff(conj_thm_2ETemporal__Logic_2EEVENTUAL__FIX,lemma,(( ! [V0y:$i] : (mem(V0y,arr(ty_2Enum_2Enum,bool)) => ( ! [V1a:$i] : (mem(V1a,arr(ty_2Enum_2Enum,bool)) => ((V0y = f956(V1a,V0y)) <=> ((V0y = ap(c_2ETemporal__Logic_2EEVENTUAL,V1a)) | (V0y = k(ty_2Enum_2Enum,c_2Ebool_2ET)))))))))).
tff(conj_thm_2ETemporal__Logic_2EWHEN__FIX,lemma,(( ! [V0y:$i] : (mem(V0y,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2a:$i] : (mem(V2a,arr(ty_2Enum_2Enum,bool)) => ((V0y = f957(V2a,V1b,V0y)) <=> ((V0y = ap(ap(c_2ETemporal__Logic_2EWHEN,V2a),V1b)) | (V0y = ap(ap(c_2ETemporal__Logic_2ESWHEN,V2a),V1b)))))))))))).
tff(conj_thm_2ETemporal__Logic_2EUNTIL__FIX,lemma,(( ! [V0y:$i] : (mem(V0y,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2a:$i] : (mem(V2a,arr(ty_2Enum_2Enum,bool)) => ((V0y = f958(V0y,V2a,V1b)) <=> ((V0y = ap(ap(c_2ETemporal__Logic_2EUNTIL,V2a),V1b)) | (V0y = ap(ap(c_2ETemporal__Logic_2ESUNTIL,V2a),V1b)))))))))))).
tff(conj_thm_2ETemporal__Logic_2EBEFORE__FIX,lemma,(( ! [V0b:$i] : (mem(V0b,arr(ty_2Enum_2Enum,bool)) => ( ! [V1a:$i] : (mem(V1a,arr(ty_2Enum_2Enum,bool)) => ( ! [V2y:$i] : (mem(V2y,arr(ty_2Enum_2Enum,bool)) => ((V2y = f959(V2y,V1a,V0b)) <=> ((V2y = ap(ap(c_2ETemporal__Logic_2EBEFORE,V1a),V0b)) | (V2y = ap(ap(c_2ETemporal__Logic_2ESBEFORE,V1a),V0b)))))))))))).
tff(conj_thm_2ETemporal__Logic_2EWHEN__INVARIANT,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EWHEN,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> (? [V3J:$i] : (mem(V3J,arr(ty_2Enum_2Enum,bool)) & (p(ap(V3J,inj__ty_2Enum_2Enum(V2t0))) & (( ! [V4t:tp__ty_2Enum_2Enum] : (((~~ p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))) & p(ap(V3J,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))) => p(ap(V3J,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))))) & ( ! [V5d:tp__ty_2Enum_2Enum] : ((p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V5d)),inj__ty_2Enum_2Enum(V2t0)))) & p(ap(V3J,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V5d)),inj__ty_2Enum_2Enum(V2t0))))) => p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V5d)),inj__ty_2Enum_2Enum(V2t0)))))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2EUNTIL__INVARIANT,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EUNTIL,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> (? [V3J:$i] : (mem(V3J,arr(ty_2Enum_2Enum,bool)) & (p(ap(V3J,inj__ty_2Enum_2Enum(V2t0))) & ( ! [V4t:tp__ty_2Enum_2Enum] : ((p(ap(V3J,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))) & (~~ p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))))) => (p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))) & p(ap(V3J,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2EBEFORE__INVARIANT,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2EBEFORE,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> (? [V3J:$i] : (mem(V3J,arr(ty_2Enum_2Enum,bool)) & (p(ap(V3J,inj__ty_2Enum_2Enum(V2t0))) & (( ! [V4t:tp__ty_2Enum_2Enum] : ((p(ap(V3J,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))) & (~~ p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))))) => p(ap(V3J,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))))) & ( ! [V5d:tp__ty_2Enum_2Enum] : (p(ap(V3J,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V5d)),inj__ty_2Enum_2Enum(V2t0)))) => (~~ p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V5d)),inj__ty_2Enum_2Enum(V2t0))))))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2EALWAYS__INVARIANT,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2ETemporal__Logic_2EALWAYS,V0a),inj__ty_2Enum_2Enum(V1t0))) <=> (? [V2J:$i] : (mem(V2J,arr(ty_2Enum_2Enum,bool)) & (p(ap(V2J,inj__ty_2Enum_2Enum(V1t0))) & ( ! [V3t:tp__ty_2Enum_2Enum] : (p(ap(V2J,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V3t)),inj__ty_2Enum_2Enum(V1t0)))) => (p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V3t)),inj__ty_2Enum_2Enum(V1t0)))) & p(ap(V2J,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V3t)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1t0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2EEVENTUAL__INVARIANT,lemma,(( ! [V0b:$i] : (mem(V0b,arr(ty_2Enum_2Enum,bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2ETemporal__Logic_2EEVENTUAL,V0b),inj__ty_2Enum_2Enum(V1t0))) <=> (? [V2J:$i] : (mem(V2J,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)) & (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(V2J,inj__ty_2Enum_2Enum(V1t0)))) & (( ! [V3t:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,ap(V2J,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V3t)),inj__ty_2Enum_2Enum(V1t0))))),ap(V2J,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V3t)),inj__ty_2Enum_2Enum(V1t0))))) | (surj__ty_2Enum_2Enum(ap(V2J,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V3t)),inj__ty_2Enum_2Enum(V1t0))))) = fo__c_2Enum_2E0))) & ( ! [V4t:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(V2J,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V1t0))))) & (surj__ty_2Enum_2Enum(ap(V2J,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V1t0))))) = fo__c_2Enum_2E0)) => p(ap(V0b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V1t0)))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2ESWHEN__INVARIANT,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2ESWHEN,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> ((? [V3J1:$i] : (mem(V3J1,arr(ty_2Enum_2Enum,bool)) & (p(ap(V3J1,inj__ty_2Enum_2Enum(V2t0))) & (( ! [V4t:tp__ty_2Enum_2Enum] : (((~~ p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))) & p(ap(V3J1,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))) => p(ap(V3J1,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))))) & ( ! [V5d:tp__ty_2Enum_2Enum] : ((p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V5d)),inj__ty_2Enum_2Enum(V2t0)))) & p(ap(V3J1,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V5d)),inj__ty_2Enum_2Enum(V2t0))))) => p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V5d)),inj__ty_2Enum_2Enum(V2t0)))))))))) & (? [V6J2:$i] : (mem(V6J2,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)) & (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(V6J2,inj__ty_2Enum_2Enum(V2t0)))) & (( ! [V7t:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,ap(V6J2,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V7t)),inj__ty_2Enum_2Enum(V2t0))))),ap(V6J2,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V7t)),inj__ty_2Enum_2Enum(V2t0))))) | (surj__ty_2Enum_2Enum(ap(V6J2,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V7t)),inj__ty_2Enum_2Enum(V2t0))))) = fo__c_2Enum_2E0))) & ( ! [V8t:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(V6J2,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V8t)),inj__ty_2Enum_2Enum(V2t0))))) & (surj__ty_2Enum_2Enum(ap(V6J2,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V8t)),inj__ty_2Enum_2Enum(V2t0))))) = fo__c_2Enum_2E0)) => p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V8t)),inj__ty_2Enum_2Enum(V2t0))))))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2ESUNTIL__INVARIANT,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2ESUNTIL,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> ((? [V3J1:$i] : (mem(V3J1,arr(ty_2Enum_2Enum,bool)) & (p(ap(V3J1,inj__ty_2Enum_2Enum(V2t0))) & ( ! [V4t:tp__ty_2Enum_2Enum] : ((p(ap(V3J1,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))) & (~~ p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))))) => (p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))) & p(ap(V3J1,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))))))))) & (? [V5J2:$i] : (mem(V5J2,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)) & (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(V5J2,inj__ty_2Enum_2Enum(V2t0)))) & (( ! [V6t:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,ap(V5J2,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V6t)),inj__ty_2Enum_2Enum(V2t0))))),ap(V5J2,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V6t)),inj__ty_2Enum_2Enum(V2t0))))) | (surj__ty_2Enum_2Enum(ap(V5J2,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V6t)),inj__ty_2Enum_2Enum(V2t0))))) = fo__c_2Enum_2E0))) & ( ! [V7t:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(V5J2,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V7t)),inj__ty_2Enum_2Enum(V2t0))))) & (surj__ty_2Enum_2Enum(ap(V5J2,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V7t)),inj__ty_2Enum_2Enum(V2t0))))) = fo__c_2Enum_2E0)) => p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V7t)),inj__ty_2Enum_2Enum(V2t0))))))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2ESBEFORE__INVARIANT,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2ETemporal__Logic_2ESBEFORE,V0a),V1b),inj__ty_2Enum_2Enum(V2t0))) <=> ((? [V3J1:$i] : (mem(V3J1,arr(ty_2Enum_2Enum,bool)) & (p(ap(V3J1,inj__ty_2Enum_2Enum(V2t0))) & (( ! [V4t:tp__ty_2Enum_2Enum] : ((p(ap(V3J1,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))) & (~~ p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0)))))) => p(ap(V3J1,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4t)),inj__ty_2Enum_2Enum(V2t0))))))) & ( ! [V5d:tp__ty_2Enum_2Enum] : (p(ap(V3J1,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V5d)),inj__ty_2Enum_2Enum(V2t0)))) => (~~ p(ap(V1b,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V5d)),inj__ty_2Enum_2Enum(V2t0))))))))))) & (? [V6J2:$i] : (mem(V6J2,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)) & (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(V6J2,inj__ty_2Enum_2Enum(V2t0)))) & (( ! [V7t:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,ap(V6J2,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V7t)),inj__ty_2Enum_2Enum(V2t0))))),ap(V6J2,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V7t)),inj__ty_2Enum_2Enum(V2t0))))) | (surj__ty_2Enum_2Enum(ap(V6J2,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V7t)),inj__ty_2Enum_2Enum(V2t0))))) = fo__c_2Enum_2E0))) & ( ! [V8t:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(V6J2,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V8t)),inj__ty_2Enum_2Enum(V2t0))))) & (surj__ty_2Enum_2Enum(ap(V6J2,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V8t)),inj__ty_2Enum_2Enum(V2t0))))) = fo__c_2Enum_2E0)) => p(ap(V0a,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V8t)),inj__ty_2Enum_2Enum(V2t0))))))))))))))))))).
tff(conj_thm_2ETemporal__Logic_2EALWAYS__IDEM,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2EALWAYS,V0a) = ap(c_2ETemporal__Logic_2EALWAYS,ap(c_2ETemporal__Logic_2EALWAYS,V0a))))))).
tff(conj_thm_2ETemporal__Logic_2EEVENTUAL__IDEM,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => (ap(c_2ETemporal__Logic_2EEVENTUAL,V0a) = ap(c_2ETemporal__Logic_2EEVENTUAL,ap(c_2ETemporal__Logic_2EEVENTUAL,V0a))))))).
tff(conj_thm_2ETemporal__Logic_2EWHEN__IDEM,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EWHEN,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2EWHEN,ap(ap(c_2ETemporal__Logic_2EWHEN,V0a),V1b)),V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2EUNTIL__IDEM,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EUNTIL,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2EUNTIL,ap(ap(c_2ETemporal__Logic_2EUNTIL,V0a),V1b)),V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2EBEFORE__IDEM,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2EBEFORE,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2EBEFORE,ap(ap(c_2ETemporal__Logic_2EBEFORE,V0a),V1b)),V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2ESWHEN__IDEM,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2ESWHEN,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2ESWHEN,ap(ap(c_2ETemporal__Logic_2ESWHEN,V0a),V1b)),V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2ESUNTIL__IDEM,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2ESUNTIL,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2ESUNTIL,ap(ap(c_2ETemporal__Logic_2ESUNTIL,V0a),V1b)),V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2ESBEFORE__IDEM,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => (ap(ap(c_2ETemporal__Logic_2ESBEFORE,V0a),V1b) = ap(ap(c_2ETemporal__Logic_2ESBEFORE,ap(ap(c_2ETemporal__Logic_2ESBEFORE,V0a),V1b)),V1b)))))))).
tff(conj_thm_2ETemporal__Logic_2ENOT__ALWAYS,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : ((~~ p(ap(ap(c_2ETemporal__Logic_2EALWAYS,V0a),inj__ty_2Enum_2Enum(V1t0)))) <=> p(ap(ap(c_2ETemporal__Logic_2EEVENTUAL,f881(V0a)),inj__ty_2Enum_2Enum(V1t0))))))))).
tff(conj_thm_2ETemporal__Logic_2ENOT__EVENTUAL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : ((~~ p(ap(ap(c_2ETemporal__Logic_2EEVENTUAL,V0a),inj__ty_2Enum_2Enum(V1t0)))) <=> p(ap(ap(c_2ETemporal__Logic_2EALWAYS,f881(V0a)),inj__ty_2Enum_2Enum(V1t0))))))))).
tff(conj_thm_2ETemporal__Logic_2ENOT__WHEN,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : ((~~ p(ap(ap(ap(c_2ETemporal__Logic_2EWHEN,V0a),V1b),inj__ty_2Enum_2Enum(V2t0)))) <=> p(ap(ap(ap(c_2ETemporal__Logic_2ESWHEN,f887(V0a)),V1b),inj__ty_2Enum_2Enum(V2t0))))))))))).
tff(conj_thm_2ETemporal__Logic_2ENOT__UNTIL,lemma,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : ((~~ p(ap(ap(ap(c_2ETemporal__Logic_2EUNTIL,V0a),V1b),inj__ty_2Enum_2Enum(V2t0)))) <=> p(ap(ap(ap(c_2ETemporal__Logic_2ESBEFORE,f887(V0a)),V1b),inj__ty_2Enum_2Enum(V2t0))))))))))).
tff(conj_thm_2ETemporal__Logic_2ENOT__BEFORE,conjecture,(( ! [V0a:$i] : (mem(V0a,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,bool)) => ( ! [V2t0:tp__ty_2Enum_2Enum] : ((~~ p(ap(ap(ap(c_2ETemporal__Logic_2EBEFORE,V0a),V1b),inj__ty_2Enum_2Enum(V2t0)))) <=> p(ap(ap(ap(c_2ETemporal__Logic_2ESUNTIL,f887(V0a)),V1b),inj__ty_2Enum_2Enum(V2t0))))))))))).
