include('Axioms/quotient^2.ax').
thf(tp_c_2EPast__Temporal__Logic_2EInitPoint,type,(c_2EPast__Temporal__Logic_2EInitPoint:$i)).
thf(mem_c_2EPast__Temporal__Logic_2EInitPoint,axiom,(mem@c_2EPast__Temporal__Logic_2EInitPoint@(arr@ty_2Enum_2Enum@bool))).
thf(tp_c_2EPast__Temporal__Logic_2EPALWAYS,type,(c_2EPast__Temporal__Logic_2EPALWAYS:$i)).
thf(mem_c_2EPast__Temporal__Logic_2EPALWAYS,axiom,(mem@c_2EPast__Temporal__Logic_2EPALWAYS@(arr@(arr@ty_2Enum_2Enum@bool)@(arr@ty_2Enum_2Enum@bool)))).
thf(tp_c_2EPast__Temporal__Logic_2EPBEFORE,type,(c_2EPast__Temporal__Logic_2EPBEFORE:$i)).
thf(mem_c_2EPast__Temporal__Logic_2EPBEFORE,axiom,(mem@c_2EPast__Temporal__Logic_2EPBEFORE@(arr@(arr@ty_2Enum_2Enum@bool)@(arr@(arr@ty_2Enum_2Enum@bool)@(arr@ty_2Enum_2Enum@bool))))).
thf(tp_c_2EPast__Temporal__Logic_2EPEVENTUAL,type,(c_2EPast__Temporal__Logic_2EPEVENTUAL:$i)).
thf(mem_c_2EPast__Temporal__Logic_2EPEVENTUAL,axiom,(mem@c_2EPast__Temporal__Logic_2EPEVENTUAL@(arr@(arr@ty_2Enum_2Enum@bool)@(arr@ty_2Enum_2Enum@bool)))).
thf(tp_c_2EPast__Temporal__Logic_2EPNEXT,type,(c_2EPast__Temporal__Logic_2EPNEXT:$i)).
thf(mem_c_2EPast__Temporal__Logic_2EPNEXT,axiom,(mem@c_2EPast__Temporal__Logic_2EPNEXT@(arr@(arr@ty_2Enum_2Enum@bool)@(arr@ty_2Enum_2Enum@bool)))).
thf(tp_c_2EPast__Temporal__Logic_2EPSBEFORE,type,(c_2EPast__Temporal__Logic_2EPSBEFORE:$i)).
thf(mem_c_2EPast__Temporal__Logic_2EPSBEFORE,axiom,(mem@c_2EPast__Temporal__Logic_2EPSBEFORE@(arr@(arr@ty_2Enum_2Enum@bool)@(arr@(arr@ty_2Enum_2Enum@bool)@(arr@ty_2Enum_2Enum@bool))))).
thf(tp_c_2EPast__Temporal__Logic_2EPSNEXT,type,(c_2EPast__Temporal__Logic_2EPSNEXT:$i)).
thf(mem_c_2EPast__Temporal__Logic_2EPSNEXT,axiom,(mem@c_2EPast__Temporal__Logic_2EPSNEXT@(arr@(arr@ty_2Enum_2Enum@bool)@(arr@ty_2Enum_2Enum@bool)))).
thf(tp_c_2EPast__Temporal__Logic_2EPSUNTIL,type,(c_2EPast__Temporal__Logic_2EPSUNTIL:$i)).
thf(mem_c_2EPast__Temporal__Logic_2EPSUNTIL,axiom,(mem@c_2EPast__Temporal__Logic_2EPSUNTIL@(arr@(arr@ty_2Enum_2Enum@bool)@(arr@(arr@ty_2Enum_2Enum@bool)@(arr@ty_2Enum_2Enum@bool))))).
thf(tp_c_2EPast__Temporal__Logic_2EPSWHEN,type,(c_2EPast__Temporal__Logic_2EPSWHEN:$i)).
thf(mem_c_2EPast__Temporal__Logic_2EPSWHEN,axiom,(mem@c_2EPast__Temporal__Logic_2EPSWHEN@(arr@(arr@ty_2Enum_2Enum@bool)@(arr@(arr@ty_2Enum_2Enum@bool)@(arr@ty_2Enum_2Enum@bool))))).
thf(tp_c_2EPast__Temporal__Logic_2EPUNTIL,type,(c_2EPast__Temporal__Logic_2EPUNTIL:$i)).
thf(mem_c_2EPast__Temporal__Logic_2EPUNTIL,axiom,(mem@c_2EPast__Temporal__Logic_2EPUNTIL@(arr@(arr@ty_2Enum_2Enum@bool)@(arr@(arr@ty_2Enum_2Enum@bool)@(arr@ty_2Enum_2Enum@bool))))).
thf(tp_c_2EPast__Temporal__Logic_2EPWHEN,type,(c_2EPast__Temporal__Logic_2EPWHEN:$i)).
thf(mem_c_2EPast__Temporal__Logic_2EPWHEN,axiom,(mem@c_2EPast__Temporal__Logic_2EPWHEN@(arr@(arr@ty_2Enum_2Enum@bool)@(arr@(arr@ty_2Enum_2Enum@bool)@(arr@ty_2Enum_2Enum@bool))))).
thf(ax_thm_2EPast__Temporal__Logic_2EInitPoint,axiom,(c_2EPast__Temporal__Logic_2EInitPoint = (lam@ty_2Enum_2Enum@(^ [V0t:$i] : (ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V0t)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))).
thf(ax_thm_2EPast__Temporal__Logic_2EPSNEXT,axiom,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V0a)@(inj__ty_2Enum_2Enum @ V1t0))) <=> ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V1t0))) & (p@(ap@V0a@(ap@c_2Eprim__rec_2EPRE@(inj__ty_2Enum_2Enum @ V1t0)))))))))).
thf(ax_thm_2EPast__Temporal__Logic_2EPNEXT,axiom,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a)@(inj__ty_2Enum_2Enum @ V1t0))) <=> ((V1t0 = fo__c_2Enum_2E0) | (p@(ap@V0a@(ap@c_2Eprim__rec_2EPRE@(inj__ty_2Enum_2Enum @ V1t0)))))))))).
thf(ax_thm_2EPast__Temporal__Logic_2EPALWAYS,axiom,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2EPast__Temporal__Logic_2EPALWAYS@V0a)@(inj__ty_2Enum_2Enum @ V1t0))) <=> ( ! [V2t:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V2t))@(inj__ty_2Enum_2Enum @ V1t0))) => (p@(ap@V0a@(inj__ty_2Enum_2Enum @ V2t)))))))))).
thf(ax_thm_2EPast__Temporal__Logic_2EPEVENTUAL,axiom,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V0a)@(inj__ty_2Enum_2Enum @ V1t0))) <=> (? [V2t:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V2t))@(inj__ty_2Enum_2Enum @ V1t0))) & (p@(ap@V0a@(inj__ty_2Enum_2Enum @ V2t)))))))))).
thf(ax_thm_2EPast__Temporal__Logic_2EPSWHEN,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_2EPast__Temporal__Logic_2EPSWHEN@V0a)@V1b)@(inj__ty_2Enum_2Enum @ V2t0))) <=> (? [V3delta:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V3delta))@(inj__ty_2Enum_2Enum @ V2t0))) & ((p@(ap@V0a@(inj__ty_2Enum_2Enum @ V3delta))) & ((p@(ap@V1b@(inj__ty_2Enum_2Enum @ V3delta))) & ( ! [V4t:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V3delta))@(inj__ty_2Enum_2Enum @ V4t))) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0)))) => (~ (p@(ap@V1b@(inj__ty_2Enum_2Enum @ V4t))))))))))))))))).
thf(ax_thm_2EPast__Temporal__Logic_2EPSUNTIL,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_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@V1b)@(inj__ty_2Enum_2Enum @ V2t0))) <=> (? [V3delta:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V3delta))@(inj__ty_2Enum_2Enum @ V2t0))) & ((p@(ap@V1b@(inj__ty_2Enum_2Enum @ V3delta))) & ( ! [V4t:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V3delta))@(inj__ty_2Enum_2Enum @ V4t))) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0)))) => ((p@(ap@V0a@(inj__ty_2Enum_2Enum @ V4t))) & (~ (p@(ap@V1b@(inj__ty_2Enum_2Enum @ V4t))))))))))))))))).
thf(ax_thm_2EPast__Temporal__Logic_2EPSBEFORE,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_2EPast__Temporal__Logic_2EPSBEFORE@V0a)@V1b)@(inj__ty_2Enum_2Enum @ V2t0))) <=> (? [V3delta:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V3delta))@(inj__ty_2Enum_2Enum @ V2t0))) & ((p@(ap@V0a@(inj__ty_2Enum_2Enum @ V3delta))) & ( ! [V4t:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V3delta))@(inj__ty_2Enum_2Enum @ V4t))) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V4t))@(inj__ty_2Enum_2Enum @ V2t0)))) => (~ (p@(ap@V1b@(inj__ty_2Enum_2Enum @ V4t)))))))))))))))).
thf(ax_thm_2EPast__Temporal__Logic_2EPWHEN,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_2EPast__Temporal__Logic_2EPWHEN@V0a)@V1b)@(inj__ty_2Enum_2Enum @ V2t0))) <=> (( ! [V3t:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V3t))@(inj__ty_2Enum_2Enum @ V2t0))) => (~ (p@(ap@V1b@(inj__ty_2Enum_2Enum @ V3t)))))) | (? [V4delta:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V4delta))@(inj__ty_2Enum_2Enum @ V2t0))) & ((p@(ap@V0a@(inj__ty_2Enum_2Enum @ V4delta))) & ((p@(ap@V1b@(inj__ty_2Enum_2Enum @ V4delta))) & ( ! [V5t:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V4delta))@(inj__ty_2Enum_2Enum @ V5t))) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V5t))@(inj__ty_2Enum_2Enum @ V2t0)))) => (~ (p@(ap@V1b@(inj__ty_2Enum_2Enum @ V5t)))))))))))))))))).
thf(ax_thm_2EPast__Temporal__Logic_2EPUNTIL,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_2EPast__Temporal__Logic_2EPUNTIL@V0a)@V1b)@(inj__ty_2Enum_2Enum @ V2t0))) <=> (( ! [V3t:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V3t))@(inj__ty_2Enum_2Enum @ V2t0))) => (p@(ap@V0a@(inj__ty_2Enum_2Enum @ V3t))))) | (? [V4delta:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V4delta))@(inj__ty_2Enum_2Enum @ V2t0))) & ((p@(ap@V1b@(inj__ty_2Enum_2Enum @ V4delta))) & ( ! [V5t:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V4delta))@(inj__ty_2Enum_2Enum @ V5t))) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V5t))@(inj__ty_2Enum_2Enum @ V2t0)))) => ((p@(ap@V0a@(inj__ty_2Enum_2Enum @ V5t))) & (~ (p@(ap@V1b@(inj__ty_2Enum_2Enum @ V5t)))))))))))))))))).
thf(ax_thm_2EPast__Temporal__Logic_2EPBEFORE,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_2EPast__Temporal__Logic_2EPBEFORE@V0a)@V1b)@(inj__ty_2Enum_2Enum @ V2t0))) <=> (( ! [V3t:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V3t))@(inj__ty_2Enum_2Enum @ V2t0))) => (~ (p@(ap@V1b@(inj__ty_2Enum_2Enum @ V3t)))))) | (? [V4delta:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V4delta))@(inj__ty_2Enum_2Enum @ V2t0))) & ((p@(ap@V0a@(inj__ty_2Enum_2Enum @ V4delta))) & ( ! [V5t:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V4delta))@(inj__ty_2Enum_2Enum @ V5t))) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V5t))@(inj__ty_2Enum_2Enum @ V2t0)))) => (~ (p@(ap@V1b@(inj__ty_2Enum_2Enum @ V5t))))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2EINITIALISATION,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => (((p@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> $true) & (((p@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V0a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> $false) & (((p@(ap@(ap@c_2EPast__Temporal__Logic_2EPALWAYS@V0a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> (p@(ap@V0a@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & (((p@(ap@(ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V0a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> (p@(ap@V0a@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & (((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@V1b)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> (p@(ap@V1b@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & (((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V0a)@V1b)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> ((p@(ap@V0a@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) & (p@(ap@V1b@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & (((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V0a)@V1b)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> ((p@(ap@V0a@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) & (~~ (p@(ap@V1b@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))) & (((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V0a)@V1b)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> ((p@(ap@V0a@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) | (p@(ap@V1b@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & (((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V0a)@V1b)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> ((p@(ap@V0a@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) | (~~ (p@(ap@V1b@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))) & ((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V0a)@V1b)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> (~~ (p@(ap@V1b@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2ERECURSION,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => (((ap@c_2ETemporal__Logic_2EALWAYS@V0a) = (lam@ty_2Enum_2Enum@(^ [V2t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V2t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@(ap@c_2ETemporal__Logic_2EALWAYS@V0a))@V2t))))) & (((ap@c_2ETemporal__Logic_2EEVENTUAL@V0a) = (lam@ty_2Enum_2Enum@(^ [V3t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V3t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@(ap@c_2ETemporal__Logic_2EEVENTUAL@V0a))@V3t))))) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@c_2Ebool_2E_7E@(ap@V1b@V4t)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V4t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@V1b))@V4t)))))) & (((ap@(ap@c_2ETemporal__Logic_2ESWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@bool)@(ap@V1b@V5t))@(ap@V0a@V5t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2ETemporal__Logic_2ESWHEN@V0a)@V1b))@V5t))))) & (((ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V6t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V1b@V6t)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V6t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V0a)@V1b))@V6t)))))) & (((ap@(ap@c_2ETemporal__Logic_2EUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@c_2Ebool_2E_7E@(ap@V1b@V7t)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V7t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2ETemporal__Logic_2EUNTIL@V0a)@V1b))@V7t)))))) & (((ap@(ap@c_2ETemporal__Logic_2EWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@bool)@(ap@V1b@V8t))@(ap@V0a@V8t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2ETemporal__Logic_2EWHEN@V0a)@V1b))@V8t))))) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V1b@V9t)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V9t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@V1b))@V9t)))))) & (((ap@c_2EPast__Temporal__Logic_2EPALWAYS@V0a) = (lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V10t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@c_2EPast__Temporal__Logic_2EPALWAYS@V0a))@V10t))))) & (((ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V0a) = (lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V11t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@(ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V0a))@V11t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V1b@V12t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V12t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@V1b))@V12t)))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V13t))@(ap@V1b@V13t)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V1b@V13t)))@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V0a)@V1b))@V13t)))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V1b@V14t)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V14t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V0a)@V1b))@V14t)))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V1b@V15t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V15t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V0a)@V1b))@V15t)))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V16t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V16t))@(ap@V1b@V16t)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V1b@V16t)))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V0a)@V1b))@V16t)))))) & ((ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V17t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V1b@V17t)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V17t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V0a)@V1b))@V17t)))))))))))))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2EFIXPOINTS,lemma,( ! [V0y:$i] : ((mem@V0y@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1a:$i] : ((mem@V1a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V2b:$i] : ((mem@V2b@(arr@ty_2Enum_2Enum@bool)) => (((V0y = (lam@ty_2Enum_2Enum@(^ [V3t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1a@V3t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0y)@V3t))))) <=> ((V0y = (ap@c_2ETemporal__Logic_2EALWAYS@V1a)) | (V0y = (lam@ty_2Enum_2Enum@(^ [V4t:$i] : c_2Ebool_2EF))))) & (((V0y = (lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V1a@V5t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0y)@V5t))))) <=> ((V0y = (ap@c_2ETemporal__Logic_2EEVENTUAL@V1a)) | (V0y = (lam@ty_2Enum_2Enum@(^ [V6t:$i] : c_2Ebool_2ET))))) & (((V0y = (lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@c_2Ebool_2E_7E@(ap@V2b@V7t)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1a@V7t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0y)@V7t)))))) <=> ((V0y = (ap@(ap@c_2ETemporal__Logic_2EUNTIL@V1a)@V2b)) | (V0y = (ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V1a)@V2b)))) & (((V0y = (lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@bool)@(ap@V2b@V8t))@(ap@V1a@V8t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0y)@V8t))))) <=> ((V0y = (ap@(ap@c_2ETemporal__Logic_2EWHEN@V1a)@V2b)) | (V0y = (ap@(ap@c_2ETemporal__Logic_2ESWHEN@V1a)@V2b)))) & (((V0y = (lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V2b@V9t)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@V1a@V9t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0y)@V9t)))))) <=> ((V0y = (ap@(ap@c_2ETemporal__Logic_2EBEFORE@V1a)@V2b)) | (V0y = (ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V1a)@V2b)))) & (((V0y = (lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1a@V10t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0y)@V10t))))) <=> (V0y = (ap@c_2EPast__Temporal__Logic_2EPALWAYS@V1a))) & (((V0y = (lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V1a@V11t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V0y)@V11t))))) <=> (V0y = (ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V1a))) & (((V0y = (lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V2b@V12t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1a@V12t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V0y)@V12t)))))) <=> (V0y = (ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V1a)@V2b))) & (((V0y = (lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1a@V13t))@(ap@V2b@V13t)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V2b@V13t)))@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V0y)@V13t)))))) <=> (V0y = (ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V1a)@V2b))) & (((V0y = (lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V2b@V14t)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@V1a@V14t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V0y)@V14t)))))) <=> (V0y = (ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V1a)@V2b))) & (((V0y = (lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V2b@V15t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1a@V15t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0y)@V15t)))))) <=> (V0y = (ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V1a)@V2b))) & (((V0y = (lam@ty_2Enum_2Enum@(^ [V16t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1a@V16t))@(ap@V2b@V16t)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V2b@V16t)))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0y)@V16t)))))) <=> (V0y = (ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V1a)@V2b))) & ((V0y = (lam@ty_2Enum_2Enum@(^ [V17t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V2b@V17t)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@V1a@V17t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0y)@V17t)))))) <=> (V0y = (ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V1a)@V2b)))))))))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2ESUNTIL__EXPRESSIVE,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => (((ap@c_2ETemporal__Logic_2EALWAYS@V0a) = (lam@ty_2Enum_2Enum@(^ [V2t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V3t:$i] : c_2Ebool_2ET)))@(lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V4t)))))@V2t))))) & (((ap@c_2ETemporal__Logic_2EEVENTUAL@V0a) = (lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V6t:$i] : c_2Ebool_2ET)))@V0a)@V5t)))) & (((ap@(ap@c_2ETemporal__Logic_2EUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@c_2Ebool_2E_7E@(ap@V1b@V8t)))))@(lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V9t)))@(ap@c_2Ebool_2E_7E@(ap@V1b@V9t))))))@V7t))))) & (((ap@(ap@c_2ETemporal__Logic_2EWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@c_2Ebool_2E_7E@(ap@V0a@V11t)))@(ap@c_2Ebool_2E_7E@(ap@V1b@V11t))))))@(lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V12t)))@(ap@V1b@V12t)))))@V10t))))) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V14t)))))@V1b)@V13t))))) & (((ap@(ap@c_2ETemporal__Logic_2ESWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V16t:$i] : (ap@c_2Ebool_2E_7E@(ap@V1b@V16t)))))@(lam@ty_2Enum_2Enum@(^ [V17t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V17t))@(ap@V1b@V17t)))))@V15t)))) & ((ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V18t:$i] : (ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V19t:$i] : (ap@c_2Ebool_2E_7E@(ap@V1b@V19t)))))@(lam@ty_2Enum_2Enum@(^ [V20t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V20t))@(ap@c_2Ebool_2E_7E@(ap@V1b@V20t))))))@V18t))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2EUNTIL__EXPRESSIVE,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => (((ap@c_2ETemporal__Logic_2EALWAYS@V0a) = (lam@ty_2Enum_2Enum@(^ [V2t:$i] : (ap@(ap@(ap@c_2ETemporal__Logic_2EUNTIL@V0a)@(lam@ty_2Enum_2Enum@(^ [V3t:$i] : c_2Ebool_2EF)))@V2t)))) & (((ap@c_2ETemporal__Logic_2EEVENTUAL@V0a) = (lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2EUNTIL@(lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V5t)))))@(lam@ty_2Enum_2Enum@(^ [V6t:$i] : c_2Ebool_2EF)))@V4t))))) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2EUNTIL@(lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@c_2Ebool_2E_7E@(ap@V1b@V8t)))))@(lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V9t)))@(ap@c_2Ebool_2E_7E@(ap@V1b@V9t))))))@V7t))))) & (((ap@(ap@c_2ETemporal__Logic_2EWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@(ap@(ap@c_2ETemporal__Logic_2EUNTIL@(lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@c_2Ebool_2E_7E@(ap@V1b@V11t)))))@(lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V12t))@(ap@V1b@V12t)))))@V10t)))) & (((ap@(ap@c_2ETemporal__Logic_2ESWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2EUNTIL@(lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@c_2Ebool_2E_7E@(ap@V0a@V14t)))@(ap@c_2Ebool_2E_7E@(ap@V1b@V14t))))))@(lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V15t)))@(ap@V1b@V15t)))))@V13t))))) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V16t:$i] : (ap@(ap@(ap@c_2ETemporal__Logic_2EUNTIL@(lam@ty_2Enum_2Enum@(^ [V17t:$i] : (ap@c_2Ebool_2E_7E@(ap@V1b@V17t)))))@(lam@ty_2Enum_2Enum@(^ [V18t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V18t))@(ap@c_2Ebool_2E_7E@(ap@V1b@V18t))))))@V16t)))) & ((ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V19t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2EUNTIL@(lam@ty_2Enum_2Enum@(^ [V20t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V20t)))))@V1b)@V19t)))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2EWHEN__EXPRESSIVE,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => (((ap@c_2ETemporal__Logic_2EALWAYS@V0a) = (lam@ty_2Enum_2Enum@(^ [V2t:$i] : (ap@(ap@(ap@c_2ETemporal__Logic_2EWHEN@(lam@ty_2Enum_2Enum@(^ [V3t:$i] : c_2Ebool_2EF)))@(lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V4t)))))@V2t)))) & (((ap@c_2ETemporal__Logic_2EEVENTUAL@V0a) = (lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2EWHEN@(lam@ty_2Enum_2Enum@(^ [V6t:$i] : c_2Ebool_2EF)))@V0a)@V5t))))) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2EWHEN@(lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@c_2Ebool_2E_7E@(ap@V1b@V8t)))))@(lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@V0a@V9t))@(ap@V1b@V9t)))))@V7t))))) & (((ap@(ap@c_2ETemporal__Logic_2EUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@(ap@(ap@c_2ETemporal__Logic_2EWHEN@V1b)@(lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@V0a@V11t))@(ap@V1b@V11t)))))@V10t)))) & (((ap@(ap@c_2ETemporal__Logic_2ESWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2EWHEN@(lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V13t)))))@V1b)@V12t))))) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@(ap@(ap@c_2ETemporal__Logic_2EWHEN@(lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@c_2Ebool_2E_7E@(ap@V1b@V15t)))))@(lam@ty_2Enum_2Enum@(^ [V16t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V16t))@(ap@V1b@V16t)))))@V14t)))) & ((ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V17t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2EWHEN@V1b)@(lam@ty_2Enum_2Enum@(^ [V18t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V18t))@(ap@V1b@V18t)))))@V17t)))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2ESWHEN__EXPRESSIVE,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => (((ap@c_2ETemporal__Logic_2EALWAYS@V0a) = (lam@ty_2Enum_2Enum@(^ [V2t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2ESWHEN@(lam@ty_2Enum_2Enum@(^ [V3t:$i] : c_2Ebool_2ET)))@(lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V4t)))))@V2t))))) & (((ap@c_2ETemporal__Logic_2EEVENTUAL@V0a) = (lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@(ap@(ap@c_2ETemporal__Logic_2ESWHEN@(lam@ty_2Enum_2Enum@(^ [V6t:$i] : c_2Ebool_2ET)))@V0a)@V5t)))) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@(ap@(ap@c_2ETemporal__Logic_2ESWHEN@V1b)@(lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@V0a@V8t))@(ap@V1b@V8t)))))@V7t)))) & (((ap@(ap@c_2ETemporal__Logic_2EUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2ESWHEN@(lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@c_2Ebool_2E_7E@(ap@V1b@V10t)))))@(lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@V0a@V11t))@(ap@V1b@V11t)))))@V9t))))) & (((ap@(ap@c_2ETemporal__Logic_2EWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2ESWHEN@(lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V13t)))))@V1b)@V12t))))) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2ESWHEN@V1b)@(lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V15t))@(ap@V1b@V15t)))))@V14t))))) & ((ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V16t:$i] : (ap@(ap@(ap@c_2ETemporal__Logic_2ESWHEN@(lam@ty_2Enum_2Enum@(^ [V17t:$i] : (ap@c_2Ebool_2E_7E@(ap@V1b@V17t)))))@(lam@ty_2Enum_2Enum@(^ [V18t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V18t))@(ap@V1b@V18t)))))@V16t))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2EBEFORE__EXPRESSIVE,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => (((ap@c_2ETemporal__Logic_2EALWAYS@V0a) = (lam@ty_2Enum_2Enum@(^ [V2t:$i] : (ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V3t:$i] : c_2Ebool_2EF)))@(lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V4t)))))@V2t)))) & (((ap@c_2ETemporal__Logic_2EEVENTUAL@V0a) = (lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V6t:$i] : c_2Ebool_2EF)))@V0a)@V5t))))) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V8t)))))@V1b)@V7t))))) & (((ap@(ap@c_2ETemporal__Logic_2EUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V1b)@(lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V10t)))@(ap@c_2Ebool_2E_7E@(ap@V1b@V10t))))))@V9t)))) & (((ap@(ap@c_2ETemporal__Logic_2ESWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V1b)@(lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V12t))@(ap@V1b@V12t)))))@V11t))))) & (((ap@(ap@c_2ETemporal__Logic_2EWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V14t))@(ap@V1b@V14t)))))@(lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V15t)))@(ap@V1b@V15t)))))@V13t)))) & ((ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V16t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V1b)@(lam@ty_2Enum_2Enum@(^ [V17t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V17t))@(ap@c_2Ebool_2E_7E@(ap@V1b@V17t))))))@V16t)))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2ESBEFORE__EXPRESSIVE,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => (((ap@c_2ETemporal__Logic_2EALWAYS@V0a) = (lam@ty_2Enum_2Enum@(^ [V2t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2ESBEFORE@(lam@ty_2Enum_2Enum@(^ [V3t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V3t)))))@(lam@ty_2Enum_2Enum@(^ [V4t:$i] : c_2Ebool_2EF)))@V2t))))) & (((ap@c_2ETemporal__Logic_2EEVENTUAL@V0a) = (lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@(ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V0a)@(lam@ty_2Enum_2Enum@(^ [V6t:$i] : c_2Ebool_2EF)))@V5t)))) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@(ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V1b)@(lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V8t)))@(ap@c_2Ebool_2E_7E@(ap@V1b@V8t))))))@V7t)))) & (((ap@(ap@c_2ETemporal__Logic_2EUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2ESBEFORE@(lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V10t)))))@V1b)@V9t))))) & (((ap@(ap@c_2ETemporal__Logic_2ESWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@(ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V1b)@(lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V12t)))@(ap@V1b@V12t)))))@V11t)))) & (((ap@(ap@c_2ETemporal__Logic_2EWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V1b)@(lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V14t))@(ap@V1b@V14t)))))@V13t))))) & ((ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V1b)@(lam@ty_2Enum_2Enum@(^ [V16t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V16t))@(ap@c_2Ebool_2E_7E@(ap@V1b@V16t))))))@V15t)))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2EPSUNTIL__EXPRESSIVE,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => (((ap@c_2EPast__Temporal__Logic_2EPALWAYS@V0a) = (lam@ty_2Enum_2Enum@(^ [V2t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V3t:$i] : c_2Ebool_2ET)))@(lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V4t)))))@V2t))))) & (((ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V0a) = (lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V6t:$i] : c_2Ebool_2ET)))@V0a)@V5t)))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@c_2Ebool_2E_7E@(ap@V1b@V8t)))))@(lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V9t)))@(ap@c_2Ebool_2E_7E@(ap@V1b@V9t))))))@V7t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@c_2Ebool_2E_7E@(ap@V0a@V11t)))@(ap@c_2Ebool_2E_7E@(ap@V1b@V11t))))))@(lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V12t)))@(ap@V1b@V12t)))))@V10t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V14t)))))@V1b)@V13t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V16t:$i] : (ap@c_2Ebool_2E_7E@(ap@V1b@V16t)))))@(lam@ty_2Enum_2Enum@(^ [V17t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V17t))@(ap@V1b@V17t)))))@V15t)))) & ((ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V18t:$i] : (ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V19t:$i] : (ap@c_2Ebool_2E_7E@(ap@V1b@V19t)))))@(lam@ty_2Enum_2Enum@(^ [V20t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V20t))@(ap@c_2Ebool_2E_7E@(ap@V1b@V20t))))))@V18t))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2EPUNTIL__EXPRESSIVE,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => (((ap@c_2EPast__Temporal__Logic_2EPALWAYS@V0a) = (lam@ty_2Enum_2Enum@(^ [V2t:$i] : (ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V0a)@(lam@ty_2Enum_2Enum@(^ [V3t:$i] : c_2Ebool_2EF)))@V2t)))) & (((ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V0a) = (lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@(lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V5t)))))@(lam@ty_2Enum_2Enum@(^ [V6t:$i] : c_2Ebool_2EF)))@V4t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@(lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@c_2Ebool_2E_7E@(ap@V1b@V8t)))))@(lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V9t)))@(ap@c_2Ebool_2E_7E@(ap@V1b@V9t))))))@V7t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@(lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@c_2Ebool_2E_7E@(ap@V1b@V11t)))))@(lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V12t))@(ap@V1b@V12t)))))@V10t)))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@(lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@c_2Ebool_2E_7E@(ap@V0a@V14t)))@(ap@c_2Ebool_2E_7E@(ap@V1b@V14t))))))@(lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V15t)))@(ap@V1b@V15t)))))@V13t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V16t:$i] : (ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@(lam@ty_2Enum_2Enum@(^ [V17t:$i] : (ap@c_2Ebool_2E_7E@(ap@V1b@V17t)))))@(lam@ty_2Enum_2Enum@(^ [V18t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V18t))@(ap@c_2Ebool_2E_7E@(ap@V1b@V18t))))))@V16t)))) & ((ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V19t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@(lam@ty_2Enum_2Enum@(^ [V20t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V20t)))))@V1b)@V19t)))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2EPWHEN__EXPRESSIVE,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => (((ap@c_2EPast__Temporal__Logic_2EPALWAYS@V0a) = (lam@ty_2Enum_2Enum@(^ [V2t:$i] : (ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@(lam@ty_2Enum_2Enum@(^ [V3t:$i] : c_2Ebool_2EF)))@(lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V4t)))))@V2t)))) & (((ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V0a) = (lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@(lam@ty_2Enum_2Enum@(^ [V6t:$i] : c_2Ebool_2EF)))@V0a)@V5t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@(lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@c_2Ebool_2E_7E@(ap@V1b@V8t)))))@(lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@V0a@V9t))@(ap@V1b@V9t)))))@V7t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V1b)@(lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@V0a@V11t))@(ap@V1b@V11t)))))@V10t)))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@(lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V13t)))))@V1b)@V12t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@(lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@c_2Ebool_2E_7E@(ap@V1b@V15t)))))@(lam@ty_2Enum_2Enum@(^ [V16t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V16t))@(ap@V1b@V16t)))))@V14t)))) & ((ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V17t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V1b)@(lam@ty_2Enum_2Enum@(^ [V18t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V18t))@(ap@V1b@V18t)))))@V17t)))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2EPSWHEN__EXPRESSIVE,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => (((ap@c_2EPast__Temporal__Logic_2EPALWAYS@V0a) = (lam@ty_2Enum_2Enum@(^ [V2t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@(lam@ty_2Enum_2Enum@(^ [V3t:$i] : c_2Ebool_2ET)))@(lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V4t)))))@V2t))))) & (((ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V0a) = (lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@(lam@ty_2Enum_2Enum@(^ [V6t:$i] : c_2Ebool_2ET)))@V0a)@V5t)))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V1b)@(lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@V0a@V8t))@(ap@V1b@V8t)))))@V7t)))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@(lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@c_2Ebool_2E_7E@(ap@V1b@V10t)))))@(lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@V0a@V11t))@(ap@V1b@V11t)))))@V9t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@(lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V13t)))))@V1b)@V12t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V1b)@(lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V15t))@(ap@V1b@V15t)))))@V14t))))) & ((ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V16t:$i] : (ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@(lam@ty_2Enum_2Enum@(^ [V17t:$i] : (ap@c_2Ebool_2E_7E@(ap@V1b@V17t)))))@(lam@ty_2Enum_2Enum@(^ [V18t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V18t))@(ap@V1b@V18t)))))@V16t))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2EPBEFORE__EXPRESSIVE,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => (((ap@c_2EPast__Temporal__Logic_2EPALWAYS@V0a) = (lam@ty_2Enum_2Enum@(^ [V2t:$i] : (ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@(lam@ty_2Enum_2Enum@(^ [V3t:$i] : c_2Ebool_2EF)))@(lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V4t)))))@V2t)))) & (((ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V0a) = (lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@(lam@ty_2Enum_2Enum@(^ [V6t:$i] : c_2Ebool_2EF)))@V0a)@V5t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@(lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V8t)))))@V1b)@V7t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V1b)@(lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V10t)))@(ap@c_2Ebool_2E_7E@(ap@V1b@V10t))))))@V9t)))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V1b)@(lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V12t))@(ap@V1b@V12t)))))@V11t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@(lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V14t))@(ap@V1b@V14t)))))@(lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V15t)))@(ap@V1b@V15t)))))@V13t)))) & ((ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V16t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V1b)@(lam@ty_2Enum_2Enum@(^ [V17t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V17t))@(ap@c_2Ebool_2E_7E@(ap@V1b@V17t))))))@V16t)))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2EPSBEFORE__EXPRESSIVE,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => (((ap@c_2EPast__Temporal__Logic_2EPALWAYS@V0a) = (lam@ty_2Enum_2Enum@(^ [V2t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@(lam@ty_2Enum_2Enum@(^ [V3t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V3t)))))@(lam@ty_2Enum_2Enum@(^ [V4t:$i] : c_2Ebool_2EF)))@V2t))))) & (((ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V0a) = (lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V0a)@(lam@ty_2Enum_2Enum@(^ [V6t:$i] : c_2Ebool_2EF)))@V5t)))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V1b)@(lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V8t)))@(ap@c_2Ebool_2E_7E@(ap@V1b@V8t))))))@V7t)))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@(lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V10t)))))@V1b)@V9t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V1b)@(lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V12t)))@(ap@V1b@V12t)))))@V11t)))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V1b)@(lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V14t))@(ap@V1b@V14t)))))@V13t))))) & ((ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V0a)@V1b) = (lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V1b)@(lam@ty_2Enum_2Enum@(^ [V16t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V16t))@(ap@c_2Ebool_2E_7E@(ap@V1b@V16t))))))@V15t)))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2ENEGATION__NORMAL__FORM,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1t:tp__ty_2Enum_2Enum] : ( ! [V2b:$i] : ((mem@V2b@(arr@ty_2Enum_2Enum@bool)) => (((~~ (p@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@(inj__ty_2Enum_2Enum @ V1t)))) <=> (p@(ap@(ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V3t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V3t)))))@(inj__ty_2Enum_2Enum @ V1t)))) & (((~~ (p@(ap@(ap@c_2ETemporal__Logic_2EALWAYS@V0a)@(inj__ty_2Enum_2Enum @ V1t)))) <=> (p@(ap@(ap@c_2ETemporal__Logic_2EEVENTUAL@(lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V4t)))))@(inj__ty_2Enum_2Enum @ V1t)))) & (((~~ (p@(ap@(ap@c_2ETemporal__Logic_2EEVENTUAL@V0a)@(inj__ty_2Enum_2Enum @ V1t)))) <=> (p@(ap@(ap@c_2ETemporal__Logic_2EALWAYS@(lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V5t)))))@(inj__ty_2Enum_2Enum @ V1t)))) & (((~~ (p@(ap@(ap@(ap@c_2ETemporal__Logic_2EWHEN@V0a)@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) <=> (p@(ap@(ap@(ap@c_2ETemporal__Logic_2ESWHEN@(lam@ty_2Enum_2Enum@(^ [V6t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V6t)))))@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) & (((~~ (p@(ap@(ap@(ap@c_2ETemporal__Logic_2EUNTIL@V0a)@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) <=> (p@(ap@(ap@(ap@c_2ETemporal__Logic_2ESBEFORE@(lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V7t)))))@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) & (((~~ (p@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) <=> (p@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V8t)))))@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) & (((~~ (p@(ap@(ap@(ap@c_2ETemporal__Logic_2ESWHEN@V0a)@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) <=> (p@(ap@(ap@(ap@c_2ETemporal__Logic_2EWHEN@(lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V9t)))))@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) & (((~~ (p@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) <=> (p@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V10t)))))@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) & (((~~ (p@(ap@(ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V0a)@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) <=> (p@(ap@(ap@(ap@c_2ETemporal__Logic_2EUNTIL@(lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V11t)))))@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) & (((~~ (p@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a)@(inj__ty_2Enum_2Enum @ V1t)))) <=> (p@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@(lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V12t)))))@(inj__ty_2Enum_2Enum @ V1t)))) & (((~~ (p@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V0a)@(inj__ty_2Enum_2Enum @ V1t)))) <=> (p@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@(lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V13t)))))@(inj__ty_2Enum_2Enum @ V1t)))) & (((~~ (p@(ap@(ap@c_2EPast__Temporal__Logic_2EPALWAYS@V0a)@(inj__ty_2Enum_2Enum @ V1t)))) <=> (p@(ap@(ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@(lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V14t)))))@(inj__ty_2Enum_2Enum @ V1t)))) & (((~~ (p@(ap@(ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V0a)@(inj__ty_2Enum_2Enum @ V1t)))) <=> (p@(ap@(ap@c_2EPast__Temporal__Logic_2EPALWAYS@(lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V15t)))))@(inj__ty_2Enum_2Enum @ V1t)))) & (((~~ (p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V0a)@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) <=> (p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@(lam@ty_2Enum_2Enum@(^ [V16t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V16t)))))@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) & (((~~ (p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V0a)@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) <=> (p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@(lam@ty_2Enum_2Enum@(^ [V17t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V17t)))))@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) & (((~~ (p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V0a)@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) <=> (p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V18t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V18t)))))@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) & (((~~ (p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V0a)@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) <=> (p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@(lam@ty_2Enum_2Enum@(^ [V19t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V19t)))))@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) & (((~~ (p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) <=> (p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@(lam@ty_2Enum_2Enum@(^ [V20t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V20t)))))@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) & ((~~ (p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V0a)@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) <=> (p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@(lam@ty_2Enum_2Enum@(^ [V21t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V21t)))))@V2b)@(inj__ty_2Enum_2Enum @ V1t)))))))))))))))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2ECONJUNCTIVE__NORMAL__FORM,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => ( ! [V2c:$i] : ((mem@V2c@(arr@ty_2Enum_2Enum@bool)) => (((ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V3t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V3t))@(ap@V1b@V3t))))) = (lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@V4t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V4t))))) & (((ap@c_2ETemporal__Logic_2EALWAYS@(lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V5t))@(ap@V1b@V5t))))) = (lam@ty_2Enum_2Enum@(^ [V6t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2ETemporal__Logic_2EALWAYS@V0a)@V6t))@(ap@(ap@c_2ETemporal__Logic_2EALWAYS@V1b)@V6t))))) & (((ap@(ap@c_2ETemporal__Logic_2EWHEN@(lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V7t))@(ap@V1b@V7t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2ETemporal__Logic_2EWHEN@V0a)@V2c)@V8t))@(ap@(ap@(ap@c_2ETemporal__Logic_2EWHEN@V1b)@V2c)@V8t))))) & (((ap@(ap@c_2ETemporal__Logic_2ESWHEN@(lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V9t))@(ap@V1b@V9t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2ETemporal__Logic_2ESWHEN@V0a)@V2c)@V10t))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESWHEN@V1b)@V2c)@V10t))))) & (((ap@(ap@c_2ETemporal__Logic_2EUNTIL@(lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V11t))@(ap@V1b@V11t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2ETemporal__Logic_2EUNTIL@V0a)@V2c)@V12t))@(ap@(ap@(ap@c_2ETemporal__Logic_2EUNTIL@V1b)@V2c)@V12t))))) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V13t))@(ap@V1b@V13t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@V2c)@V14t))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V1b)@V2c)@V14t))))) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@V2c)@(lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V15t))@(ap@V1b@V15t))))) = (lam@ty_2Enum_2Enum@(^ [V16t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V2c)@V0a)@V16t))@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V2c)@V1b)@V16t))))) & (((ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V2c)@(lam@ty_2Enum_2Enum@(^ [V17t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V17t))@(ap@V1b@V17t))))) = (lam@ty_2Enum_2Enum@(^ [V18t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V2c)@V0a)@V18t))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V2c)@V1b)@V18t))))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(lam@ty_2Enum_2Enum@(^ [V19t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V19t))@(ap@V1b@V19t))))) = (lam@ty_2Enum_2Enum@(^ [V20t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a)@V20t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V1b)@V20t))))) & (((ap@c_2EPast__Temporal__Logic_2EPSNEXT@(lam@ty_2Enum_2Enum@(^ [V21t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V21t))@(ap@V1b@V21t))))) = (lam@ty_2Enum_2Enum@(^ [V22t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V0a)@V22t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V1b)@V22t))))) & (((ap@c_2EPast__Temporal__Logic_2EPALWAYS@(lam@ty_2Enum_2Enum@(^ [V23t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V23t))@(ap@V1b@V23t))))) = (lam@ty_2Enum_2Enum@(^ [V24t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2EPast__Temporal__Logic_2EPALWAYS@V0a)@V24t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPALWAYS@V1b)@V24t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@(lam@ty_2Enum_2Enum@(^ [V25t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V25t))@(ap@V1b@V25t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V26t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V0a)@V2c)@V26t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V1b)@V2c)@V26t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@(lam@ty_2Enum_2Enum@(^ [V27t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V27t))@(ap@V1b@V27t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V28t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V0a)@V2c)@V28t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V1b)@V2c)@V28t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@(lam@ty_2Enum_2Enum@(^ [V29t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V29t))@(ap@V1b@V29t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V30t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V0a)@V2c)@V30t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V1b)@V2c)@V30t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V31t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V31t))@(ap@V1b@V31t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V32t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@V2c)@V32t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V1b)@V2c)@V32t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V2c)@(lam@ty_2Enum_2Enum@(^ [V33t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V33t))@(ap@V1b@V33t))))) = (lam@ty_2Enum_2Enum@(^ [V34t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V2c)@V0a)@V34t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V2c)@V1b)@V34t))))) & ((ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V2c)@(lam@ty_2Enum_2Enum@(^ [V35t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V35t))@(ap@V1b@V35t))))) = (lam@ty_2Enum_2Enum@(^ [V36t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V2c)@V0a)@V36t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V2c)@V1b)@V36t)))))))))))))))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2EDISJUNCTIVE__NORMAL__FORM,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => ( ! [V2c:$i] : ((mem@V2c@(arr@ty_2Enum_2Enum@bool)) => (((ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V3t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V3t))@(ap@V1b@V3t))))) = (lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@V4t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V4t))))) & (((ap@c_2ETemporal__Logic_2EEVENTUAL@(lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V5t))@(ap@V1b@V5t))))) = (lam@ty_2Enum_2Enum@(^ [V6t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2ETemporal__Logic_2EEVENTUAL@V0a)@V6t))@(ap@(ap@c_2ETemporal__Logic_2EEVENTUAL@V1b)@V6t))))) & (((ap@(ap@c_2ETemporal__Logic_2EWHEN@(lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V7t))@(ap@V1b@V7t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2ETemporal__Logic_2EWHEN@V0a)@V2c)@V8t))@(ap@(ap@(ap@c_2ETemporal__Logic_2EWHEN@V1b)@V2c)@V8t))))) & (((ap@(ap@c_2ETemporal__Logic_2ESWHEN@(lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V9t))@(ap@V1b@V9t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2ETemporal__Logic_2ESWHEN@V0a)@V2c)@V10t))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESWHEN@V1b)@V2c)@V10t))))) & (((ap@(ap@c_2ETemporal__Logic_2EUNTIL@V0a)@(lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V1b@V11t))@(ap@V2c@V11t))))) = (lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2ETemporal__Logic_2EUNTIL@V0a)@V1b)@V12t))@(ap@(ap@(ap@c_2ETemporal__Logic_2EUNTIL@V0a)@V2c)@V12t))))) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@(lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V1b@V13t))@(ap@V2c@V13t))))) = (lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@V1b)@V14t))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@V2c)@V14t))))) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V15t))@(ap@V1b@V15t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V16t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@V2c)@V16t))@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V1b)@V2c)@V16t))))) & (((ap@(ap@c_2ETemporal__Logic_2ESBEFORE@(lam@ty_2Enum_2Enum@(^ [V17t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V17t))@(ap@V1b@V17t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V18t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V0a)@V2c)@V18t))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V1b)@V2c)@V18t))))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(lam@ty_2Enum_2Enum@(^ [V19t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V19t))@(ap@V1b@V19t))))) = (lam@ty_2Enum_2Enum@(^ [V20t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a)@V20t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V1b)@V20t))))) & (((ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@(lam@ty_2Enum_2Enum@(^ [V21t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V21t))@(ap@V1b@V21t))))) = (lam@ty_2Enum_2Enum@(^ [V22t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V0a)@V22t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V1b)@V22t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@(lam@ty_2Enum_2Enum@(^ [V23t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V23t))@(ap@V1b@V23t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V24t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V0a)@V2c)@V24t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V1b)@V2c)@V24t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@(lam@ty_2Enum_2Enum@(^ [V25t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V25t))@(ap@V1b@V25t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V26t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V0a)@V2c)@V26t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V1b)@V2c)@V26t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V0a)@(lam@ty_2Enum_2Enum@(^ [V27t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V1b@V27t))@(ap@V2c@V27t))))) = (lam@ty_2Enum_2Enum@(^ [V28t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V0a)@V1b)@V28t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V0a)@V2c)@V28t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@(lam@ty_2Enum_2Enum@(^ [V29t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V1b@V29t))@(ap@V2c@V29t))))) = (lam@ty_2Enum_2Enum@(^ [V30t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@V1b)@V30t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@V2c)@V30t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@(lam@ty_2Enum_2Enum@(^ [V31t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V31t))@(ap@V1b@V31t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V32t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V0a)@V2c)@V32t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V1b)@V2c)@V32t))))) & ((ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@(lam@ty_2Enum_2Enum@(^ [V33t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V33t))@(ap@V1b@V33t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V34t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V0a)@V2c)@V34t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V1b)@V2c)@V34t))))))))))))))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2EPRENEX__NEXT__NORMAL__FORM,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1t:tp__ty_2Enum_2Enum] : ( ! [V2b:$i] : ((mem@V2b@(arr@ty_2Enum_2Enum@bool)) => (((~~ (p@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@(inj__ty_2Enum_2Enum @ V1t)))) <=> (p@(ap@(ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V3t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V3t)))))@(inj__ty_2Enum_2Enum @ V1t)))) & ((((p@(ap@V0a@(inj__ty_2Enum_2Enum @ V1t))) & (p@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) <=> (p@(ap@(ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a)@V4t))@(ap@V2b@V4t)))))@(inj__ty_2Enum_2Enum @ V1t)))) & ((((p@(ap@V0a@(inj__ty_2Enum_2Enum @ V1t))) | (p@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V2b)@(inj__ty_2Enum_2Enum @ V1t)))) <=> (p@(ap@(ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a)@V5t))@(ap@V2b@V5t)))))@(inj__ty_2Enum_2Enum @ V1t)))) & (((ap@c_2ETemporal__Logic_2EALWAYS@(ap@c_2ETemporal__Logic_2ENEXT@V0a)) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@c_2ETemporal__Logic_2EALWAYS@V0a))) & (((ap@c_2ETemporal__Logic_2EEVENTUAL@(ap@c_2ETemporal__Logic_2ENEXT@V0a)) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@c_2ETemporal__Logic_2EEVENTUAL@V0a))) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@(ap@c_2ETemporal__Logic_2ENEXT@V2b)) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@V2b))) & (((ap@(ap@c_2ETemporal__Logic_2ESWHEN@V0a)@(ap@c_2ETemporal__Logic_2ENEXT@V2b)) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2ETemporal__Logic_2ESWHEN@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@V2b))) & (((ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V0a)@(ap@c_2ETemporal__Logic_2ENEXT@V2b)) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2ETemporal__Logic_2ESBEFORE@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@V2b))) & (((ap@(ap@c_2ETemporal__Logic_2EUNTIL@V0a)@(ap@c_2ETemporal__Logic_2ENEXT@V2b)) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2ETemporal__Logic_2EUNTIL@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@V2b))) & (((ap@(ap@c_2ETemporal__Logic_2EWHEN@V0a)@(ap@c_2ETemporal__Logic_2ENEXT@V2b)) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2ETemporal__Logic_2EWHEN@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@V2b))) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@(ap@c_2ETemporal__Logic_2ENEXT@V2b)) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@V2b))) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(ap@c_2ETemporal__Logic_2ENEXT@V0a))@V2b) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V2b)))) & (((ap@(ap@c_2ETemporal__Logic_2ESWHEN@(ap@c_2ETemporal__Logic_2ENEXT@V0a))@V2b) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2ETemporal__Logic_2ESWHEN@V0a)@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V2b)))) & (((ap@(ap@c_2ETemporal__Logic_2ESBEFORE@(ap@c_2ETemporal__Logic_2ENEXT@V0a))@V2b) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V0a)@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V2b)))) & (((ap@(ap@c_2ETemporal__Logic_2EUNTIL@(ap@c_2ETemporal__Logic_2ENEXT@V0a))@V2b) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2ETemporal__Logic_2EUNTIL@V0a)@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V2b)))) & (((ap@(ap@c_2ETemporal__Logic_2EWHEN@(ap@c_2ETemporal__Logic_2ENEXT@V0a))@V2b) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2ETemporal__Logic_2EWHEN@V0a)@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V2b)))) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@(ap@c_2ETemporal__Logic_2ENEXT@V0a))@V2b) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V2b)))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@c_2ETemporal__Logic_2ENEXT@V0a)) = (lam@ty_2Enum_2Enum@(^ [V6t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@c_2EPast__Temporal__Logic_2EInitPoint@V6t))@(ap@V0a@V6t))))) & (((ap@c_2EPast__Temporal__Logic_2EPSNEXT@(ap@c_2ETemporal__Logic_2ENEXT@V0a)) = (lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@c_2EPast__Temporal__Logic_2EInitPoint@V7t)))@(ap@V0a@V7t))))) & (((ap@c_2EPast__Temporal__Logic_2EPALWAYS@(ap@c_2ETemporal__Logic_2ENEXT@V0a)) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@c_2EPast__Temporal__Logic_2EPALWAYS@(lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@c_2EPast__Temporal__Logic_2EInitPoint@V8t))@(ap@V0a@V8t))))))) & (((ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@(ap@c_2ETemporal__Logic_2ENEXT@V0a)) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@(lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@c_2EPast__Temporal__Logic_2EInitPoint@V9t)))@(ap@V0a@V9t))))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@(ap@c_2ETemporal__Logic_2ENEXT@V2b)) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@(lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@c_2EPast__Temporal__Logic_2EInitPoint@V10t)))@(ap@V2b@V10t))))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V0a)@(ap@c_2ETemporal__Logic_2ENEXT@V2b)) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@(lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@c_2EPast__Temporal__Logic_2EInitPoint@V11t)))@(ap@V2b@V11t))))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V0a)@(ap@c_2ETemporal__Logic_2ENEXT@V2b)) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V0a))@V2b))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V0a)@(ap@c_2ETemporal__Logic_2ENEXT@V2b)) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@V2b))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V0a)@(ap@c_2ETemporal__Logic_2ENEXT@V2b)) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@(lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@c_2EPast__Temporal__Logic_2EInitPoint@V12t)))@(ap@V2b@V12t))))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V0a)@(ap@c_2ETemporal__Logic_2ENEXT@V2b)) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@(lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@c_2EPast__Temporal__Logic_2EInitPoint@V13t)))@(ap@V2b@V13t))))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(ap@c_2ETemporal__Logic_2ENEXT@V0a))@V2b) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V2b)))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@(ap@c_2ETemporal__Logic_2ENEXT@V0a))@V2b) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V0a)@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V2b)))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@(ap@c_2ETemporal__Logic_2ENEXT@V0a))@V2b) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@(lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@c_2EPast__Temporal__Logic_2EInitPoint@V14t)))@(ap@V0a@V14t)))))@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V2b)))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@(ap@c_2ETemporal__Logic_2ENEXT@V0a))@V2b) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@(lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@c_2EPast__Temporal__Logic_2EInitPoint@V15t))@(ap@V0a@V15t)))))@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V2b)))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@(ap@c_2ETemporal__Logic_2ENEXT@V0a))@V2b) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V0a)@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V2b)))) & ((ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@(ap@c_2ETemporal__Logic_2ENEXT@V0a))@V2b) = (ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V0a)@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V2b)))))))))))))))))))))))))))))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2ENEXT__INWARDS__NORMAL__FORM,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => (((ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V2t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V2t))))) = (lam@ty_2Enum_2Enum@(^ [V3t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@V3t))))) & (((ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V4t))@(ap@V1b@V4t))))) = (lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@V5t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V5t))))) & (((ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V6t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V6t))@(ap@V1b@V6t))))) = (lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@V7t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V7t))))) & (((ap@c_2ETemporal__Logic_2ENEXT@(ap@c_2ETemporal__Logic_2EALWAYS@V0a)) = (ap@c_2ETemporal__Logic_2EALWAYS@(ap@c_2ETemporal__Logic_2ENEXT@V0a))) & (((ap@c_2ETemporal__Logic_2ENEXT@(ap@c_2ETemporal__Logic_2EEVENTUAL@V0a)) = (ap@c_2ETemporal__Logic_2EEVENTUAL@(ap@c_2ETemporal__Logic_2ENEXT@V0a))) & (((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))) & (((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))) & (((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))) & (((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))) & (((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))) & (((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))) & (((ap@c_2ETemporal__Logic_2ENEXT@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a)) = V0a) & (((ap@c_2ETemporal__Logic_2ENEXT@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V0a)) = V0a) & (((ap@c_2ETemporal__Logic_2ENEXT@(ap@c_2EPast__Temporal__Logic_2EPALWAYS@V0a)) = (lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2EPast__Temporal__Logic_2EPALWAYS@V0a)@V8t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@V8t))))) & (((ap@c_2ETemporal__Logic_2ENEXT@(ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V0a)) = (lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V0a)@V9t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@V9t))))) & (((ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@V1b)) = (lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V10t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@V10t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@V1b)@V10t)))))) & (((ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V0a)@V1b)) = (lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@bool)@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V11t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@V11t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V0a)@V1b)@V11t))))) & (((ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V0a)@V1b)) = (lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V12t)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@V12t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V0a)@V1b)@V12t)))))) & (((ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V0a)@V1b)) = (lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V13t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@V13t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V0a)@V1b)@V13t)))))) & (((ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V0a)@V1b)) = (lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@bool)@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V14t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@V14t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V0a)@V1b)@V14t))))) & ((ap@c_2ETemporal__Logic_2ENEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V0a)@V1b)) = (lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V15t)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@V15t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V0a)@V1b)@V15t))))))))))))))))))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2EPNEXT__INWARDS__NORMAL__FORM,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(lam@ty_2Enum_2Enum@(^ [V2t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0a@V2t))))) = (lam@ty_2Enum_2Enum@(^ [V3t:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V0a)@V3t))))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V4t))@(ap@V1b@V4t))))) = (lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a)@V5t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V1b)@V5t))))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(lam@ty_2Enum_2Enum@(^ [V6t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V6t))@(ap@V1b@V6t))))) = (lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a)@V7t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V1b)@V7t))))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@c_2ETemporal__Logic_2ENEXT@V0a)) = (lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@c_2EPast__Temporal__Logic_2EInitPoint@V8t))@(ap@V0a@V8t))))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@c_2ETemporal__Logic_2EALWAYS@V0a)) = (lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@c_2EPast__Temporal__Logic_2EInitPoint@V9t))@(ap@(ap@c_2ETemporal__Logic_2EALWAYS@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@V9t))))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@c_2ETemporal__Logic_2EEVENTUAL@V0a)) = (lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@c_2EPast__Temporal__Logic_2EInitPoint@V10t))@(ap@(ap@c_2ETemporal__Logic_2EEVENTUAL@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@V10t))))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@V1b)) = (ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V1b))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@(ap@c_2ETemporal__Logic_2ESWHEN@V0a)@V1b)) = (ap@(ap@c_2ETemporal__Logic_2ESWHEN@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V1b))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V0a)@V1b)) = (ap@(ap@c_2ETemporal__Logic_2ESBEFORE@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V1b))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@(ap@c_2ETemporal__Logic_2EUNTIL@V0a)@V1b)) = (ap@(ap@c_2ETemporal__Logic_2EUNTIL@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V1b))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@(ap@c_2ETemporal__Logic_2EWHEN@V0a)@V1b)) = (ap@(ap@c_2ETemporal__Logic_2EWHEN@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V1b))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@V1b)) = (ap@(ap@c_2ETemporal__Logic_2EBEFORE@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V1b))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@c_2EPast__Temporal__Logic_2EPALWAYS@V0a)) = (ap@c_2EPast__Temporal__Logic_2EPALWAYS@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V0a)) = (lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@c_2EPast__Temporal__Logic_2EInitPoint@V11t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V0a))@V11t))))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@V1b)) = (lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@c_2EPast__Temporal__Logic_2EInitPoint@V12t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V1b))@V12t))))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V0a)@V1b)) = (lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@c_2EPast__Temporal__Logic_2EInitPoint@V13t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V1b))@V13t))))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V0a)@V1b)) = (lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@c_2EPast__Temporal__Logic_2EInitPoint@V14t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V0a))@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V1b))@V14t))))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V0a)@V1b)) = (ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V1b))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V0a)@V1b)) = (ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V1b))) & ((ap@c_2EPast__Temporal__Logic_2EPNEXT@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V0a)@V1b)) = (ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a))@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V1b))))))))))))))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2ESIMPLIFY,lemma,( ! [V0b:$i] : ((mem@V0b@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1a:$i] : ((mem@V1a@(arr@ty_2Enum_2Enum@bool)) => (((ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V2t:$i] : c_2Ebool_2EF))) = (lam@ty_2Enum_2Enum@(^ [V3t:$i] : c_2Ebool_2EF))) & (((ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V4t:$i] : c_2Ebool_2ET))) = (lam@ty_2Enum_2Enum@(^ [V5t:$i] : c_2Ebool_2ET))) & (((ap@c_2ETemporal__Logic_2EALWAYS@(lam@ty_2Enum_2Enum@(^ [V6t:$i] : c_2Ebool_2ET))) = (lam@ty_2Enum_2Enum@(^ [V7t:$i] : c_2Ebool_2ET))) & (((ap@c_2ETemporal__Logic_2EALWAYS@(lam@ty_2Enum_2Enum@(^ [V8t:$i] : c_2Ebool_2EF))) = (lam@ty_2Enum_2Enum@(^ [V9t:$i] : c_2Ebool_2EF))) & (((ap@c_2ETemporal__Logic_2EEVENTUAL@(lam@ty_2Enum_2Enum@(^ [V10t:$i] : c_2Ebool_2ET))) = (lam@ty_2Enum_2Enum@(^ [V11t:$i] : c_2Ebool_2ET))) & (((ap@c_2ETemporal__Logic_2EEVENTUAL@(lam@ty_2Enum_2Enum@(^ [V12t:$i] : c_2Ebool_2EF))) = (lam@ty_2Enum_2Enum@(^ [V13t:$i] : c_2Ebool_2EF))) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V14t:$i] : c_2Ebool_2EF)))@V0b) = V0b) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V15t:$i] : c_2Ebool_2ET)))@V0b) = (ap@c_2ETemporal__Logic_2EEVENTUAL@V0b)) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V1a)@(lam@ty_2Enum_2Enum@(^ [V16t:$i] : c_2Ebool_2EF))) = (lam@ty_2Enum_2Enum@(^ [V17t:$i] : c_2Ebool_2EF))) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V1a)@(lam@ty_2Enum_2Enum@(^ [V18t:$i] : c_2Ebool_2ET))) = (lam@ty_2Enum_2Enum@(^ [V19t:$i] : c_2Ebool_2ET))) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V1a)@V1a) = V1a) & (((ap@(ap@c_2ETemporal__Logic_2EUNTIL@(lam@ty_2Enum_2Enum@(^ [V20t:$i] : c_2Ebool_2EF)))@V0b) = V0b) & (((ap@(ap@c_2ETemporal__Logic_2EUNTIL@(lam@ty_2Enum_2Enum@(^ [V21t:$i] : c_2Ebool_2ET)))@V0b) = (lam@ty_2Enum_2Enum@(^ [V22t:$i] : c_2Ebool_2ET))) & (((ap@(ap@c_2ETemporal__Logic_2EUNTIL@V1a)@(lam@ty_2Enum_2Enum@(^ [V23t:$i] : c_2Ebool_2EF))) = (ap@c_2ETemporal__Logic_2EALWAYS@V1a)) & (((ap@(ap@c_2ETemporal__Logic_2EUNTIL@V1a)@(lam@ty_2Enum_2Enum@(^ [V24t:$i] : c_2Ebool_2ET))) = (lam@ty_2Enum_2Enum@(^ [V25t:$i] : c_2Ebool_2ET))) & (((ap@(ap@c_2ETemporal__Logic_2EUNTIL@V1a)@V1a) = V1a) & (((ap@(ap@c_2ETemporal__Logic_2ESWHEN@(lam@ty_2Enum_2Enum@(^ [V26t:$i] : c_2Ebool_2EF)))@V0b) = (lam@ty_2Enum_2Enum@(^ [V27t:$i] : c_2Ebool_2EF))) & (((ap@(ap@c_2ETemporal__Logic_2ESWHEN@(lam@ty_2Enum_2Enum@(^ [V28t:$i] : c_2Ebool_2ET)))@V0b) = (ap@c_2ETemporal__Logic_2EEVENTUAL@V0b)) & (((ap@(ap@c_2ETemporal__Logic_2ESWHEN@V1a)@(lam@ty_2Enum_2Enum@(^ [V29t:$i] : c_2Ebool_2EF))) = (lam@ty_2Enum_2Enum@(^ [V30t:$i] : c_2Ebool_2EF))) & (((ap@(ap@c_2ETemporal__Logic_2ESWHEN@V1a)@(lam@ty_2Enum_2Enum@(^ [V31t:$i] : c_2Ebool_2ET))) = V1a) & (((ap@(ap@c_2ETemporal__Logic_2ESWHEN@V1a)@V1a) = (ap@c_2ETemporal__Logic_2EEVENTUAL@V1a)) & (((ap@(ap@c_2ETemporal__Logic_2EWHEN@(lam@ty_2Enum_2Enum@(^ [V32t:$i] : c_2Ebool_2EF)))@V0b) = (ap@c_2ETemporal__Logic_2EALWAYS@(lam@ty_2Enum_2Enum@(^ [V33t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0b@V33t)))))) & (((ap@(ap@c_2ETemporal__Logic_2EWHEN@(lam@ty_2Enum_2Enum@(^ [V34t:$i] : c_2Ebool_2ET)))@V0b) = (lam@ty_2Enum_2Enum@(^ [V35t:$i] : c_2Ebool_2ET))) & (((ap@(ap@c_2ETemporal__Logic_2EWHEN@V1a)@(lam@ty_2Enum_2Enum@(^ [V36t:$i] : c_2Ebool_2EF))) = (lam@ty_2Enum_2Enum@(^ [V37t:$i] : c_2Ebool_2ET))) & (((ap@(ap@c_2ETemporal__Logic_2EWHEN@V1a)@(lam@ty_2Enum_2Enum@(^ [V38t:$i] : c_2Ebool_2ET))) = V1a) & (((ap@(ap@c_2ETemporal__Logic_2EWHEN@V1a)@V1a) = (lam@ty_2Enum_2Enum@(^ [V39t:$i] : c_2Ebool_2ET))) & (((ap@(ap@c_2ETemporal__Logic_2ESBEFORE@(lam@ty_2Enum_2Enum@(^ [V40t:$i] : c_2Ebool_2EF)))@V0b) = (lam@ty_2Enum_2Enum@(^ [V41t:$i] : c_2Ebool_2EF))) & (((ap@(ap@c_2ETemporal__Logic_2ESBEFORE@(lam@ty_2Enum_2Enum@(^ [V42t:$i] : c_2Ebool_2ET)))@V0b) = (lam@ty_2Enum_2Enum@(^ [V43t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0b@V43t))))) & (((ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V1a)@(lam@ty_2Enum_2Enum@(^ [V44t:$i] : c_2Ebool_2EF))) = (ap@c_2ETemporal__Logic_2EEVENTUAL@V1a)) & (((ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V1a)@(lam@ty_2Enum_2Enum@(^ [V45t:$i] : c_2Ebool_2ET))) = (lam@ty_2Enum_2Enum@(^ [V46t:$i] : c_2Ebool_2EF))) & (((ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V1a)@V1a) = (lam@ty_2Enum_2Enum@(^ [V47t:$i] : c_2Ebool_2EF))) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V48t:$i] : c_2Ebool_2EF)))@V0b) = (ap@c_2ETemporal__Logic_2EALWAYS@(lam@ty_2Enum_2Enum@(^ [V49t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0b@V49t)))))) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V50t:$i] : c_2Ebool_2ET)))@V0b) = (lam@ty_2Enum_2Enum@(^ [V51t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0b@V51t))))) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@V1a)@(lam@ty_2Enum_2Enum@(^ [V52t:$i] : c_2Ebool_2EF))) = (lam@ty_2Enum_2Enum@(^ [V53t:$i] : c_2Ebool_2ET))) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@V1a)@(lam@ty_2Enum_2Enum@(^ [V54t:$i] : c_2Ebool_2ET))) = (lam@ty_2Enum_2Enum@(^ [V55t:$i] : c_2Ebool_2EF))) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@V1a)@V1a) = (ap@c_2ETemporal__Logic_2EALWAYS@(lam@ty_2Enum_2Enum@(^ [V56t:$i] : (ap@c_2Ebool_2E_7E@(ap@V1a@V56t)))))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(lam@ty_2Enum_2Enum@(^ [V57t:$i] : c_2Ebool_2EF))) = c_2EPast__Temporal__Logic_2EInitPoint) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(lam@ty_2Enum_2Enum@(^ [V58t:$i] : c_2Ebool_2ET))) = (lam@ty_2Enum_2Enum@(^ [V59t:$i] : c_2Ebool_2ET))) & (((ap@c_2EPast__Temporal__Logic_2EPSNEXT@(lam@ty_2Enum_2Enum@(^ [V60t:$i] : c_2Ebool_2EF))) = (lam@ty_2Enum_2Enum@(^ [V61t:$i] : c_2Ebool_2EF))) & (((ap@c_2EPast__Temporal__Logic_2EPSNEXT@(lam@ty_2Enum_2Enum@(^ [V62t:$i] : c_2Ebool_2ET))) = (lam@ty_2Enum_2Enum@(^ [V63t:$i] : (ap@c_2Ebool_2E_7E@(ap@c_2EPast__Temporal__Logic_2EInitPoint@V63t))))) & (((ap@c_2EPast__Temporal__Logic_2EPALWAYS@(lam@ty_2Enum_2Enum@(^ [V64t:$i] : c_2Ebool_2ET))) = (lam@ty_2Enum_2Enum@(^ [V65t:$i] : c_2Ebool_2ET))) & (((ap@c_2EPast__Temporal__Logic_2EPALWAYS@(lam@ty_2Enum_2Enum@(^ [V66t:$i] : c_2Ebool_2EF))) = (lam@ty_2Enum_2Enum@(^ [V67t:$i] : c_2Ebool_2EF))) & (((ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@(lam@ty_2Enum_2Enum@(^ [V68t:$i] : c_2Ebool_2ET))) = (lam@ty_2Enum_2Enum@(^ [V69t:$i] : c_2Ebool_2ET))) & (((ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@(lam@ty_2Enum_2Enum@(^ [V70t:$i] : c_2Ebool_2EF))) = (lam@ty_2Enum_2Enum@(^ [V71t:$i] : c_2Ebool_2EF))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V72t:$i] : c_2Ebool_2EF)))@V0b) = V0b) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V73t:$i] : c_2Ebool_2ET)))@V0b) = (ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V0b)) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V1a)@(lam@ty_2Enum_2Enum@(^ [V74t:$i] : c_2Ebool_2EF))) = (lam@ty_2Enum_2Enum@(^ [V75t:$i] : c_2Ebool_2EF))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V1a)@(lam@ty_2Enum_2Enum@(^ [V76t:$i] : c_2Ebool_2ET))) = (lam@ty_2Enum_2Enum@(^ [V77t:$i] : c_2Ebool_2ET))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V1a)@V1a) = V1a) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@(lam@ty_2Enum_2Enum@(^ [V78t:$i] : c_2Ebool_2EF)))@V0b) = V0b) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@(lam@ty_2Enum_2Enum@(^ [V79t:$i] : c_2Ebool_2ET)))@V0b) = (lam@ty_2Enum_2Enum@(^ [V80t:$i] : c_2Ebool_2ET))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V1a)@(lam@ty_2Enum_2Enum@(^ [V81t:$i] : c_2Ebool_2EF))) = (ap@c_2EPast__Temporal__Logic_2EPALWAYS@V1a)) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V1a)@(lam@ty_2Enum_2Enum@(^ [V82t:$i] : c_2Ebool_2ET))) = (lam@ty_2Enum_2Enum@(^ [V83t:$i] : c_2Ebool_2ET))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V1a)@V1a) = V1a) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@(lam@ty_2Enum_2Enum@(^ [V84t:$i] : c_2Ebool_2EF)))@V0b) = (lam@ty_2Enum_2Enum@(^ [V85t:$i] : c_2Ebool_2EF))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@(lam@ty_2Enum_2Enum@(^ [V86t:$i] : c_2Ebool_2ET)))@V0b) = (ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V0b)) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V1a)@(lam@ty_2Enum_2Enum@(^ [V87t:$i] : c_2Ebool_2EF))) = (lam@ty_2Enum_2Enum@(^ [V88t:$i] : c_2Ebool_2EF))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V1a)@(lam@ty_2Enum_2Enum@(^ [V89t:$i] : c_2Ebool_2ET))) = V1a) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V1a)@V1a) = (ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V1a)) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@(lam@ty_2Enum_2Enum@(^ [V90t:$i] : c_2Ebool_2EF)))@V0b) = (ap@c_2EPast__Temporal__Logic_2EPALWAYS@(lam@ty_2Enum_2Enum@(^ [V91t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0b@V91t)))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@(lam@ty_2Enum_2Enum@(^ [V92t:$i] : c_2Ebool_2ET)))@V0b) = (lam@ty_2Enum_2Enum@(^ [V93t:$i] : c_2Ebool_2ET))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V1a)@(lam@ty_2Enum_2Enum@(^ [V94t:$i] : c_2Ebool_2EF))) = (lam@ty_2Enum_2Enum@(^ [V95t:$i] : c_2Ebool_2ET))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V1a)@(lam@ty_2Enum_2Enum@(^ [V96t:$i] : c_2Ebool_2ET))) = V1a) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V1a)@V1a) = (lam@ty_2Enum_2Enum@(^ [V97t:$i] : c_2Ebool_2ET))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@(lam@ty_2Enum_2Enum@(^ [V98t:$i] : c_2Ebool_2EF)))@V0b) = (lam@ty_2Enum_2Enum@(^ [V99t:$i] : c_2Ebool_2EF))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@(lam@ty_2Enum_2Enum@(^ [V100t:$i] : c_2Ebool_2ET)))@V0b) = (lam@ty_2Enum_2Enum@(^ [V101t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0b@V101t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V1a)@(lam@ty_2Enum_2Enum@(^ [V102t:$i] : c_2Ebool_2EF))) = (ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V1a)) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V1a)@(lam@ty_2Enum_2Enum@(^ [V103t:$i] : c_2Ebool_2ET))) = (lam@ty_2Enum_2Enum@(^ [V104t:$i] : c_2Ebool_2EF))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V1a)@V1a) = (lam@ty_2Enum_2Enum@(^ [V105t:$i] : c_2Ebool_2EF))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@(lam@ty_2Enum_2Enum@(^ [V106t:$i] : c_2Ebool_2EF)))@V0b) = (ap@c_2EPast__Temporal__Logic_2EPALWAYS@(lam@ty_2Enum_2Enum@(^ [V107t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0b@V107t)))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@(lam@ty_2Enum_2Enum@(^ [V108t:$i] : c_2Ebool_2ET)))@V0b) = (lam@ty_2Enum_2Enum@(^ [V109t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0b@V109t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V1a)@(lam@ty_2Enum_2Enum@(^ [V110t:$i] : c_2Ebool_2EF))) = (lam@ty_2Enum_2Enum@(^ [V111t:$i] : c_2Ebool_2ET))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V1a)@(lam@ty_2Enum_2Enum@(^ [V112t:$i] : c_2Ebool_2ET))) = (lam@ty_2Enum_2Enum@(^ [V113t:$i] : c_2Ebool_2EF))) & ((ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V1a)@V1a) = (ap@c_2EPast__Temporal__Logic_2EPALWAYS@(lam@ty_2Enum_2Enum@(^ [V114t:$i] : (ap@c_2Ebool_2E_7E@(ap@V1a@V114t)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
thf(conj_thm_2EPast__Temporal__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@(lam@ty_2Enum_2Enum@(^ [V2t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V2t))@(ap@V1b@V2t)))))@V1b)) & (((ap@(ap@c_2ETemporal__Logic_2EUNTIL@V0a)@V1b) = (ap@(ap@c_2ETemporal__Logic_2EUNTIL@(lam@ty_2Enum_2Enum@(^ [V3t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V3t))@(ap@c_2Ebool_2E_7E@(ap@V1b@V3t))))))@V1b)) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@V1b) = (ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V4t))@(ap@c_2Ebool_2E_7E@(ap@V1b@V4t))))))@V1b)) & (((ap@(ap@c_2ETemporal__Logic_2ESWHEN@V0a)@V1b) = (ap@(ap@c_2ETemporal__Logic_2ESWHEN@(lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V5t))@(ap@V1b@V5t)))))@V1b)) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@V1b) = (ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V6t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V6t))@(ap@c_2Ebool_2E_7E@(ap@V1b@V6t))))))@V1b)) & (((ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V0a)@V1b) = (ap@(ap@c_2ETemporal__Logic_2ESBEFORE@(lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V7t))@(ap@c_2Ebool_2E_7E@(ap@V1b@V7t))))))@V1b)) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V0a)@V1b) = (ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@(lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V8t))@(ap@V1b@V8t)))))@V1b)) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V0a)@V1b) = (ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@(lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V9t))@(ap@c_2Ebool_2E_7E@(ap@V1b@V9t))))))@V1b)) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V0a)@V1b) = (ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@(lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V10t))@(ap@c_2Ebool_2E_7E@(ap@V1b@V10t))))))@V1b)) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V0a)@V1b) = (ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@(lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V11t))@(ap@V1b@V11t)))))@V1b)) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@V1b) = (ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V12t))@(ap@c_2Ebool_2E_7E@(ap@V1b@V12t))))))@V1b)) & ((ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V0a)@V1b) = (ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@(lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V13t))@(ap@c_2Ebool_2E_7E@(ap@V1b@V13t))))))@V1b)))))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2EIMMEDIATE__EVENT,lemma,( ! [V0b:$i] : ((mem@V0b@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1t:tp__ty_2Enum_2Enum] : ( ! [V2a:$i] : ((mem@V2a@(arr@ty_2Enum_2Enum@bool)) => ((p@(ap@V0b@(inj__ty_2Enum_2Enum @ V1t))) => (((p@(ap@(ap@(ap@c_2ETemporal__Logic_2EWHEN@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t))) <=> (p@(ap@V2a@(inj__ty_2Enum_2Enum @ V1t)))) & (((p@(ap@(ap@(ap@c_2ETemporal__Logic_2EUNTIL@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t))) <=> $true) & (((p@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t))) <=> $false) & (((p@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0b)@V2a)@(inj__ty_2Enum_2Enum @ V1t))) <=> (~~ (p@(ap@V2a@(inj__ty_2Enum_2Enum @ V1t))))) & (((p@(ap@(ap@(ap@c_2ETemporal__Logic_2ESWHEN@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t))) <=> (p@(ap@V2a@(inj__ty_2Enum_2Enum @ V1t)))) & (((p@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t))) <=> $true) & (((p@(ap@(ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t))) <=> $false) & (((p@(ap@(ap@(ap@c_2ETemporal__Logic_2ESBEFORE@V0b)@V2a)@(inj__ty_2Enum_2Enum @ V1t))) <=> (~~ (p@(ap@V2a@(inj__ty_2Enum_2Enum @ V1t))))) & (((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t))) <=> (p@(ap@V2a@(inj__ty_2Enum_2Enum @ V1t)))) & (((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t))) <=> $true) & (((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t))) <=> $false) & (((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V0b)@V2a)@(inj__ty_2Enum_2Enum @ V1t))) <=> (~~ (p@(ap@V2a@(inj__ty_2Enum_2Enum @ V1t))))) & (((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t))) <=> (p@(ap@V2a@(inj__ty_2Enum_2Enum @ V1t)))) & (((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t))) <=> $true) & (((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t))) <=> $false) & ((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V0b)@V2a)@(inj__ty_2Enum_2Enum @ V1t))) <=> (~~ (p@(ap@V2a@(inj__ty_2Enum_2Enum @ V1t))))))))))))))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2ENO__FUTURE__EVENT,lemma,( ! [V0b:$i] : ((mem@V0b@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1t0:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2ETemporal__Logic_2EALWAYS@(lam@ty_2Enum_2Enum@(^ [V2t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0b@V2t)))))@(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)))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2ENO__PAST__EVENT,lemma,( ! [V0b:$i] : ((mem@V0b@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1t:tp__ty_2Enum_2Enum] : ( ! [V2a:$i] : ((mem@V2a@(arr@ty_2Enum_2Enum@bool)) => ((p@(ap@(ap@c_2EPast__Temporal__Logic_2EPALWAYS@(lam@ty_2Enum_2Enum@(^ [V3t:$i] : (ap@c_2Ebool_2E_7E@(ap@V0b@V3t)))))@(inj__ty_2Enum_2Enum @ V1t))) => (((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t))) <=> $true) & (((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t))) <=> (p@(ap@(ap@c_2EPast__Temporal__Logic_2EPALWAYS@V2a)@(inj__ty_2Enum_2Enum @ V1t)))) & (((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t))) <=> $true) & (((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V0b)@V2a)@(inj__ty_2Enum_2Enum @ V1t))) <=> (p@(ap@(ap@c_2EPast__Temporal__Logic_2EPALWAYS@(lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@c_2Ebool_2E_7E@(ap@V2a@V4t)))))@(inj__ty_2Enum_2Enum @ V1t)))) & (((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t))) <=> $false) & (((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t))) <=> $false) & (((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t))) <=> (p@(ap@(ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V2a)@(inj__ty_2Enum_2Enum @ V1t)))) & ((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V0b)@V2a)@(inj__ty_2Enum_2Enum @ V1t))) <=> $false))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2ESOME__FUTURE__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))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2ESOME__PAST__EVENT,lemma,( ! [V0b:$i] : ((mem@V0b@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1t:tp__ty_2Enum_2Enum] : ( ! [V2a:$i] : ((mem@V2a@(arr@ty_2Enum_2Enum@bool)) => ((p@(ap@(ap@c_2EPast__Temporal__Logic_2EPEVENTUAL@V0b)@(inj__ty_2Enum_2Enum @ V1t))) => (((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPWHEN@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t))) <=> (p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSWHEN@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t)))) & (((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPUNTIL@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t))) <=> (p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t)))) & (((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t))) <=> (p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V2a)@V0b)@(inj__ty_2Enum_2Enum @ V1t)))) & ((p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V0b)@V2a)@(inj__ty_2Enum_2Enum @ V1t))) <=> (p@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSBEFORE@V0b)@V2a)@(inj__ty_2Enum_2Enum @ V1t)))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2ESEPARATE__NEXT__THM,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => ( ! [V2c:$i] : ((mem@V2c@(arr@ty_2Enum_2Enum@bool)) => (((ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V3t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V3t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V1b)@V3t))))) = (lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V4t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@V4t))))) & (((ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V5t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V1b)@V5t))))) = (lam@ty_2Enum_2Enum@(^ [V6t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V6t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@V6t))))) & (((ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V7t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V1b)@V2c)@V7t))))) = (lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V9t))@(ap@V2c@V9t)))))@V8t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V1b)@V2c)@V8t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V10t))@(ap@V1b@V10t)))))@V8t)))))) & (((ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V11t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V1b)@V2c)@V11t))))) = (lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V13t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V13t))@(ap@c_2Ebool_2E_7E@(ap@V2c@V13t)))))))@V12t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V1b)@V2c)@V12t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V14t))@(ap@c_2Ebool_2E_7E@(ap@V2c@V14t))))))@V12t)))))) & (((ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V15t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V1b)@V15t))))) = (lam@ty_2Enum_2Enum@(^ [V16t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V1b@V16t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@V16t))))) & (((ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V17t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V17t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V1b)@V17t))))) = (lam@ty_2Enum_2Enum@(^ [V18t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V1b@V18t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@V18t))))) & (((ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V19t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V19t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V1b)@V2c)@V19t))))) = (lam@ty_2Enum_2Enum@(^ [V20t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V21t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V21t))@(ap@V2c@V21t)))))@V20t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V1b)@V2c)@V20t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V20t)))))) & ((ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V22t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V22t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V1b)@V2c)@V22t))))) = (lam@ty_2Enum_2Enum@(^ [V23t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V24t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V24t))@(ap@c_2Ebool_2E_7E@(ap@V2c@V24t))))))@V23t))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V1b)@V2c)@V23t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@(lam@ty_2Enum_2Enum@(^ [V25t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V25t))@(ap@V1b@V25t)))))@V23t)))))))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2ESEPARATE__SUNTIL__THM,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => ( ! [V2c:$i] : ((mem@V2c@(arr@ty_2Enum_2Enum@bool)) => ( ! [V3d:$i] : ((mem@V3d@(arr@ty_2Enum_2Enum@bool)) => (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@(lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V1b@V4t))@(ap@V2c@V4t))))) = (lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@V1b)@V5t))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@V2c)@V5t))))) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@(lam@ty_2Enum_2Enum@(^ [V6t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V6t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V2c)@V6t))))) = (lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V7t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V2c)@V7t)))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@(lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V8t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V2c@V8t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V8t))))))@V7t))))) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@(lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V9t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V2c)@V9t))))) = (lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V10t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V2c)@V10t)))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@(lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V11t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V2c@V11t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V11t))))))@V10t))))) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@(lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V12t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V2c)@V3d)@V12t))))) = (lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V2c)@V3d)@V13t))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V14t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V2c)@V14t)))))@V1b)@V13t)))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@(lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V3d@V15t))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V16t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V16t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V2c)@V16t)))))@V1b)@V15t)))))@V13t))))) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@(lam@ty_2Enum_2Enum@(^ [V17t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V17t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V2c)@V3d)@V17t))))) = (lam@ty_2Enum_2Enum@(^ [V18t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V2c)@V3d)@V18t))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V19t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V19t))@(ap@c_2Ebool_2E_7E@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V3d)@V19t))))))@V1b)@V18t)))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@(lam@ty_2Enum_2Enum@(^ [V20t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V2c@V20t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V3d@V20t)))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V21t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V21t))@(ap@c_2Ebool_2E_7E@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V3d)@V21t))))))@V1b)@V20t))))))@V18t))))) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V22t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V22t))@(ap@V1b@V22t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V23t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V0a)@V2c)@V23t))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V1b)@V2c)@V23t))))) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V24t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V24t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V1b)@V24t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V25t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V2c@V25t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V25t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V1b)@V25t)))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V26t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V1b@V26t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@V26t)))))@(ap@c_2ETemporal__Logic_2ENEXT@V2c))@V25t)))))) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V27t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V27t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V1b)@V27t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V28t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V2c@V28t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V28t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V1b)@V28t)))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V29t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V1b@V29t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@V29t)))))@(ap@c_2ETemporal__Logic_2ENEXT@V2c))@V28t)))))) & (((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V30t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V30t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V1b)@V2c)@V30t)))))@V3d) = (lam@ty_2Enum_2Enum@(^ [V31t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V1b)@V2c)@V31t))@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V32t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V3d@V32t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V2c)@V32t)))))@(lam@ty_2Enum_2Enum@(^ [V33t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V33t)))@(ap@c_2Ebool_2E_7E@(ap@V3d@V33t))))))@V31t)))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V34t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V1b@V34t))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@V2c@V34t))@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V35t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V3d@V35t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V2c)@V35t)))))@(lam@ty_2Enum_2Enum@(^ [V36t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V36t)))@(ap@c_2Ebool_2E_7E@(ap@V3d@V36t))))))@V34t))))))@V3d)@V31t))))) & ((ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V37t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V37t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V1b)@V2c)@V37t)))))@V3d) = (lam@ty_2Enum_2Enum@(^ [V38t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V1b)@V2c)@V38t))@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V39t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V3d@V39t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V39t)))))@(lam@ty_2Enum_2Enum@(^ [V40t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V40t)))@(ap@c_2Ebool_2E_7E@(ap@V3d@V40t))))))@V38t)))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V41t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@c_2Ebool_2E_7E@(ap@V2c@V41t)))@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V42t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V3d@V42t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V42t)))))@(lam@ty_2Enum_2Enum@(^ [V43t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V43t)))@(ap@c_2Ebool_2E_7E@(ap@V3d@V43t))))))@V41t)))))@V3d)@V38t))))))))))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2ESEPARATE__BEFORE__THM,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => ( ! [V2c:$i] : ((mem@V2c@(arr@ty_2Enum_2Enum@bool)) => ( ! [V3d:$i] : ((mem@V3d@(arr@ty_2Enum_2Enum@bool)) => (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@(lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V1b@V4t))@(ap@V2c@V4t))))) = (lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@V1b)@V5t))@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@V2c)@V5t))))) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V6t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V6t))@(ap@V1b@V6t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@V2c)@V7t))@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V1b)@V2c)@V7t))))) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@(lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V8t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V2c)@V8t))))) = (lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V9t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V2c)@V9t))))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V9t))@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@(ap@c_2ETemporal__Logic_2ENEXT@V0a))@(lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V2c@V10t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V10t)))))@V9t)))))) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@(lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V11t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V2c)@V11t))))) = (lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V12t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V2c)@V12t))))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V12t))@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@(ap@c_2ETemporal__Logic_2ENEXT@V0a))@(lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V2c@V13t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V13t)))))@V12t)))))) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@(lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V14t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V2c)@V3d)@V14t))))) = (lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@(lam@ty_2Enum_2Enum@(^ [V16t:$i] : (ap@c_2Ebool_2E_7E@(ap@V2c@V16t)))))@V3d)@V15t))@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V17t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V17t))@(ap@c_2Ebool_2E_7E@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V2c)@V17t))))))@V1b)@V15t)))@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@(lam@ty_2Enum_2Enum@(^ [V18t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V3d@V18t))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V19t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V19t)))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V2c)@V19t)))))@V1b)@V18t)))))@V15t))))) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@(lam@ty_2Enum_2Enum@(^ [V20t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V20t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V2c)@V3d)@V20t))))) = (lam@ty_2Enum_2Enum@(^ [V21t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V22t:$i] : (ap@c_2Ebool_2E_7E@(ap@V2c@V22t)))))@V3d)@V21t))@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V23t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V23t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V3d)@V23t)))))@V1b)@V21t)))@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V0a)@(lam@ty_2Enum_2Enum@(^ [V24t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V2c@V24t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V3d@V24t)))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V25t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V25t)))@(ap@c_2Ebool_2E_7E@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V3d)@V25t))))))@V1b)@V24t))))))@V21t))))) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V26t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V26t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V1b)@V26t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V27t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V2c@V27t)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V27t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V1b)@V27t))))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V2c@V27t)))@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V28t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V28t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@V28t)))))@(ap@c_2ETemporal__Logic_2ENEXT@V2c))@V27t)))))) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V29t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V29t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V1b)@V29t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V30t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V2c@V30t)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V30t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V1b)@V30t))))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V2c@V30t)))@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V31t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V31t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V0a)@V31t)))))@(ap@c_2ETemporal__Logic_2ENEXT@V2c))@V30t)))))) & (((ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V32t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V32t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V1b)@V2c)@V32t)))))@V3d) = (lam@ty_2Enum_2Enum@(^ [V33t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@V1b)@V2c)@V33t))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V34t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V3d@V34t)))@(ap@c_2Ebool_2E_7E@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V2c)@V34t))))))@(lam@ty_2Enum_2Enum@(^ [V35t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V35t))@(ap@c_2Ebool_2E_7E@(ap@V3d@V35t))))))@V33t)))@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V36t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V36t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V2c@V36t)))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V37t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V3d@V37t)))@(ap@c_2Ebool_2E_7E@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V2c)@V37t))))))@(lam@ty_2Enum_2Enum@(^ [V38t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V38t))@(ap@c_2Ebool_2E_7E@(ap@V3d@V38t))))))@V36t))))))@V3d)@V33t))))) & ((ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V39t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V39t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V1b)@V2c)@V39t)))))@V3d) = (lam@ty_2Enum_2Enum@(^ [V40t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V1b)@V2c)@V40t))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V41t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V3d@V41t)))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V41t)))))@(lam@ty_2Enum_2Enum@(^ [V42t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V42t))@(ap@c_2Ebool_2E_7E@(ap@V3d@V42t))))))@V40t)))@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@(lam@ty_2Enum_2Enum@(^ [V43t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V2c@V43t))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@(lam@ty_2Enum_2Enum@(^ [V44t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V3d@V44t)))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V44t)))))@(lam@ty_2Enum_2Enum@(^ [V45t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V45t))@(ap@c_2Ebool_2E_7E@(ap@V3d@V45t))))))@V43t)))))@V3d)@V40t))))))))))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2ESEPARATE__PNEXT__THM,lemma,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => ( ! [V2c:$i] : ((mem@V2c@(arr@ty_2Enum_2Enum@bool)) => (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(lam@ty_2Enum_2Enum@(^ [V3t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V3t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V3t))))) = (lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@c_2EPast__Temporal__Logic_2EInitPoint@V4t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V4t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a)@V4t)))))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V5t))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V1b)@V2c)@V5t))))) = (lam@ty_2Enum_2Enum@(^ [V6t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@(lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V7t))@(ap@V2c@V7t)))))@V6t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V1b)@V2c)@V6t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@(lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V8t))@(ap@V1b@V8t)))))@V6t)))))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V9t))@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V1b)@V2c)@V9t))))) = (lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@(lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V11t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V11t))@(ap@c_2Ebool_2E_7E@(ap@V2c@V11t)))))))@V10t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V1b)@V2c)@V10t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@(lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V12t))@(ap@c_2Ebool_2E_7E@(ap@V2c@V12t))))))@V10t)))))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V13t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V13t))))) = (lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V1b@V14t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a)@V14t))))) & (((ap@c_2EPast__Temporal__Logic_2EPNEXT@(lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V15t))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V1b)@V2c)@V15t))))) = (lam@ty_2Enum_2Enum@(^ [V16t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@(lam@ty_2Enum_2Enum@(^ [V17t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V17t))@(ap@V2c@V17t)))))@V16t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V1b)@V2c)@V16t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V1b)@V16t)))))) & ((ap@c_2EPast__Temporal__Logic_2EPNEXT@(lam@ty_2Enum_2Enum@(^ [V18t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V18t))@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V1b)@V2c)@V18t))))) = (lam@ty_2Enum_2Enum@(^ [V19t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@(lam@ty_2Enum_2Enum@(^ [V20t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V20t))@(ap@c_2Ebool_2E_7E@(ap@V2c@V20t))))))@V19t))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V1b)@V2c)@V19t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@(lam@ty_2Enum_2Enum@(^ [V21t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V21t))@(ap@V1b@V21t)))))@V19t)))))))))))))))))).
thf(conj_thm_2EPast__Temporal__Logic_2ESEPARATE__PSUNTIL__THM,conjecture,( ! [V0a:$i] : ((mem@V0a@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@ty_2Enum_2Enum@bool)) => ( ! [V2c:$i] : ((mem@V2c@(arr@ty_2Enum_2Enum@bool)) => ( ! [V3d:$i] : ((mem@V3d@(arr@ty_2Enum_2Enum@bool)) => (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@(lam@ty_2Enum_2Enum@(^ [V4t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V1b@V4t))@(ap@V2c@V4t))))) = (lam@ty_2Enum_2Enum@(^ [V5t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@V1b)@V5t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@V2c)@V5t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@(lam@ty_2Enum_2Enum@(^ [V6t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V6t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V2c)@V6t))))) = (lam@ty_2Enum_2Enum@(^ [V7t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V7t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V2c)@V7t)))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@(lam@ty_2Enum_2Enum@(^ [V8t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V8t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V2c@V8t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V1b)@V8t))))))@V7t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@(lam@ty_2Enum_2Enum@(^ [V9t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V9t))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V2c)@V3d)@V9t))))) = (lam@ty_2Enum_2Enum@(^ [V10t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V2c)@V3d)@V10t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V11t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V11t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V2c)@V11t)))))@V1b)@V10t)))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@(lam@ty_2Enum_2Enum@(^ [V12t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V3d@V12t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V13t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V13t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V2c)@V13t)))))@V1b)@V12t)))))@V10t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@(lam@ty_2Enum_2Enum@(^ [V14t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1b@V14t))@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V2c)@V3d)@V14t))))) = (lam@ty_2Enum_2Enum@(^ [V15t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V2c)@V3d)@V15t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V16t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V16t))@(ap@c_2Ebool_2E_7E@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V3d)@V16t))))))@V1b)@V15t)))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@(lam@ty_2Enum_2Enum@(^ [V17t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V2c@V17t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V3d@V17t)))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V18t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V18t))@(ap@c_2Ebool_2E_7E@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V3d)@V18t))))))@V1b)@V17t))))))@V15t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V19t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0a@V19t))@(ap@V1b@V19t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V20t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V0a)@V2c)@V20t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@V1b)@V2c)@V20t))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V21t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V21t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V21t)))))@V2c) = (lam@ty_2Enum_2Enum@(^ [V22t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V2c@V22t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V22t))@(ap@(ap@c_2ETemporal__Logic_2ENEXT@V1b)@V22t)))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V23t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V1b@V23t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V0a)@V23t)))))@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V2c))@V22t)))))) & (((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V24t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V24t))@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V1b)@V2c)@V24t)))))@V3d) = (lam@ty_2Enum_2Enum@(^ [V25t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2ETemporal__Logic_2ESUNTIL@V1b)@V2c)@V25t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@(lam@ty_2Enum_2Enum@(^ [V26t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V3d@V26t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V2c)@V26t)))))@(lam@ty_2Enum_2Enum@(^ [V27t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V27t)))@(ap@c_2Ebool_2E_7E@(ap@V3d@V27t))))))@V25t)))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V28t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V1b@V28t))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@V2c@V28t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@(lam@ty_2Enum_2Enum@(^ [V29t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V3d@V29t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPNEXT@V2c)@V29t)))))@(lam@ty_2Enum_2Enum@(^ [V30t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V30t)))@(ap@c_2Ebool_2E_7E@(ap@V3d@V30t))))))@V28t))))))@V3d)@V25t))))) & ((ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V31t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0a@V31t))@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V1b)@V2c)@V31t)))))@V3d) = (lam@ty_2Enum_2Enum@(^ [V32t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(ap@c_2ETemporal__Logic_2EBEFORE@V1b)@V2c)@V32t))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@(lam@ty_2Enum_2Enum@(^ [V33t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V3d@V33t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V1b)@V33t)))))@(lam@ty_2Enum_2Enum@(^ [V34t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V34t)))@(ap@c_2Ebool_2E_7E@(ap@V3d@V34t))))))@V32t)))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPSUNTIL@(lam@ty_2Enum_2Enum@(^ [V35t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@c_2Ebool_2E_7E@(ap@V2c@V35t)))@(ap@(ap@(ap@c_2EPast__Temporal__Logic_2EPBEFORE@(lam@ty_2Enum_2Enum@(^ [V36t:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V3d@V36t))@(ap@(ap@c_2EPast__Temporal__Logic_2EPSNEXT@V1b)@V36t)))))@(lam@ty_2Enum_2Enum@(^ [V37t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@V0a@V37t)))@(ap@c_2Ebool_2E_7E@(ap@V3d@V37t))))))@V35t)))))@V3d)@V32t))))))))))))))))))))).
