tt('const/Past_Temporal_Logic/InitPoint', ty, ('type/num/num' > $o)).
tt('const/Past_Temporal_Logic/PALWAYS', ty, (('type/num/num' > $o) > ('type/num/num' > $o))).
tt('const/Past_Temporal_Logic/PBEFORE', ty, (('type/num/num' > $o) > (('type/num/num' > $o) > ('type/num/num' > $o)))).
tt('const/Past_Temporal_Logic/PEVENTUAL', ty, (('type/num/num' > $o) > ('type/num/num' > $o))).
tt('const/Past_Temporal_Logic/PNEXT', ty, (('type/num/num' > $o) > ('type/num/num' > $o))).
tt('const/Past_Temporal_Logic/PSBEFORE', ty, (('type/num/num' > $o) > (('type/num/num' > $o) > ('type/num/num' > $o)))).
tt('const/Past_Temporal_Logic/PSNEXT', ty, (('type/num/num' > $o) > ('type/num/num' > $o))).
tt('const/Past_Temporal_Logic/PSUNTIL', ty, (('type/num/num' > $o) > (('type/num/num' > $o) > ('type/num/num' > $o)))).
tt('const/Past_Temporal_Logic/PSWHEN', ty, (('type/num/num' > $o) > (('type/num/num' > $o) > ('type/num/num' > $o)))).
tt('const/Past_Temporal_Logic/PUNTIL', ty, (('type/num/num' > $o) > (('type/num/num' > $o) > ('type/num/num' > $o)))).
tt('const/Past_Temporal_Logic/PWHEN', ty, (('type/num/num' > $o) > (('type/num/num' > $o) > ('type/num/num' > $o)))).
tt('thm/Past_Temporal_Logic/InitPoint_', def, ('const/Past_Temporal_Logic/InitPoint' = (^[t : 'type/num/num']: (t = 'const/num/0')))).
tt('thm/Past_Temporal_Logic/PSNEXT_', def, (![a : ('type/num/num' > $o), t0 : 'type/num/num']: (('const/Past_Temporal_Logic/PSNEXT' a t0) = (('const/prim_rec/<' 'const/num/0' t0) & (a ('const/prim_rec/PRE' t0)))))).
tt('thm/Past_Temporal_Logic/PNEXT_', def, (![a : ('type/num/num' > $o), t0 : 'type/num/num']: (('const/Past_Temporal_Logic/PNEXT' a t0) = ((t0 = 'const/num/0') | (a ('const/prim_rec/PRE' t0)))))).
tt('thm/Past_Temporal_Logic/PALWAYS_', def, (![a : ('type/num/num' > $o), t0 : 'type/num/num']: (('const/Past_Temporal_Logic/PALWAYS' a t0) = (![t : 'type/num/num']: (('const/arithmetic/<=' t t0) => (a t)))))).
tt('thm/Past_Temporal_Logic/PEVENTUAL_', def, (![a : ('type/num/num' > $o), t0 : 'type/num/num']: (('const/Past_Temporal_Logic/PEVENTUAL' a t0) = (?[t : 'type/num/num']: (('const/arithmetic/<=' t t0) & (a t)))))).
tt('thm/Past_Temporal_Logic/PSWHEN_', def, (![a : ('type/num/num' > $o), b : ('type/num/num' > $o), t0 : 'type/num/num']: (('const/Past_Temporal_Logic/PSWHEN' a b t0) = (?[delta : 'type/num/num']: (('const/arithmetic/<=' delta t0) & ((a delta) & ((b delta) & (![t : 'type/num/num']: ((('const/prim_rec/<' delta t) & ('const/arithmetic/<=' t t0)) => (~ (b t))))))))))).
tt('thm/Past_Temporal_Logic/PSUNTIL_', def, (![a : ('type/num/num' > $o), b : ('type/num/num' > $o), t0 : 'type/num/num']: (('const/Past_Temporal_Logic/PSUNTIL' a b t0) = (?[delta : 'type/num/num']: (('const/arithmetic/<=' delta t0) & ((b delta) & (![t : 'type/num/num']: ((('const/prim_rec/<' delta t) & ('const/arithmetic/<=' t t0)) => ((a t) & (~ (b t))))))))))).
tt('thm/Past_Temporal_Logic/PSBEFORE_', def, (![a : ('type/num/num' > $o), b : ('type/num/num' > $o), t0 : 'type/num/num']: (('const/Past_Temporal_Logic/PSBEFORE' a b t0) = (?[delta : 'type/num/num']: (('const/arithmetic/<=' delta t0) & ((a delta) & (![t : 'type/num/num']: ((('const/arithmetic/<=' delta t) & ('const/arithmetic/<=' t t0)) => (~ (b t)))))))))).
tt('thm/Past_Temporal_Logic/PWHEN_', def, (![a : ('type/num/num' > $o), b : ('type/num/num' > $o), t0 : 'type/num/num']: (('const/Past_Temporal_Logic/PWHEN' a b t0) = ((![t : 'type/num/num']: (('const/arithmetic/<=' t t0) => (~ (b t)))) | (?[delta : 'type/num/num']: (('const/arithmetic/<=' delta t0) & ((a delta) & ((b delta) & (![t : 'type/num/num']: ((('const/prim_rec/<' delta t) & ('const/arithmetic/<=' t t0)) => (~ (b t)))))))))))).
tt('thm/Past_Temporal_Logic/PUNTIL_', def, (![a : ('type/num/num' > $o), b : ('type/num/num' > $o), t0 : 'type/num/num']: (('const/Past_Temporal_Logic/PUNTIL' a b t0) = ((![t : 'type/num/num']: (('const/arithmetic/<=' t t0) => (a t))) | (?[delta : 'type/num/num']: (('const/arithmetic/<=' delta t0) & ((b delta) & (![t : 'type/num/num']: ((('const/prim_rec/<' delta t) & ('const/arithmetic/<=' t t0)) => ((a t) & (~ (b t)))))))))))).
tt('thm/Past_Temporal_Logic/PBEFORE_', def, (![a : ('type/num/num' > $o), b : ('type/num/num' > $o), t0 : 'type/num/num']: (('const/Past_Temporal_Logic/PBEFORE' a b t0) = ((![t : 'type/num/num']: (('const/arithmetic/<=' t t0) => (~ (b t)))) | (?[delta : 'type/num/num']: (('const/arithmetic/<=' delta t0) & ((a delta) & (![t : 'type/num/num']: ((('const/arithmetic/<=' delta t) & ('const/arithmetic/<=' t t0)) => (~ (b t))))))))))).
tt('thm/Past_Temporal_Logic/INITIALISATION_0', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' a 'const/num/0') = $true))).
tt('thm/Past_Temporal_Logic/INITIALISATION_1', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSNEXT' a 'const/num/0') = $false))).
tt('thm/Past_Temporal_Logic/INITIALISATION_2', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PALWAYS' a 'const/num/0') = (a 'const/num/0')))).
tt('thm/Past_Temporal_Logic/INITIALISATION_3', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PEVENTUAL' a 'const/num/0') = (a 'const/num/0')))).
tt('thm/Past_Temporal_Logic/INITIALISATION_4', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' a b 'const/num/0') = (b 'const/num/0')))).
tt('thm/Past_Temporal_Logic/INITIALISATION_5', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSWHEN' a b 'const/num/0') = ((a 'const/num/0') & (b 'const/num/0'))))).
tt('thm/Past_Temporal_Logic/INITIALISATION_6', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSBEFORE' a b 'const/num/0') = ((a 'const/num/0') & (~ (b 'const/num/0')))))).
tt('thm/Past_Temporal_Logic/INITIALISATION_7', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PUNTIL' a b 'const/num/0') = ((a 'const/num/0') | (b 'const/num/0'))))).
tt('thm/Past_Temporal_Logic/INITIALISATION_8', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PWHEN' a b 'const/num/0') = ((a 'const/num/0') | (~ (b 'const/num/0')))))).
tt('thm/Past_Temporal_Logic/INITIALISATION_e9', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PBEFORE' a b 'const/num/0') = (~ (b 'const/num/0'))))).
tt('thm/Past_Temporal_Logic/RECURSION_0', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/ALWAYS' a) = (^[t : 'type/num/num']: ((a t) & ('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/ALWAYS' a) t)))))).
tt('thm/Past_Temporal_Logic/RECURSION_1', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/EVENTUAL' a) = (^[t : 'type/num/num']: ((a t) | ('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/EVENTUAL' a) t)))))).
tt('thm/Past_Temporal_Logic/RECURSION_2', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' a b) = (^[t : 'type/num/num']: ((~ (b t)) => ((a t) & ('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/SUNTIL' a b) t))))))).
tt('thm/Past_Temporal_Logic/RECURSION_3', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SWHEN' a b) = (^[t : 'type/num/num']: (('const/bool/COND' $o) (b t) (a t) ('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/SWHEN' a b) t)))))).
tt('thm/Past_Temporal_Logic/RECURSION_4', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SBEFORE' a b) = (^[t : 'type/num/num']: ((~ (b t)) & ((a t) | ('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/SBEFORE' a b) t))))))).
tt('thm/Past_Temporal_Logic/RECURSION_5', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/UNTIL' a b) = (^[t : 'type/num/num']: ((~ (b t)) => ((a t) & ('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/UNTIL' a b) t))))))).
tt('thm/Past_Temporal_Logic/RECURSION_6', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/WHEN' a b) = (^[t : 'type/num/num']: (('const/bool/COND' $o) (b t) (a t) ('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/WHEN' a b) t)))))).
tt('thm/Past_Temporal_Logic/RECURSION_7', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' a b) = (^[t : 'type/num/num']: ((~ (b t)) & ((a t) | ('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/BEFORE' a b) t))))))).
tt('thm/Past_Temporal_Logic/RECURSION_8', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PALWAYS' a) = (^[t : 'type/num/num']: ((a t) & ('const/Past_Temporal_Logic/PNEXT' ('const/Past_Temporal_Logic/PALWAYS' a) t)))))).
tt('thm/Past_Temporal_Logic/RECURSION_9', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PEVENTUAL' a) = (^[t : 'type/num/num']: ((a t) | ('const/Past_Temporal_Logic/PSNEXT' ('const/Past_Temporal_Logic/PEVENTUAL' a) t)))))).
tt('thm/Past_Temporal_Logic/RECURSION_10', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' a b) = (^[t : 'type/num/num']: ((b t) | ((a t) & ('const/Past_Temporal_Logic/PSNEXT' ('const/Past_Temporal_Logic/PSUNTIL' a b) t))))))).
tt('thm/Past_Temporal_Logic/RECURSION_11', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSWHEN' a b) = (^[t : 'type/num/num']: (((a t) & (b t)) | ((~ (b t)) & ('const/Past_Temporal_Logic/PSNEXT' ('const/Past_Temporal_Logic/PSWHEN' a b) t))))))).
tt('thm/Past_Temporal_Logic/RECURSION_12', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSBEFORE' a b) = (^[t : 'type/num/num']: ((~ (b t)) & ((a t) | ('const/Past_Temporal_Logic/PSNEXT' ('const/Past_Temporal_Logic/PSBEFORE' a b) t))))))).
tt('thm/Past_Temporal_Logic/RECURSION_13', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PUNTIL' a b) = (^[t : 'type/num/num']: ((b t) | ((a t) & ('const/Past_Temporal_Logic/PNEXT' ('const/Past_Temporal_Logic/PUNTIL' a b) t))))))).
tt('thm/Past_Temporal_Logic/RECURSION_14', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PWHEN' a b) = (^[t : 'type/num/num']: (((a t) & (b t)) | ((~ (b t)) & ('const/Past_Temporal_Logic/PNEXT' ('const/Past_Temporal_Logic/PWHEN' a b) t))))))).
tt('thm/Past_Temporal_Logic/RECURSION_e15', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PBEFORE' a b) = (^[t : 'type/num/num']: ((~ (b t)) & ((a t) | ('const/Past_Temporal_Logic/PNEXT' ('const/Past_Temporal_Logic/PBEFORE' a b) t))))))).
tt('thm/Past_Temporal_Logic/FIXPOINTS_0', ax, (![y : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((y = (^[t : 'type/num/num']: ((a t) & ('const/Temporal_Logic/NEXT' y t)))) = ((y = ('const/Temporal_Logic/ALWAYS' a)) | (y = (^[t : 'type/num/num']: $false)))))).
tt('thm/Past_Temporal_Logic/FIXPOINTS_1', ax, (![y : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((y = (^[t : 'type/num/num']: ((a t) | ('const/Temporal_Logic/NEXT' y t)))) = ((y = ('const/Temporal_Logic/EVENTUAL' a)) | (y = (^[t : 'type/num/num']: $true)))))).
tt('thm/Past_Temporal_Logic/FIXPOINTS_2', ax, (![y : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((y = (^[t : 'type/num/num']: ((~ (b t)) => ((a t) & ('const/Temporal_Logic/NEXT' y t))))) = ((y = ('const/Temporal_Logic/UNTIL' a b)) | (y = ('const/Temporal_Logic/SUNTIL' a b)))))).
tt('thm/Past_Temporal_Logic/FIXPOINTS_3', ax, (![y : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((y = (^[t : 'type/num/num']: (('const/bool/COND' $o) (b t) (a t) ('const/Temporal_Logic/NEXT' y t)))) = ((y = ('const/Temporal_Logic/WHEN' a b)) | (y = ('const/Temporal_Logic/SWHEN' a b)))))).
tt('thm/Past_Temporal_Logic/FIXPOINTS_4', ax, (![y : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((y = (^[t : 'type/num/num']: ((~ (b t)) & ((a t) | ('const/Temporal_Logic/NEXT' y t))))) = ((y = ('const/Temporal_Logic/BEFORE' a b)) | (y = ('const/Temporal_Logic/SBEFORE' a b)))))).
tt('thm/Past_Temporal_Logic/FIXPOINTS_5', ax, (![y : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((y = (^[t : 'type/num/num']: ((a t) & ('const/Past_Temporal_Logic/PNEXT' y t)))) = (y = ('const/Past_Temporal_Logic/PALWAYS' a))))).
tt('thm/Past_Temporal_Logic/FIXPOINTS_6', ax, (![y : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((y = (^[t : 'type/num/num']: ((a t) | ('const/Past_Temporal_Logic/PSNEXT' y t)))) = (y = ('const/Past_Temporal_Logic/PEVENTUAL' a))))).
tt('thm/Past_Temporal_Logic/FIXPOINTS_7', ax, (![y : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((y = (^[t : 'type/num/num']: ((b t) | ((a t) & ('const/Past_Temporal_Logic/PSNEXT' y t))))) = (y = ('const/Past_Temporal_Logic/PSUNTIL' a b))))).
tt('thm/Past_Temporal_Logic/FIXPOINTS_8', ax, (![y : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((y = (^[t : 'type/num/num']: (((a t) & (b t)) | ((~ (b t)) & ('const/Past_Temporal_Logic/PSNEXT' y t))))) = (y = ('const/Past_Temporal_Logic/PSWHEN' a b))))).
tt('thm/Past_Temporal_Logic/FIXPOINTS_9', ax, (![y : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((y = (^[t : 'type/num/num']: ((~ (b t)) & ((a t) | ('const/Past_Temporal_Logic/PSNEXT' y t))))) = (y = ('const/Past_Temporal_Logic/PSBEFORE' a b))))).
tt('thm/Past_Temporal_Logic/FIXPOINTS_10', ax, (![y : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((y = (^[t : 'type/num/num']: ((b t) | ((a t) & ('const/Past_Temporal_Logic/PNEXT' y t))))) = (y = ('const/Past_Temporal_Logic/PUNTIL' a b))))).
tt('thm/Past_Temporal_Logic/FIXPOINTS_11', ax, (![y : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((y = (^[t : 'type/num/num']: (((a t) & (b t)) | ((~ (b t)) & ('const/Past_Temporal_Logic/PNEXT' y t))))) = (y = ('const/Past_Temporal_Logic/PWHEN' a b))))).
tt('thm/Past_Temporal_Logic/FIXPOINTS_e12', ax, (![y : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((y = (^[t : 'type/num/num']: ((~ (b t)) & ((a t) | ('const/Past_Temporal_Logic/PNEXT' y t))))) = (y = ('const/Past_Temporal_Logic/PBEFORE' a b))))).
tt('thm/Past_Temporal_Logic/SUNTIL_EXPRESSIVE_0', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/ALWAYS' a) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/SUNTIL' (^[t0 : 'type/num/num']: $true) (^[t0 : 'type/num/num']: (~ (a t0))) t)))))).
tt('thm/Past_Temporal_Logic/SUNTIL_EXPRESSIVE_1', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/EVENTUAL' a) = (^[t : 'type/num/num']: ('const/Temporal_Logic/SUNTIL' (^[t0 : 'type/num/num']: $true) a t))))).
tt('thm/Past_Temporal_Logic/SUNTIL_EXPRESSIVE_2', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/UNTIL' a b) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/SUNTIL' (^[t0 : 'type/num/num']: (~ (b t0))) (^[t0 : 'type/num/num']: ((~ (a t0)) & (~ (b t0)))) t)))))).
tt('thm/Past_Temporal_Logic/SUNTIL_EXPRESSIVE_3', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/WHEN' a b) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/SUNTIL' (^[t0 : 'type/num/num']: ((~ (a t0)) | (~ (b t0)))) (^[t0 : 'type/num/num']: ((~ (a t0)) & (b t0))) t)))))).
tt('thm/Past_Temporal_Logic/SUNTIL_EXPRESSIVE_4', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' a b) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/SUNTIL' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))))).
tt('thm/Past_Temporal_Logic/SUNTIL_EXPRESSIVE_5', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SWHEN' a b) = (^[t : 'type/num/num']: ('const/Temporal_Logic/SUNTIL' (^[t0 : 'type/num/num']: (~ (b t0))) (^[t0 : 'type/num/num']: ((a t0) & (b t0))) t))))).
tt('thm/Past_Temporal_Logic/SUNTIL_EXPRESSIVE_e6', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SBEFORE' a b) = (^[t : 'type/num/num']: ('const/Temporal_Logic/SUNTIL' (^[t0 : 'type/num/num']: (~ (b t0))) (^[t0 : 'type/num/num']: ((a t0) & (~ (b t0)))) t))))).
tt('thm/Past_Temporal_Logic/UNTIL_EXPRESSIVE_0', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/ALWAYS' a) = (^[t : 'type/num/num']: ('const/Temporal_Logic/UNTIL' a (^[t0 : 'type/num/num']: $false) t))))).
tt('thm/Past_Temporal_Logic/UNTIL_EXPRESSIVE_1', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/EVENTUAL' a) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/UNTIL' (^[t0 : 'type/num/num']: (~ (a t0))) (^[t0 : 'type/num/num']: $false) t)))))).
tt('thm/Past_Temporal_Logic/UNTIL_EXPRESSIVE_2', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' a b) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/UNTIL' (^[t0 : 'type/num/num']: (~ (b t0))) (^[t0 : 'type/num/num']: ((~ (a t0)) & (~ (b t0)))) t)))))).
tt('thm/Past_Temporal_Logic/UNTIL_EXPRESSIVE_3', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/WHEN' a b) = (^[t : 'type/num/num']: ('const/Temporal_Logic/UNTIL' (^[t0 : 'type/num/num']: (~ (b t0))) (^[t0 : 'type/num/num']: ((a t0) & (b t0))) t))))).
tt('thm/Past_Temporal_Logic/UNTIL_EXPRESSIVE_4', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SWHEN' a b) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/UNTIL' (^[t0 : 'type/num/num']: ((~ (a t0)) | (~ (b t0)))) (^[t0 : 'type/num/num']: ((~ (a t0)) & (b t0))) t)))))).
tt('thm/Past_Temporal_Logic/UNTIL_EXPRESSIVE_5', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' a b) = (^[t : 'type/num/num']: ('const/Temporal_Logic/UNTIL' (^[t0 : 'type/num/num']: (~ (b t0))) (^[t0 : 'type/num/num']: ((a t0) & (~ (b t0)))) t))))).
tt('thm/Past_Temporal_Logic/UNTIL_EXPRESSIVE_e6', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SBEFORE' a b) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/UNTIL' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))))).
tt('thm/Past_Temporal_Logic/WHEN_EXPRESSIVE_0', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/ALWAYS' a) = (^[t : 'type/num/num']: ('const/Temporal_Logic/WHEN' (^[t0 : 'type/num/num']: $false) (^[t0 : 'type/num/num']: (~ (a t0))) t))))).
tt('thm/Past_Temporal_Logic/WHEN_EXPRESSIVE_1', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/EVENTUAL' a) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/WHEN' (^[t0 : 'type/num/num']: $false) a t)))))).
tt('thm/Past_Temporal_Logic/WHEN_EXPRESSIVE_2', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' a b) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/WHEN' (^[t0 : 'type/num/num']: (~ (b t0))) (^[t0 : 'type/num/num']: ((a t0) => (b t0))) t)))))).
tt('thm/Past_Temporal_Logic/WHEN_EXPRESSIVE_3', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/UNTIL' a b) = (^[t : 'type/num/num']: ('const/Temporal_Logic/WHEN' b (^[t0 : 'type/num/num']: ((a t0) => (b t0))) t))))).
tt('thm/Past_Temporal_Logic/WHEN_EXPRESSIVE_4', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SWHEN' a b) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/WHEN' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))))).
tt('thm/Past_Temporal_Logic/WHEN_EXPRESSIVE_5', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' a b) = (^[t : 'type/num/num']: ('const/Temporal_Logic/WHEN' (^[t0 : 'type/num/num']: (~ (b t0))) (^[t0 : 'type/num/num']: ((a t0) | (b t0))) t))))).
tt('thm/Past_Temporal_Logic/WHEN_EXPRESSIVE_e6', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SBEFORE' a b) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/WHEN' b (^[t0 : 'type/num/num']: ((a t0) | (b t0))) t)))))).
tt('thm/Past_Temporal_Logic/SWHEN_EXPRESSIVE_0', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/ALWAYS' a) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/SWHEN' (^[t0 : 'type/num/num']: $true) (^[t0 : 'type/num/num']: (~ (a t0))) t)))))).
tt('thm/Past_Temporal_Logic/SWHEN_EXPRESSIVE_1', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/EVENTUAL' a) = (^[t : 'type/num/num']: ('const/Temporal_Logic/SWHEN' (^[t0 : 'type/num/num']: $true) a t))))).
tt('thm/Past_Temporal_Logic/SWHEN_EXPRESSIVE_2', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' a b) = (^[t : 'type/num/num']: ('const/Temporal_Logic/SWHEN' b (^[t0 : 'type/num/num']: ((a t0) => (b t0))) t))))).
tt('thm/Past_Temporal_Logic/SWHEN_EXPRESSIVE_3', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/UNTIL' a b) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/SWHEN' (^[t0 : 'type/num/num']: (~ (b t0))) (^[t0 : 'type/num/num']: ((a t0) => (b t0))) t)))))).
tt('thm/Past_Temporal_Logic/SWHEN_EXPRESSIVE_4', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/WHEN' a b) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/SWHEN' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))))).
tt('thm/Past_Temporal_Logic/SWHEN_EXPRESSIVE_5', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' a b) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/SWHEN' b (^[t0 : 'type/num/num']: ((a t0) | (b t0))) t)))))).
tt('thm/Past_Temporal_Logic/SWHEN_EXPRESSIVE_e6', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SBEFORE' a b) = (^[t : 'type/num/num']: ('const/Temporal_Logic/SWHEN' (^[t0 : 'type/num/num']: (~ (b t0))) (^[t0 : 'type/num/num']: ((a t0) | (b t0))) t))))).
tt('thm/Past_Temporal_Logic/BEFORE_EXPRESSIVE_0', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/ALWAYS' a) = (^[t : 'type/num/num']: ('const/Temporal_Logic/BEFORE' (^[t0 : 'type/num/num']: $false) (^[t0 : 'type/num/num']: (~ (a t0))) t))))).
tt('thm/Past_Temporal_Logic/BEFORE_EXPRESSIVE_1', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/EVENTUAL' a) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/BEFORE' (^[t0 : 'type/num/num']: $false) a t)))))).
tt('thm/Past_Temporal_Logic/BEFORE_EXPRESSIVE_2', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' a b) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/BEFORE' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))))).
tt('thm/Past_Temporal_Logic/BEFORE_EXPRESSIVE_3', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/UNTIL' a b) = (^[t : 'type/num/num']: ('const/Temporal_Logic/BEFORE' b (^[t0 : 'type/num/num']: ((~ (a t0)) & (~ (b t0)))) t))))).
tt('thm/Past_Temporal_Logic/BEFORE_EXPRESSIVE_4', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SWHEN' a b) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/BEFORE' b (^[t0 : 'type/num/num']: ((a t0) & (b t0))) t)))))).
tt('thm/Past_Temporal_Logic/BEFORE_EXPRESSIVE_5', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/WHEN' a b) = (^[t : 'type/num/num']: ('const/Temporal_Logic/BEFORE' (^[t0 : 'type/num/num']: ((a t0) & (b t0))) (^[t0 : 'type/num/num']: ((~ (a t0)) & (b t0))) t))))).
tt('thm/Past_Temporal_Logic/BEFORE_EXPRESSIVE_e6', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SBEFORE' a b) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/BEFORE' b (^[t0 : 'type/num/num']: ((a t0) & (~ (b t0)))) t)))))).
tt('thm/Past_Temporal_Logic/SBEFORE_EXPRESSIVE_0', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/ALWAYS' a) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/SBEFORE' (^[t0 : 'type/num/num']: (~ (a t0))) (^[t0 : 'type/num/num']: $false) t)))))).
tt('thm/Past_Temporal_Logic/SBEFORE_EXPRESSIVE_1', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/EVENTUAL' a) = (^[t : 'type/num/num']: ('const/Temporal_Logic/SBEFORE' a (^[t0 : 'type/num/num']: $false) t))))).
tt('thm/Past_Temporal_Logic/SBEFORE_EXPRESSIVE_2', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' a b) = (^[t : 'type/num/num']: ('const/Temporal_Logic/SBEFORE' b (^[t0 : 'type/num/num']: ((~ (a t0)) & (~ (b t0)))) t))))).
tt('thm/Past_Temporal_Logic/SBEFORE_EXPRESSIVE_3', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/UNTIL' a b) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/SBEFORE' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))))).
tt('thm/Past_Temporal_Logic/SBEFORE_EXPRESSIVE_4', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SWHEN' a b) = (^[t : 'type/num/num']: ('const/Temporal_Logic/SBEFORE' b (^[t0 : 'type/num/num']: ((~ (a t0)) & (b t0))) t))))).
tt('thm/Past_Temporal_Logic/SBEFORE_EXPRESSIVE_5', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/WHEN' a b) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/SBEFORE' b (^[t0 : 'type/num/num']: ((a t0) & (b t0))) t)))))).
tt('thm/Past_Temporal_Logic/SBEFORE_EXPRESSIVE_e6', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' a b) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/SBEFORE' b (^[t0 : 'type/num/num']: ((a t0) & (~ (b t0)))) t)))))).
tt('thm/Past_Temporal_Logic/PSUNTIL_EXPRESSIVE_0', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PALWAYS' a) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PSUNTIL' (^[t0 : 'type/num/num']: $true) (^[t0 : 'type/num/num']: (~ (a t0))) t)))))).
tt('thm/Past_Temporal_Logic/PSUNTIL_EXPRESSIVE_1', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PEVENTUAL' a) = (^[t : 'type/num/num']: ('const/Past_Temporal_Logic/PSUNTIL' (^[t0 : 'type/num/num']: $true) a t))))).
tt('thm/Past_Temporal_Logic/PSUNTIL_EXPRESSIVE_2', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PUNTIL' a b) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PSUNTIL' (^[t0 : 'type/num/num']: (~ (b t0))) (^[t0 : 'type/num/num']: ((~ (a t0)) & (~ (b t0)))) t)))))).
tt('thm/Past_Temporal_Logic/PSUNTIL_EXPRESSIVE_3', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PWHEN' a b) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PSUNTIL' (^[t0 : 'type/num/num']: ((~ (a t0)) | (~ (b t0)))) (^[t0 : 'type/num/num']: ((~ (a t0)) & (b t0))) t)))))).
tt('thm/Past_Temporal_Logic/PSUNTIL_EXPRESSIVE_4', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PBEFORE' a b) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PSUNTIL' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))))).
tt('thm/Past_Temporal_Logic/PSUNTIL_EXPRESSIVE_5', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSWHEN' a b) = (^[t : 'type/num/num']: ('const/Past_Temporal_Logic/PSUNTIL' (^[t0 : 'type/num/num']: (~ (b t0))) (^[t0 : 'type/num/num']: ((a t0) & (b t0))) t))))).
tt('thm/Past_Temporal_Logic/PSUNTIL_EXPRESSIVE_e6', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSBEFORE' a b) = (^[t : 'type/num/num']: ('const/Past_Temporal_Logic/PSUNTIL' (^[t0 : 'type/num/num']: (~ (b t0))) (^[t0 : 'type/num/num']: ((a t0) & (~ (b t0)))) t))))).
tt('thm/Past_Temporal_Logic/PUNTIL_EXPRESSIVE_0', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PALWAYS' a) = (^[t : 'type/num/num']: ('const/Past_Temporal_Logic/PUNTIL' a (^[t0 : 'type/num/num']: $false) t))))).
tt('thm/Past_Temporal_Logic/PUNTIL_EXPRESSIVE_1', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PEVENTUAL' a) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PUNTIL' (^[t0 : 'type/num/num']: (~ (a t0))) (^[t0 : 'type/num/num']: $false) t)))))).
tt('thm/Past_Temporal_Logic/PUNTIL_EXPRESSIVE_2', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' a b) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PUNTIL' (^[t0 : 'type/num/num']: (~ (b t0))) (^[t0 : 'type/num/num']: ((~ (a t0)) & (~ (b t0)))) t)))))).
tt('thm/Past_Temporal_Logic/PUNTIL_EXPRESSIVE_3', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PWHEN' a b) = (^[t : 'type/num/num']: ('const/Past_Temporal_Logic/PUNTIL' (^[t0 : 'type/num/num']: (~ (b t0))) (^[t0 : 'type/num/num']: ((a t0) & (b t0))) t))))).
tt('thm/Past_Temporal_Logic/PUNTIL_EXPRESSIVE_4', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSWHEN' a b) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PUNTIL' (^[t0 : 'type/num/num']: ((~ (a t0)) | (~ (b t0)))) (^[t0 : 'type/num/num']: ((~ (a t0)) & (b t0))) t)))))).
tt('thm/Past_Temporal_Logic/PUNTIL_EXPRESSIVE_5', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PBEFORE' a b) = (^[t : 'type/num/num']: ('const/Past_Temporal_Logic/PUNTIL' (^[t0 : 'type/num/num']: (~ (b t0))) (^[t0 : 'type/num/num']: ((a t0) & (~ (b t0)))) t))))).
tt('thm/Past_Temporal_Logic/PUNTIL_EXPRESSIVE_e6', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSBEFORE' a b) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PUNTIL' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))))).
tt('thm/Past_Temporal_Logic/PWHEN_EXPRESSIVE_0', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PALWAYS' a) = (^[t : 'type/num/num']: ('const/Past_Temporal_Logic/PWHEN' (^[t0 : 'type/num/num']: $false) (^[t0 : 'type/num/num']: (~ (a t0))) t))))).
tt('thm/Past_Temporal_Logic/PWHEN_EXPRESSIVE_1', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PEVENTUAL' a) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PWHEN' (^[t0 : 'type/num/num']: $false) a t)))))).
tt('thm/Past_Temporal_Logic/PWHEN_EXPRESSIVE_2', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' a b) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PWHEN' (^[t0 : 'type/num/num']: (~ (b t0))) (^[t0 : 'type/num/num']: ((a t0) => (b t0))) t)))))).
tt('thm/Past_Temporal_Logic/PWHEN_EXPRESSIVE_3', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PUNTIL' a b) = (^[t : 'type/num/num']: ('const/Past_Temporal_Logic/PWHEN' b (^[t0 : 'type/num/num']: ((a t0) => (b t0))) t))))).
tt('thm/Past_Temporal_Logic/PWHEN_EXPRESSIVE_4', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSWHEN' a b) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PWHEN' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))))).
tt('thm/Past_Temporal_Logic/PWHEN_EXPRESSIVE_5', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PBEFORE' a b) = (^[t : 'type/num/num']: ('const/Past_Temporal_Logic/PWHEN' (^[t0 : 'type/num/num']: (~ (b t0))) (^[t0 : 'type/num/num']: ((a t0) | (b t0))) t))))).
tt('thm/Past_Temporal_Logic/PWHEN_EXPRESSIVE_e6', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSBEFORE' a b) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PWHEN' b (^[t0 : 'type/num/num']: ((a t0) | (b t0))) t)))))).
tt('thm/Past_Temporal_Logic/PSWHEN_EXPRESSIVE_0', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PALWAYS' a) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PSWHEN' (^[t0 : 'type/num/num']: $true) (^[t0 : 'type/num/num']: (~ (a t0))) t)))))).
tt('thm/Past_Temporal_Logic/PSWHEN_EXPRESSIVE_1', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PEVENTUAL' a) = (^[t : 'type/num/num']: ('const/Past_Temporal_Logic/PSWHEN' (^[t0 : 'type/num/num']: $true) a t))))).
tt('thm/Past_Temporal_Logic/PSWHEN_EXPRESSIVE_2', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' a b) = (^[t : 'type/num/num']: ('const/Past_Temporal_Logic/PSWHEN' b (^[t0 : 'type/num/num']: ((a t0) => (b t0))) t))))).
tt('thm/Past_Temporal_Logic/PSWHEN_EXPRESSIVE_3', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PUNTIL' a b) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PSWHEN' (^[t0 : 'type/num/num']: (~ (b t0))) (^[t0 : 'type/num/num']: ((a t0) => (b t0))) t)))))).
tt('thm/Past_Temporal_Logic/PSWHEN_EXPRESSIVE_4', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PWHEN' a b) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PSWHEN' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))))).
tt('thm/Past_Temporal_Logic/PSWHEN_EXPRESSIVE_5', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PBEFORE' a b) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PSWHEN' b (^[t0 : 'type/num/num']: ((a t0) | (b t0))) t)))))).
tt('thm/Past_Temporal_Logic/PSWHEN_EXPRESSIVE_e6', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSBEFORE' a b) = (^[t : 'type/num/num']: ('const/Past_Temporal_Logic/PSWHEN' (^[t0 : 'type/num/num']: (~ (b t0))) (^[t0 : 'type/num/num']: ((a t0) | (b t0))) t))))).
tt('thm/Past_Temporal_Logic/PBEFORE_EXPRESSIVE_0', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PALWAYS' a) = (^[t : 'type/num/num']: ('const/Past_Temporal_Logic/PBEFORE' (^[t0 : 'type/num/num']: $false) (^[t0 : 'type/num/num']: (~ (a t0))) t))))).
tt('thm/Past_Temporal_Logic/PBEFORE_EXPRESSIVE_1', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PEVENTUAL' a) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PBEFORE' (^[t0 : 'type/num/num']: $false) a t)))))).
tt('thm/Past_Temporal_Logic/PBEFORE_EXPRESSIVE_2', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' a b) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PBEFORE' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))))).
tt('thm/Past_Temporal_Logic/PBEFORE_EXPRESSIVE_3', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PUNTIL' a b) = (^[t : 'type/num/num']: ('const/Past_Temporal_Logic/PBEFORE' b (^[t0 : 'type/num/num']: ((~ (a t0)) & (~ (b t0)))) t))))).
tt('thm/Past_Temporal_Logic/PBEFORE_EXPRESSIVE_4', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSWHEN' a b) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PBEFORE' b (^[t0 : 'type/num/num']: ((a t0) & (b t0))) t)))))).
tt('thm/Past_Temporal_Logic/PBEFORE_EXPRESSIVE_5', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PWHEN' a b) = (^[t : 'type/num/num']: ('const/Past_Temporal_Logic/PBEFORE' (^[t0 : 'type/num/num']: ((a t0) & (b t0))) (^[t0 : 'type/num/num']: ((~ (a t0)) & (b t0))) t))))).
tt('thm/Past_Temporal_Logic/PBEFORE_EXPRESSIVE_e6', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSBEFORE' a b) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PBEFORE' b (^[t0 : 'type/num/num']: ((a t0) & (~ (b t0)))) t)))))).
tt('thm/Past_Temporal_Logic/PSBEFORE_EXPRESSIVE_0', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PALWAYS' a) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PSBEFORE' (^[t0 : 'type/num/num']: (~ (a t0))) (^[t0 : 'type/num/num']: $false) t)))))).
tt('thm/Past_Temporal_Logic/PSBEFORE_EXPRESSIVE_1', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PEVENTUAL' a) = (^[t : 'type/num/num']: ('const/Past_Temporal_Logic/PSBEFORE' a (^[t0 : 'type/num/num']: $false) t))))).
tt('thm/Past_Temporal_Logic/PSBEFORE_EXPRESSIVE_2', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' a b) = (^[t : 'type/num/num']: ('const/Past_Temporal_Logic/PSBEFORE' b (^[t0 : 'type/num/num']: ((~ (a t0)) & (~ (b t0)))) t))))).
tt('thm/Past_Temporal_Logic/PSBEFORE_EXPRESSIVE_3', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PUNTIL' a b) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PSBEFORE' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))))).
tt('thm/Past_Temporal_Logic/PSBEFORE_EXPRESSIVE_4', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSWHEN' a b) = (^[t : 'type/num/num']: ('const/Past_Temporal_Logic/PSBEFORE' b (^[t0 : 'type/num/num']: ((~ (a t0)) & (b t0))) t))))).
tt('thm/Past_Temporal_Logic/PSBEFORE_EXPRESSIVE_5', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PWHEN' a b) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PSBEFORE' b (^[t0 : 'type/num/num']: ((a t0) & (b t0))) t)))))).
tt('thm/Past_Temporal_Logic/PSBEFORE_EXPRESSIVE_e6', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PBEFORE' a b) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PSBEFORE' b (^[t0 : 'type/num/num']: ((a t0) & (~ (b t0)))) t)))))).
tt('thm/Past_Temporal_Logic/NEGATION_NORMAL_FORM_0', ax, (![t : 'type/num/num', a : ('type/num/num' > $o)]: ((~ ('const/Temporal_Logic/NEXT' a t)) = ('const/Temporal_Logic/NEXT' (^[t0 : 'type/num/num']: (~ (a t0))) t)))).
tt('thm/Past_Temporal_Logic/NEGATION_NORMAL_FORM_1', ax, (![t : 'type/num/num', a : ('type/num/num' > $o)]: ((~ ('const/Temporal_Logic/ALWAYS' a t)) = ('const/Temporal_Logic/EVENTUAL' (^[t0 : 'type/num/num']: (~ (a t0))) t)))).
tt('thm/Past_Temporal_Logic/NEGATION_NORMAL_FORM_2', ax, (![t : 'type/num/num', a : ('type/num/num' > $o)]: ((~ ('const/Temporal_Logic/EVENTUAL' a t)) = ('const/Temporal_Logic/ALWAYS' (^[t0 : 'type/num/num']: (~ (a t0))) t)))).
tt('thm/Past_Temporal_Logic/NEGATION_NORMAL_FORM_3', ax, (![t : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((~ ('const/Temporal_Logic/WHEN' a b t)) = ('const/Temporal_Logic/SWHEN' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))).
tt('thm/Past_Temporal_Logic/NEGATION_NORMAL_FORM_4', ax, (![t : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((~ ('const/Temporal_Logic/UNTIL' a b t)) = ('const/Temporal_Logic/SBEFORE' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))).
tt('thm/Past_Temporal_Logic/NEGATION_NORMAL_FORM_5', ax, (![t : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((~ ('const/Temporal_Logic/BEFORE' a b t)) = ('const/Temporal_Logic/SUNTIL' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))).
tt('thm/Past_Temporal_Logic/NEGATION_NORMAL_FORM_6', ax, (![t : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((~ ('const/Temporal_Logic/SWHEN' a b t)) = ('const/Temporal_Logic/WHEN' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))).
tt('thm/Past_Temporal_Logic/NEGATION_NORMAL_FORM_7', ax, (![t : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((~ ('const/Temporal_Logic/SUNTIL' a b t)) = ('const/Temporal_Logic/BEFORE' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))).
tt('thm/Past_Temporal_Logic/NEGATION_NORMAL_FORM_8', ax, (![t : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((~ ('const/Temporal_Logic/SBEFORE' a b t)) = ('const/Temporal_Logic/UNTIL' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))).
tt('thm/Past_Temporal_Logic/NEGATION_NORMAL_FORM_9', ax, (![t : 'type/num/num', a : ('type/num/num' > $o)]: ((~ ('const/Past_Temporal_Logic/PNEXT' a t)) = ('const/Past_Temporal_Logic/PSNEXT' (^[t0 : 'type/num/num']: (~ (a t0))) t)))).
tt('thm/Past_Temporal_Logic/NEGATION_NORMAL_FORM_10', ax, (![t : 'type/num/num', a : ('type/num/num' > $o)]: ((~ ('const/Past_Temporal_Logic/PSNEXT' a t)) = ('const/Past_Temporal_Logic/PNEXT' (^[t0 : 'type/num/num']: (~ (a t0))) t)))).
tt('thm/Past_Temporal_Logic/NEGATION_NORMAL_FORM_11', ax, (![t : 'type/num/num', a : ('type/num/num' > $o)]: ((~ ('const/Past_Temporal_Logic/PALWAYS' a t)) = ('const/Past_Temporal_Logic/PEVENTUAL' (^[t0 : 'type/num/num']: (~ (a t0))) t)))).
tt('thm/Past_Temporal_Logic/NEGATION_NORMAL_FORM_12', ax, (![t : 'type/num/num', a : ('type/num/num' > $o)]: ((~ ('const/Past_Temporal_Logic/PEVENTUAL' a t)) = ('const/Past_Temporal_Logic/PALWAYS' (^[t0 : 'type/num/num']: (~ (a t0))) t)))).
tt('thm/Past_Temporal_Logic/NEGATION_NORMAL_FORM_13', ax, (![t : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((~ ('const/Past_Temporal_Logic/PWHEN' a b t)) = ('const/Past_Temporal_Logic/PSWHEN' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))).
tt('thm/Past_Temporal_Logic/NEGATION_NORMAL_FORM_14', ax, (![t : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((~ ('const/Past_Temporal_Logic/PUNTIL' a b t)) = ('const/Past_Temporal_Logic/PSBEFORE' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))).
tt('thm/Past_Temporal_Logic/NEGATION_NORMAL_FORM_15', ax, (![t : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((~ ('const/Past_Temporal_Logic/PBEFORE' a b t)) = ('const/Past_Temporal_Logic/PSUNTIL' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))).
tt('thm/Past_Temporal_Logic/NEGATION_NORMAL_FORM_16', ax, (![t : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((~ ('const/Past_Temporal_Logic/PSWHEN' a b t)) = ('const/Past_Temporal_Logic/PWHEN' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))).
tt('thm/Past_Temporal_Logic/NEGATION_NORMAL_FORM_17', ax, (![t : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((~ ('const/Past_Temporal_Logic/PSUNTIL' a b t)) = ('const/Past_Temporal_Logic/PBEFORE' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))).
tt('thm/Past_Temporal_Logic/NEGATION_NORMAL_FORM_e18', ax, (![t : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((~ ('const/Past_Temporal_Logic/PSBEFORE' a b t)) = ('const/Past_Temporal_Logic/PUNTIL' (^[t0 : 'type/num/num']: (~ (a t0))) b t)))).
tt('thm/Past_Temporal_Logic/CONJUNCTIVE_NORMAL_FORM_0', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' (^[t : 'type/num/num']: ((a t) & (b t)))) = (^[t : 'type/num/num']: (('const/Temporal_Logic/NEXT' a t) & ('const/Temporal_Logic/NEXT' b t)))))).
tt('thm/Past_Temporal_Logic/CONJUNCTIVE_NORMAL_FORM_1', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/ALWAYS' (^[t : 'type/num/num']: ((a t) & (b t)))) = (^[t : 'type/num/num']: (('const/Temporal_Logic/ALWAYS' a t) & ('const/Temporal_Logic/ALWAYS' b t)))))).
tt('thm/Past_Temporal_Logic/CONJUNCTIVE_NORMAL_FORM_2', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/WHEN' (^[t : 'type/num/num']: ((a t) & (b t))) c) = (^[t : 'type/num/num']: (('const/Temporal_Logic/WHEN' a c t) & ('const/Temporal_Logic/WHEN' b c t)))))).
tt('thm/Past_Temporal_Logic/CONJUNCTIVE_NORMAL_FORM_3', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SWHEN' (^[t : 'type/num/num']: ((a t) & (b t))) c) = (^[t : 'type/num/num']: (('const/Temporal_Logic/SWHEN' a c t) & ('const/Temporal_Logic/SWHEN' b c t)))))).
tt('thm/Past_Temporal_Logic/CONJUNCTIVE_NORMAL_FORM_4', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/UNTIL' (^[t : 'type/num/num']: ((a t) & (b t))) c) = (^[t : 'type/num/num']: (('const/Temporal_Logic/UNTIL' a c t) & ('const/Temporal_Logic/UNTIL' b c t)))))).
tt('thm/Past_Temporal_Logic/CONJUNCTIVE_NORMAL_FORM_5', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' (^[t : 'type/num/num']: ((a t) & (b t))) c) = (^[t : 'type/num/num']: (('const/Temporal_Logic/SUNTIL' a c t) & ('const/Temporal_Logic/SUNTIL' b c t)))))).
tt('thm/Past_Temporal_Logic/CONJUNCTIVE_NORMAL_FORM_6', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' c (^[t : 'type/num/num']: ((a t) | (b t)))) = (^[t : 'type/num/num']: (('const/Temporal_Logic/BEFORE' c a t) & ('const/Temporal_Logic/BEFORE' c b t)))))).
tt('thm/Past_Temporal_Logic/CONJUNCTIVE_NORMAL_FORM_7', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SBEFORE' c (^[t : 'type/num/num']: ((a t) | (b t)))) = (^[t : 'type/num/num']: (('const/Temporal_Logic/SBEFORE' c a t) & ('const/Temporal_Logic/SBEFORE' c b t)))))).
tt('thm/Past_Temporal_Logic/CONJUNCTIVE_NORMAL_FORM_8', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' (^[t : 'type/num/num']: ((a t) & (b t)))) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PNEXT' a t) & ('const/Past_Temporal_Logic/PNEXT' b t)))))).
tt('thm/Past_Temporal_Logic/CONJUNCTIVE_NORMAL_FORM_9', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSNEXT' (^[t : 'type/num/num']: ((a t) & (b t)))) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PSNEXT' a t) & ('const/Past_Temporal_Logic/PSNEXT' b t)))))).
tt('thm/Past_Temporal_Logic/CONJUNCTIVE_NORMAL_FORM_10', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PALWAYS' (^[t : 'type/num/num']: ((a t) & (b t)))) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PALWAYS' a t) & ('const/Past_Temporal_Logic/PALWAYS' b t)))))).
tt('thm/Past_Temporal_Logic/CONJUNCTIVE_NORMAL_FORM_11', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PWHEN' (^[t : 'type/num/num']: ((a t) & (b t))) c) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PWHEN' a c t) & ('const/Past_Temporal_Logic/PWHEN' b c t)))))).
tt('thm/Past_Temporal_Logic/CONJUNCTIVE_NORMAL_FORM_12', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSWHEN' (^[t : 'type/num/num']: ((a t) & (b t))) c) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PSWHEN' a c t) & ('const/Past_Temporal_Logic/PSWHEN' b c t)))))).
tt('thm/Past_Temporal_Logic/CONJUNCTIVE_NORMAL_FORM_13', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PUNTIL' (^[t : 'type/num/num']: ((a t) & (b t))) c) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PUNTIL' a c t) & ('const/Past_Temporal_Logic/PUNTIL' b c t)))))).
tt('thm/Past_Temporal_Logic/CONJUNCTIVE_NORMAL_FORM_14', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' (^[t : 'type/num/num']: ((a t) & (b t))) c) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PSUNTIL' a c t) & ('const/Past_Temporal_Logic/PSUNTIL' b c t)))))).
tt('thm/Past_Temporal_Logic/CONJUNCTIVE_NORMAL_FORM_15', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PBEFORE' c (^[t : 'type/num/num']: ((a t) | (b t)))) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PBEFORE' c a t) & ('const/Past_Temporal_Logic/PBEFORE' c b t)))))).
tt('thm/Past_Temporal_Logic/CONJUNCTIVE_NORMAL_FORM_e16', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSBEFORE' c (^[t : 'type/num/num']: ((a t) | (b t)))) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PSBEFORE' c a t) & ('const/Past_Temporal_Logic/PSBEFORE' c b t)))))).
tt('thm/Past_Temporal_Logic/DISJUNCTIVE_NORMAL_FORM_0', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' (^[t : 'type/num/num']: ((a t) | (b t)))) = (^[t : 'type/num/num']: (('const/Temporal_Logic/NEXT' a t) | ('const/Temporal_Logic/NEXT' b t)))))).
tt('thm/Past_Temporal_Logic/DISJUNCTIVE_NORMAL_FORM_1', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/EVENTUAL' (^[t : 'type/num/num']: ((a t) | (b t)))) = (^[t : 'type/num/num']: (('const/Temporal_Logic/EVENTUAL' a t) | ('const/Temporal_Logic/EVENTUAL' b t)))))).
tt('thm/Past_Temporal_Logic/DISJUNCTIVE_NORMAL_FORM_2', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/WHEN' (^[t : 'type/num/num']: ((a t) | (b t))) c) = (^[t : 'type/num/num']: (('const/Temporal_Logic/WHEN' a c t) | ('const/Temporal_Logic/WHEN' b c t)))))).
tt('thm/Past_Temporal_Logic/DISJUNCTIVE_NORMAL_FORM_3', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SWHEN' (^[t : 'type/num/num']: ((a t) | (b t))) c) = (^[t : 'type/num/num']: (('const/Temporal_Logic/SWHEN' a c t) | ('const/Temporal_Logic/SWHEN' b c t)))))).
tt('thm/Past_Temporal_Logic/DISJUNCTIVE_NORMAL_FORM_4', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/UNTIL' a (^[t : 'type/num/num']: ((b t) | (c t)))) = (^[t : 'type/num/num']: (('const/Temporal_Logic/UNTIL' a b t) | ('const/Temporal_Logic/UNTIL' a c t)))))).
tt('thm/Past_Temporal_Logic/DISJUNCTIVE_NORMAL_FORM_5', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' a (^[t : 'type/num/num']: ((b t) | (c t)))) = (^[t : 'type/num/num']: (('const/Temporal_Logic/SUNTIL' a b t) | ('const/Temporal_Logic/SUNTIL' a c t)))))).
tt('thm/Past_Temporal_Logic/DISJUNCTIVE_NORMAL_FORM_6', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' (^[t : 'type/num/num']: ((a t) | (b t))) c) = (^[t : 'type/num/num']: (('const/Temporal_Logic/BEFORE' a c t) | ('const/Temporal_Logic/BEFORE' b c t)))))).
tt('thm/Past_Temporal_Logic/DISJUNCTIVE_NORMAL_FORM_7', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SBEFORE' (^[t : 'type/num/num']: ((a t) | (b t))) c) = (^[t : 'type/num/num']: (('const/Temporal_Logic/SBEFORE' a c t) | ('const/Temporal_Logic/SBEFORE' b c t)))))).
tt('thm/Past_Temporal_Logic/DISJUNCTIVE_NORMAL_FORM_8', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' (^[t : 'type/num/num']: ((a t) | (b t)))) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PNEXT' a t) | ('const/Past_Temporal_Logic/PNEXT' b t)))))).
tt('thm/Past_Temporal_Logic/DISJUNCTIVE_NORMAL_FORM_9', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PEVENTUAL' (^[t : 'type/num/num']: ((a t) | (b t)))) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PEVENTUAL' a t) | ('const/Past_Temporal_Logic/PEVENTUAL' b t)))))).
tt('thm/Past_Temporal_Logic/DISJUNCTIVE_NORMAL_FORM_10', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PWHEN' (^[t : 'type/num/num']: ((a t) | (b t))) c) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PWHEN' a c t) | ('const/Past_Temporal_Logic/PWHEN' b c t)))))).
tt('thm/Past_Temporal_Logic/DISJUNCTIVE_NORMAL_FORM_11', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSWHEN' (^[t : 'type/num/num']: ((a t) | (b t))) c) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PSWHEN' a c t) | ('const/Past_Temporal_Logic/PSWHEN' b c t)))))).
tt('thm/Past_Temporal_Logic/DISJUNCTIVE_NORMAL_FORM_12', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PUNTIL' a (^[t : 'type/num/num']: ((b t) | (c t)))) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PUNTIL' a b t) | ('const/Past_Temporal_Logic/PUNTIL' a c t)))))).
tt('thm/Past_Temporal_Logic/DISJUNCTIVE_NORMAL_FORM_13', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' a (^[t : 'type/num/num']: ((b t) | (c t)))) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PSUNTIL' a b t) | ('const/Past_Temporal_Logic/PSUNTIL' a c t)))))).
tt('thm/Past_Temporal_Logic/DISJUNCTIVE_NORMAL_FORM_14', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PBEFORE' (^[t : 'type/num/num']: ((a t) | (b t))) c) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PBEFORE' a c t) | ('const/Past_Temporal_Logic/PBEFORE' b c t)))))).
tt('thm/Past_Temporal_Logic/DISJUNCTIVE_NORMAL_FORM_e15', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSBEFORE' (^[t : 'type/num/num']: ((a t) | (b t))) c) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PSBEFORE' a c t) | ('const/Past_Temporal_Logic/PSBEFORE' b c t)))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_0', ax, (![t : 'type/num/num', a : ('type/num/num' > $o)]: ((~ ('const/Temporal_Logic/NEXT' a t)) = ('const/Temporal_Logic/NEXT' (^[t0 : 'type/num/num']: (~ (a t0))) t)))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_1', ax, (![t : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (((a t) & ('const/Temporal_Logic/NEXT' b t)) = ('const/Temporal_Logic/NEXT' (^[t0 : 'type/num/num']: (('const/Past_Temporal_Logic/PNEXT' a t0) & (b t0))) t)))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_2', ax, (![t : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (((a t) | ('const/Temporal_Logic/NEXT' b t)) = ('const/Temporal_Logic/NEXT' (^[t0 : 'type/num/num']: (('const/Past_Temporal_Logic/PNEXT' a t0) | (b t0))) t)))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_3', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/ALWAYS' ('const/Temporal_Logic/NEXT' a)) = ('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/ALWAYS' a))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_4', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/EVENTUAL' ('const/Temporal_Logic/NEXT' a)) = ('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/EVENTUAL' a))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_5', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' a ('const/Temporal_Logic/NEXT' b)) = ('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/SUNTIL' ('const/Past_Temporal_Logic/PNEXT' a) b))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_6', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SWHEN' a ('const/Temporal_Logic/NEXT' b)) = ('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/SWHEN' ('const/Past_Temporal_Logic/PNEXT' a) b))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_7', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SBEFORE' a ('const/Temporal_Logic/NEXT' b)) = ('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/SBEFORE' ('const/Past_Temporal_Logic/PNEXT' a) b))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_8', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/UNTIL' a ('const/Temporal_Logic/NEXT' b)) = ('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/UNTIL' ('const/Past_Temporal_Logic/PNEXT' a) b))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_9', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/WHEN' a ('const/Temporal_Logic/NEXT' b)) = ('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/WHEN' ('const/Past_Temporal_Logic/PNEXT' a) b))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_10', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' a ('const/Temporal_Logic/NEXT' b)) = ('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/BEFORE' ('const/Past_Temporal_Logic/PNEXT' a) b))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_11', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' ('const/Temporal_Logic/NEXT' a) b) = ('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/SUNTIL' a ('const/Past_Temporal_Logic/PNEXT' b)))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_12', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SWHEN' ('const/Temporal_Logic/NEXT' a) b) = ('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/SWHEN' a ('const/Past_Temporal_Logic/PNEXT' b)))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_13', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SBEFORE' ('const/Temporal_Logic/NEXT' a) b) = ('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/SBEFORE' a ('const/Past_Temporal_Logic/PNEXT' b)))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_14', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/UNTIL' ('const/Temporal_Logic/NEXT' a) b) = ('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/UNTIL' a ('const/Past_Temporal_Logic/PNEXT' b)))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_15', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/WHEN' ('const/Temporal_Logic/NEXT' a) b) = ('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/WHEN' a ('const/Past_Temporal_Logic/PNEXT' b)))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_16', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' ('const/Temporal_Logic/NEXT' a) b) = ('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/BEFORE' a ('const/Past_Temporal_Logic/PNEXT' b)))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_17', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' ('const/Temporal_Logic/NEXT' a)) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/InitPoint' t) | (a t)))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_18', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSNEXT' ('const/Temporal_Logic/NEXT' a)) = (^[t : 'type/num/num']: ((~ ('const/Past_Temporal_Logic/InitPoint' t)) & (a t)))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_19', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PALWAYS' ('const/Temporal_Logic/NEXT' a)) = ('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PALWAYS' (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/InitPoint' t) | (a t)))))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_20', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PEVENTUAL' ('const/Temporal_Logic/NEXT' a)) = ('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PEVENTUAL' (^[t : 'type/num/num']: ((~ ('const/Past_Temporal_Logic/InitPoint' t)) & (a t)))))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_21', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' a ('const/Temporal_Logic/NEXT' b)) = ('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PSUNTIL' ('const/Past_Temporal_Logic/PNEXT' a) (^[t : 'type/num/num']: ((~ ('const/Past_Temporal_Logic/InitPoint' t)) & (b t)))))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_22', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSWHEN' a ('const/Temporal_Logic/NEXT' b)) = ('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PSWHEN' ('const/Past_Temporal_Logic/PNEXT' a) (^[t : 'type/num/num']: ((~ ('const/Past_Temporal_Logic/InitPoint' t)) & (b t)))))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_23', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSBEFORE' a ('const/Temporal_Logic/NEXT' b)) = ('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PSBEFORE' ('const/Past_Temporal_Logic/PSNEXT' a) b))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_24', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PUNTIL' a ('const/Temporal_Logic/NEXT' b)) = ('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PUNTIL' ('const/Past_Temporal_Logic/PNEXT' a) b))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_25', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PWHEN' a ('const/Temporal_Logic/NEXT' b)) = ('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PWHEN' ('const/Past_Temporal_Logic/PNEXT' a) (^[t : 'type/num/num']: ((~ ('const/Past_Temporal_Logic/InitPoint' t)) & (b t)))))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_26', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PBEFORE' a ('const/Temporal_Logic/NEXT' b)) = ('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PBEFORE' ('const/Past_Temporal_Logic/PNEXT' a) (^[t : 'type/num/num']: ((~ ('const/Past_Temporal_Logic/InitPoint' t)) & (b t)))))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_27', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' ('const/Temporal_Logic/NEXT' a) b) = ('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PSUNTIL' a ('const/Past_Temporal_Logic/PSNEXT' b)))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_28', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSWHEN' ('const/Temporal_Logic/NEXT' a) b) = ('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PSWHEN' a ('const/Past_Temporal_Logic/PSNEXT' b)))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_29', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSBEFORE' ('const/Temporal_Logic/NEXT' a) b) = ('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PSBEFORE' (^[t : 'type/num/num']: ((~ ('const/Past_Temporal_Logic/InitPoint' t)) & (a t))) ('const/Past_Temporal_Logic/PNEXT' b)))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_30', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PUNTIL' ('const/Temporal_Logic/NEXT' a) b) = ('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PUNTIL' (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/InitPoint' t) | (a t))) ('const/Past_Temporal_Logic/PNEXT' b)))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_31', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PWHEN' ('const/Temporal_Logic/NEXT' a) b) = ('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PWHEN' a ('const/Past_Temporal_Logic/PSNEXT' b)))))).
tt('thm/Past_Temporal_Logic/PRENEX_NEXT_NORMAL_FORM_e32', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PBEFORE' ('const/Temporal_Logic/NEXT' a) b) = ('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PBEFORE' a ('const/Past_Temporal_Logic/PSNEXT' b)))))).
tt('thm/Past_Temporal_Logic/NEXT_INWARDS_NORMAL_FORM_0', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' (^[t : 'type/num/num']: (~ (a t)))) = (^[t : 'type/num/num']: (~ ('const/Temporal_Logic/NEXT' a t)))))).
tt('thm/Past_Temporal_Logic/NEXT_INWARDS_NORMAL_FORM_1', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' (^[t : 'type/num/num']: ((a t) & (b t)))) = (^[t : 'type/num/num']: (('const/Temporal_Logic/NEXT' a t) & ('const/Temporal_Logic/NEXT' b t)))))).
tt('thm/Past_Temporal_Logic/NEXT_INWARDS_NORMAL_FORM_2', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' (^[t : 'type/num/num']: ((a t) | (b t)))) = (^[t : 'type/num/num']: (('const/Temporal_Logic/NEXT' a t) | ('const/Temporal_Logic/NEXT' b t)))))).
tt('thm/Past_Temporal_Logic/NEXT_INWARDS_NORMAL_FORM_3', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/ALWAYS' a)) = ('const/Temporal_Logic/ALWAYS' ('const/Temporal_Logic/NEXT' a))))).
tt('thm/Past_Temporal_Logic/NEXT_INWARDS_NORMAL_FORM_4', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/EVENTUAL' a)) = ('const/Temporal_Logic/EVENTUAL' ('const/Temporal_Logic/NEXT' a))))).
tt('thm/Past_Temporal_Logic/NEXT_INWARDS_NORMAL_FORM_5', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/SUNTIL' a b)) = ('const/Temporal_Logic/SUNTIL' ('const/Temporal_Logic/NEXT' a) ('const/Temporal_Logic/NEXT' b))))).
tt('thm/Past_Temporal_Logic/NEXT_INWARDS_NORMAL_FORM_6', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/SWHEN' a b)) = ('const/Temporal_Logic/SWHEN' ('const/Temporal_Logic/NEXT' a) ('const/Temporal_Logic/NEXT' b))))).
tt('thm/Past_Temporal_Logic/NEXT_INWARDS_NORMAL_FORM_7', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/SBEFORE' a b)) = ('const/Temporal_Logic/SBEFORE' ('const/Temporal_Logic/NEXT' a) ('const/Temporal_Logic/NEXT' b))))).
tt('thm/Past_Temporal_Logic/NEXT_INWARDS_NORMAL_FORM_8', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/UNTIL' a b)) = ('const/Temporal_Logic/UNTIL' ('const/Temporal_Logic/NEXT' a) ('const/Temporal_Logic/NEXT' b))))).
tt('thm/Past_Temporal_Logic/NEXT_INWARDS_NORMAL_FORM_9', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/WHEN' a b)) = ('const/Temporal_Logic/WHEN' ('const/Temporal_Logic/NEXT' a) ('const/Temporal_Logic/NEXT' b))))).
tt('thm/Past_Temporal_Logic/NEXT_INWARDS_NORMAL_FORM_10', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' ('const/Temporal_Logic/BEFORE' a b)) = ('const/Temporal_Logic/BEFORE' ('const/Temporal_Logic/NEXT' a) ('const/Temporal_Logic/NEXT' b))))).
tt('thm/Past_Temporal_Logic/NEXT_INWARDS_NORMAL_FORM_11', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PNEXT' a)) = a))).
tt('thm/Past_Temporal_Logic/NEXT_INWARDS_NORMAL_FORM_12', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PSNEXT' a)) = a))).
tt('thm/Past_Temporal_Logic/NEXT_INWARDS_NORMAL_FORM_13', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PALWAYS' a)) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PALWAYS' a t) & ('const/Temporal_Logic/NEXT' a t)))))).
tt('thm/Past_Temporal_Logic/NEXT_INWARDS_NORMAL_FORM_14', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PEVENTUAL' a)) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PEVENTUAL' a t) | ('const/Temporal_Logic/NEXT' a t)))))).
tt('thm/Past_Temporal_Logic/NEXT_INWARDS_NORMAL_FORM_15', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PSUNTIL' a b)) = (^[t : 'type/num/num']: (('const/Temporal_Logic/NEXT' b t) | (('const/Temporal_Logic/NEXT' a t) & ('const/Past_Temporal_Logic/PSUNTIL' a b t))))))).
tt('thm/Past_Temporal_Logic/NEXT_INWARDS_NORMAL_FORM_16', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PSWHEN' a b)) = (^[t : 'type/num/num']: (('const/bool/COND' $o) ('const/Temporal_Logic/NEXT' b t) ('const/Temporal_Logic/NEXT' a t) ('const/Past_Temporal_Logic/PSWHEN' a b t)))))).
tt('thm/Past_Temporal_Logic/NEXT_INWARDS_NORMAL_FORM_17', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PSBEFORE' a b)) = (^[t : 'type/num/num']: ((~ ('const/Temporal_Logic/NEXT' b t)) & (('const/Temporal_Logic/NEXT' a t) | ('const/Past_Temporal_Logic/PSBEFORE' a b t))))))).
tt('thm/Past_Temporal_Logic/NEXT_INWARDS_NORMAL_FORM_18', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PUNTIL' a b)) = (^[t : 'type/num/num']: (('const/Temporal_Logic/NEXT' b t) | (('const/Temporal_Logic/NEXT' a t) & ('const/Past_Temporal_Logic/PUNTIL' a b t))))))).
tt('thm/Past_Temporal_Logic/NEXT_INWARDS_NORMAL_FORM_19', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PWHEN' a b)) = (^[t : 'type/num/num']: (('const/bool/COND' $o) ('const/Temporal_Logic/NEXT' b t) ('const/Temporal_Logic/NEXT' a t) ('const/Past_Temporal_Logic/PWHEN' a b t)))))).
tt('thm/Past_Temporal_Logic/NEXT_INWARDS_NORMAL_FORM_e20', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' ('const/Past_Temporal_Logic/PBEFORE' a b)) = (^[t : 'type/num/num']: ((~ ('const/Temporal_Logic/NEXT' b t)) & (('const/Temporal_Logic/NEXT' a t) | ('const/Past_Temporal_Logic/PBEFORE' a b t))))))).
tt('thm/Past_Temporal_Logic/PNEXT_INWARDS_NORMAL_FORM_0', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' (^[t : 'type/num/num']: (~ (a t)))) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/PSNEXT' a t)))))).
tt('thm/Past_Temporal_Logic/PNEXT_INWARDS_NORMAL_FORM_1', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' (^[t : 'type/num/num']: ((a t) & (b t)))) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PNEXT' a t) & ('const/Past_Temporal_Logic/PNEXT' b t)))))).
tt('thm/Past_Temporal_Logic/PNEXT_INWARDS_NORMAL_FORM_2', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' (^[t : 'type/num/num']: ((a t) | (b t)))) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PNEXT' a t) | ('const/Past_Temporal_Logic/PNEXT' b t)))))).
tt('thm/Past_Temporal_Logic/PNEXT_INWARDS_NORMAL_FORM_3', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' ('const/Temporal_Logic/NEXT' a)) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/InitPoint' t) | (a t)))))).
tt('thm/Past_Temporal_Logic/PNEXT_INWARDS_NORMAL_FORM_4', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' ('const/Temporal_Logic/ALWAYS' a)) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/InitPoint' t) | ('const/Temporal_Logic/ALWAYS' ('const/Past_Temporal_Logic/PNEXT' a) t)))))).
tt('thm/Past_Temporal_Logic/PNEXT_INWARDS_NORMAL_FORM_5', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' ('const/Temporal_Logic/EVENTUAL' a)) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/InitPoint' t) | ('const/Temporal_Logic/EVENTUAL' ('const/Past_Temporal_Logic/PNEXT' a) t)))))).
tt('thm/Past_Temporal_Logic/PNEXT_INWARDS_NORMAL_FORM_6', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' ('const/Temporal_Logic/SUNTIL' a b)) = ('const/Temporal_Logic/SUNTIL' ('const/Past_Temporal_Logic/PNEXT' a) ('const/Past_Temporal_Logic/PNEXT' b))))).
tt('thm/Past_Temporal_Logic/PNEXT_INWARDS_NORMAL_FORM_7', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' ('const/Temporal_Logic/SWHEN' a b)) = ('const/Temporal_Logic/SWHEN' ('const/Past_Temporal_Logic/PNEXT' a) ('const/Past_Temporal_Logic/PNEXT' b))))).
tt('thm/Past_Temporal_Logic/PNEXT_INWARDS_NORMAL_FORM_8', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' ('const/Temporal_Logic/SBEFORE' a b)) = ('const/Temporal_Logic/SBEFORE' ('const/Past_Temporal_Logic/PNEXT' a) ('const/Past_Temporal_Logic/PSNEXT' b))))).
tt('thm/Past_Temporal_Logic/PNEXT_INWARDS_NORMAL_FORM_9', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' ('const/Temporal_Logic/UNTIL' a b)) = ('const/Temporal_Logic/UNTIL' ('const/Past_Temporal_Logic/PNEXT' a) ('const/Past_Temporal_Logic/PNEXT' b))))).
tt('thm/Past_Temporal_Logic/PNEXT_INWARDS_NORMAL_FORM_10', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' ('const/Temporal_Logic/WHEN' a b)) = ('const/Temporal_Logic/WHEN' ('const/Past_Temporal_Logic/PNEXT' a) ('const/Past_Temporal_Logic/PNEXT' b))))).
tt('thm/Past_Temporal_Logic/PNEXT_INWARDS_NORMAL_FORM_11', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' ('const/Temporal_Logic/BEFORE' a b)) = ('const/Temporal_Logic/BEFORE' ('const/Past_Temporal_Logic/PNEXT' a) ('const/Past_Temporal_Logic/PSNEXT' b))))).
tt('thm/Past_Temporal_Logic/PNEXT_INWARDS_NORMAL_FORM_12', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' ('const/Past_Temporal_Logic/PALWAYS' a)) = ('const/Past_Temporal_Logic/PALWAYS' ('const/Past_Temporal_Logic/PNEXT' a))))).
tt('thm/Past_Temporal_Logic/PNEXT_INWARDS_NORMAL_FORM_13', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' ('const/Past_Temporal_Logic/PEVENTUAL' a)) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/InitPoint' t) | ('const/Past_Temporal_Logic/PEVENTUAL' ('const/Past_Temporal_Logic/PSNEXT' a) t)))))).
tt('thm/Past_Temporal_Logic/PNEXT_INWARDS_NORMAL_FORM_14', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' ('const/Past_Temporal_Logic/PSUNTIL' a b)) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/InitPoint' t) | ('const/Past_Temporal_Logic/PSUNTIL' ('const/Past_Temporal_Logic/PNEXT' a) ('const/Past_Temporal_Logic/PSNEXT' b) t)))))).
tt('thm/Past_Temporal_Logic/PNEXT_INWARDS_NORMAL_FORM_15', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' ('const/Past_Temporal_Logic/PSWHEN' a b)) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/InitPoint' t) | ('const/Past_Temporal_Logic/PSWHEN' ('const/Past_Temporal_Logic/PNEXT' a) ('const/Past_Temporal_Logic/PSNEXT' b) t)))))).
tt('thm/Past_Temporal_Logic/PNEXT_INWARDS_NORMAL_FORM_16', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' ('const/Past_Temporal_Logic/PSBEFORE' a b)) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/InitPoint' t) | ('const/Past_Temporal_Logic/PSBEFORE' ('const/Past_Temporal_Logic/PSNEXT' a) ('const/Past_Temporal_Logic/PNEXT' b) t)))))).
tt('thm/Past_Temporal_Logic/PNEXT_INWARDS_NORMAL_FORM_17', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' ('const/Past_Temporal_Logic/PUNTIL' a b)) = ('const/Past_Temporal_Logic/PUNTIL' ('const/Past_Temporal_Logic/PNEXT' a) ('const/Past_Temporal_Logic/PNEXT' b))))).
tt('thm/Past_Temporal_Logic/PNEXT_INWARDS_NORMAL_FORM_18', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' ('const/Past_Temporal_Logic/PWHEN' a b)) = ('const/Past_Temporal_Logic/PWHEN' ('const/Past_Temporal_Logic/PNEXT' a) ('const/Past_Temporal_Logic/PNEXT' b))))).
tt('thm/Past_Temporal_Logic/PNEXT_INWARDS_NORMAL_FORM_e19', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' ('const/Past_Temporal_Logic/PBEFORE' a b)) = ('const/Past_Temporal_Logic/PBEFORE' ('const/Past_Temporal_Logic/PNEXT' a) ('const/Past_Temporal_Logic/PSNEXT' b))))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_0', ax, (('const/Temporal_Logic/NEXT' (^[t : 'type/num/num']: $false)) = (^[t : 'type/num/num']: $false))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_1', ax, (('const/Temporal_Logic/NEXT' (^[t : 'type/num/num']: $true)) = (^[t : 'type/num/num']: $true))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_2', ax, (('const/Temporal_Logic/ALWAYS' (^[t : 'type/num/num']: $true)) = (^[t : 'type/num/num']: $true))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_3', ax, (('const/Temporal_Logic/ALWAYS' (^[t : 'type/num/num']: $false)) = (^[t : 'type/num/num']: $false))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_4', ax, (('const/Temporal_Logic/EVENTUAL' (^[t : 'type/num/num']: $true)) = (^[t : 'type/num/num']: $true))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_5', ax, (('const/Temporal_Logic/EVENTUAL' (^[t : 'type/num/num']: $false)) = (^[t : 'type/num/num']: $false))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_6', ax, (![b : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' (^[t : 'type/num/num']: $false) b) = b))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_7', ax, (![b : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' (^[t : 'type/num/num']: $true) b) = ('const/Temporal_Logic/EVENTUAL' b)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_8', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' a (^[t : 'type/num/num']: $false)) = (^[t : 'type/num/num']: $false)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_9', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' a (^[t : 'type/num/num']: $true)) = (^[t : 'type/num/num']: $true)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_10', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' a a) = a))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_11', ax, (![b : ('type/num/num' > $o)]: (('const/Temporal_Logic/UNTIL' (^[t : 'type/num/num']: $false) b) = b))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_12', ax, (![b : ('type/num/num' > $o)]: (('const/Temporal_Logic/UNTIL' (^[t : 'type/num/num']: $true) b) = (^[t : 'type/num/num']: $true)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_13', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/UNTIL' a (^[t : 'type/num/num']: $false)) = ('const/Temporal_Logic/ALWAYS' a)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_14', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/UNTIL' a (^[t : 'type/num/num']: $true)) = (^[t : 'type/num/num']: $true)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_15', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/UNTIL' a a) = a))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_16', ax, (![b : ('type/num/num' > $o)]: (('const/Temporal_Logic/SWHEN' (^[t : 'type/num/num']: $false) b) = (^[t : 'type/num/num']: $false)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_17', ax, (![b : ('type/num/num' > $o)]: (('const/Temporal_Logic/SWHEN' (^[t : 'type/num/num']: $true) b) = ('const/Temporal_Logic/EVENTUAL' b)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_18', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SWHEN' a (^[t : 'type/num/num']: $false)) = (^[t : 'type/num/num']: $false)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_19', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SWHEN' a (^[t : 'type/num/num']: $true)) = a))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_20', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SWHEN' a a) = ('const/Temporal_Logic/EVENTUAL' a)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_21', ax, (![b : ('type/num/num' > $o)]: (('const/Temporal_Logic/WHEN' (^[t : 'type/num/num']: $false) b) = ('const/Temporal_Logic/ALWAYS' (^[t : 'type/num/num']: (~ (b t))))))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_22', ax, (![b : ('type/num/num' > $o)]: (('const/Temporal_Logic/WHEN' (^[t : 'type/num/num']: $true) b) = (^[t : 'type/num/num']: $true)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_23', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/WHEN' a (^[t : 'type/num/num']: $false)) = (^[t : 'type/num/num']: $true)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_24', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/WHEN' a (^[t : 'type/num/num']: $true)) = a))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_25', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/WHEN' a a) = (^[t : 'type/num/num']: $true)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_26', ax, (![b : ('type/num/num' > $o)]: (('const/Temporal_Logic/SBEFORE' (^[t : 'type/num/num']: $false) b) = (^[t : 'type/num/num']: $false)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_27', ax, (![b : ('type/num/num' > $o)]: (('const/Temporal_Logic/SBEFORE' (^[t : 'type/num/num']: $true) b) = (^[t : 'type/num/num']: (~ (b t)))))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_28', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SBEFORE' a (^[t : 'type/num/num']: $false)) = ('const/Temporal_Logic/EVENTUAL' a)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_29', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SBEFORE' a (^[t : 'type/num/num']: $true)) = (^[t : 'type/num/num']: $false)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_30', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SBEFORE' a a) = (^[t : 'type/num/num']: $false)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_31', ax, (![b : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' (^[t : 'type/num/num']: $false) b) = ('const/Temporal_Logic/ALWAYS' (^[t : 'type/num/num']: (~ (b t))))))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_32', ax, (![b : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' (^[t : 'type/num/num']: $true) b) = (^[t : 'type/num/num']: (~ (b t)))))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_33', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' a (^[t : 'type/num/num']: $false)) = (^[t : 'type/num/num']: $true)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_34', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' a (^[t : 'type/num/num']: $true)) = (^[t : 'type/num/num']: $false)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_35', ax, (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' a a) = ('const/Temporal_Logic/ALWAYS' (^[t : 'type/num/num']: (~ (a t))))))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_36', ax, (('const/Past_Temporal_Logic/PNEXT' (^[t : 'type/num/num']: $false)) = 'const/Past_Temporal_Logic/InitPoint')).
tt('thm/Past_Temporal_Logic/SIMPLIFY_37', ax, (('const/Past_Temporal_Logic/PNEXT' (^[t : 'type/num/num']: $true)) = (^[t : 'type/num/num']: $true))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_38', ax, (('const/Past_Temporal_Logic/PSNEXT' (^[t : 'type/num/num']: $false)) = (^[t : 'type/num/num']: $false))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_39', ax, (('const/Past_Temporal_Logic/PSNEXT' (^[t : 'type/num/num']: $true)) = (^[t : 'type/num/num']: (~ ('const/Past_Temporal_Logic/InitPoint' t))))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_40', ax, (('const/Past_Temporal_Logic/PALWAYS' (^[t : 'type/num/num']: $true)) = (^[t : 'type/num/num']: $true))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_41', ax, (('const/Past_Temporal_Logic/PALWAYS' (^[t : 'type/num/num']: $false)) = (^[t : 'type/num/num']: $false))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_42', ax, (('const/Past_Temporal_Logic/PEVENTUAL' (^[t : 'type/num/num']: $true)) = (^[t : 'type/num/num']: $true))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_43', ax, (('const/Past_Temporal_Logic/PEVENTUAL' (^[t : 'type/num/num']: $false)) = (^[t : 'type/num/num']: $false))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_44', ax, (![b : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' (^[t : 'type/num/num']: $false) b) = b))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_45', ax, (![b : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' (^[t : 'type/num/num']: $true) b) = ('const/Past_Temporal_Logic/PEVENTUAL' b)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_46', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' a (^[t : 'type/num/num']: $false)) = (^[t : 'type/num/num']: $false)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_47', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' a (^[t : 'type/num/num']: $true)) = (^[t : 'type/num/num']: $true)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_48', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' a a) = a))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_49', ax, (![b : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PUNTIL' (^[t : 'type/num/num']: $false) b) = b))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_50', ax, (![b : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PUNTIL' (^[t : 'type/num/num']: $true) b) = (^[t : 'type/num/num']: $true)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_51', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PUNTIL' a (^[t : 'type/num/num']: $false)) = ('const/Past_Temporal_Logic/PALWAYS' a)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_52', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PUNTIL' a (^[t : 'type/num/num']: $true)) = (^[t : 'type/num/num']: $true)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_53', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PUNTIL' a a) = a))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_54', ax, (![b : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSWHEN' (^[t : 'type/num/num']: $false) b) = (^[t : 'type/num/num']: $false)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_55', ax, (![b : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSWHEN' (^[t : 'type/num/num']: $true) b) = ('const/Past_Temporal_Logic/PEVENTUAL' b)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_56', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSWHEN' a (^[t : 'type/num/num']: $false)) = (^[t : 'type/num/num']: $false)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_57', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSWHEN' a (^[t : 'type/num/num']: $true)) = a))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_58', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSWHEN' a a) = ('const/Past_Temporal_Logic/PEVENTUAL' a)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_59', ax, (![b : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PWHEN' (^[t : 'type/num/num']: $false) b) = ('const/Past_Temporal_Logic/PALWAYS' (^[t : 'type/num/num']: (~ (b t))))))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_60', ax, (![b : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PWHEN' (^[t : 'type/num/num']: $true) b) = (^[t : 'type/num/num']: $true)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_61', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PWHEN' a (^[t : 'type/num/num']: $false)) = (^[t : 'type/num/num']: $true)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_62', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PWHEN' a (^[t : 'type/num/num']: $true)) = a))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_63', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PWHEN' a a) = (^[t : 'type/num/num']: $true)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_64', ax, (![b : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSBEFORE' (^[t : 'type/num/num']: $false) b) = (^[t : 'type/num/num']: $false)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_65', ax, (![b : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSBEFORE' (^[t : 'type/num/num']: $true) b) = (^[t : 'type/num/num']: (~ (b t)))))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_66', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSBEFORE' a (^[t : 'type/num/num']: $false)) = ('const/Past_Temporal_Logic/PEVENTUAL' a)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_67', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSBEFORE' a (^[t : 'type/num/num']: $true)) = (^[t : 'type/num/num']: $false)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_68', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSBEFORE' a a) = (^[t : 'type/num/num']: $false)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_69', ax, (![b : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PBEFORE' (^[t : 'type/num/num']: $false) b) = ('const/Past_Temporal_Logic/PALWAYS' (^[t : 'type/num/num']: (~ (b t))))))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_70', ax, (![b : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PBEFORE' (^[t : 'type/num/num']: $true) b) = (^[t : 'type/num/num']: (~ (b t)))))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_71', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PBEFORE' a (^[t : 'type/num/num']: $false)) = (^[t : 'type/num/num']: $true)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_72', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PBEFORE' a (^[t : 'type/num/num']: $true)) = (^[t : 'type/num/num']: $false)))).
tt('thm/Past_Temporal_Logic/SIMPLIFY_e73', ax, (![a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PBEFORE' a a) = ('const/Past_Temporal_Logic/PALWAYS' (^[t : 'type/num/num']: (~ (a t))))))).
tt('thm/Past_Temporal_Logic/MORE_EVENT_0', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/WHEN' a b) = ('const/Temporal_Logic/WHEN' (^[t : 'type/num/num']: ((a t) & (b t))) b)))).
tt('thm/Past_Temporal_Logic/MORE_EVENT_1', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/UNTIL' a b) = ('const/Temporal_Logic/UNTIL' (^[t : 'type/num/num']: ((a t) & (~ (b t)))) b)))).
tt('thm/Past_Temporal_Logic/MORE_EVENT_2', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' a b) = ('const/Temporal_Logic/BEFORE' (^[t : 'type/num/num']: ((a t) & (~ (b t)))) b)))).
tt('thm/Past_Temporal_Logic/MORE_EVENT_3', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SWHEN' a b) = ('const/Temporal_Logic/SWHEN' (^[t : 'type/num/num']: ((a t) & (b t))) b)))).
tt('thm/Past_Temporal_Logic/MORE_EVENT_4', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' a b) = ('const/Temporal_Logic/SUNTIL' (^[t : 'type/num/num']: ((a t) & (~ (b t)))) b)))).
tt('thm/Past_Temporal_Logic/MORE_EVENT_5', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SBEFORE' a b) = ('const/Temporal_Logic/SBEFORE' (^[t : 'type/num/num']: ((a t) & (~ (b t)))) b)))).
tt('thm/Past_Temporal_Logic/MORE_EVENT_6', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PWHEN' a b) = ('const/Past_Temporal_Logic/PWHEN' (^[t : 'type/num/num']: ((a t) & (b t))) b)))).
tt('thm/Past_Temporal_Logic/MORE_EVENT_7', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PUNTIL' a b) = ('const/Past_Temporal_Logic/PUNTIL' (^[t : 'type/num/num']: ((a t) & (~ (b t)))) b)))).
tt('thm/Past_Temporal_Logic/MORE_EVENT_8', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PBEFORE' a b) = ('const/Past_Temporal_Logic/PBEFORE' (^[t : 'type/num/num']: ((a t) & (~ (b t)))) b)))).
tt('thm/Past_Temporal_Logic/MORE_EVENT_9', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSWHEN' a b) = ('const/Past_Temporal_Logic/PSWHEN' (^[t : 'type/num/num']: ((a t) & (b t))) b)))).
tt('thm/Past_Temporal_Logic/MORE_EVENT_10', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' a b) = ('const/Past_Temporal_Logic/PSUNTIL' (^[t : 'type/num/num']: ((a t) & (~ (b t)))) b)))).
tt('thm/Past_Temporal_Logic/MORE_EVENT_e11', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSBEFORE' a b) = ('const/Past_Temporal_Logic/PSBEFORE' (^[t : 'type/num/num']: ((a t) & (~ (b t)))) b)))).
tt('thm/Past_Temporal_Logic/IMMEDIATE_EVENT_', ax, (![t : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((b t) => ((('const/Temporal_Logic/WHEN' a b t) = (a t)) & ((('const/Temporal_Logic/UNTIL' a b t) = $true) & ((('const/Temporal_Logic/BEFORE' a b t) = $false) & ((('const/Temporal_Logic/BEFORE' b a t) = (~ (a t))) & ((('const/Temporal_Logic/SWHEN' a b t) = (a t)) & ((('const/Temporal_Logic/SUNTIL' a b t) = $true) & ((('const/Temporal_Logic/SBEFORE' a b t) = $false) & ((('const/Temporal_Logic/SBEFORE' b a t) = (~ (a t))) & ((('const/Past_Temporal_Logic/PWHEN' a b t) = (a t)) & ((('const/Past_Temporal_Logic/PUNTIL' a b t) = $true) & ((('const/Past_Temporal_Logic/PBEFORE' a b t) = $false) & ((('const/Past_Temporal_Logic/PBEFORE' b a t) = (~ (a t))) & ((('const/Past_Temporal_Logic/PSWHEN' a b t) = (a t)) & ((('const/Past_Temporal_Logic/PSUNTIL' a b t) = $true) & ((('const/Past_Temporal_Logic/PSBEFORE' a b t) = $false) & (('const/Past_Temporal_Logic/PSBEFORE' b a t) = (~ (a t))))))))))))))))))))).
tt('thm/Past_Temporal_Logic/NO_FUTURE_EVENT_', ax, (![t0 : 'type/num/num', b : ('type/num/num' > $o)]: (('const/Temporal_Logic/ALWAYS' (^[t : 'type/num/num']: (~ (b t))) t0) => ((![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/WHEN' a b t0) = $true)) & ((![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/UNTIL' a b t0) = ('const/Temporal_Logic/ALWAYS' a t0))) & ((![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' a b t0) = $true)) & ((![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SWHEN' a b t0) = $false)) & ((![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' a b t0) = $false)) & (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SBEFORE' a b t0) = ('const/Temporal_Logic/EVENTUAL' a t0))))))))))).
tt('thm/Past_Temporal_Logic/NO_PAST_EVENT_', ax, (![t : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PALWAYS' (^[t0 : 'type/num/num']: (~ (b t0))) t) => ((('const/Past_Temporal_Logic/PWHEN' a b t) = $true) & ((('const/Past_Temporal_Logic/PUNTIL' a b t) = ('const/Past_Temporal_Logic/PALWAYS' a t)) & ((('const/Past_Temporal_Logic/PBEFORE' a b t) = $true) & ((('const/Past_Temporal_Logic/PBEFORE' b a t) = ('const/Past_Temporal_Logic/PALWAYS' (^[t0 : 'type/num/num']: (~ (a t0))) t)) & ((('const/Past_Temporal_Logic/PSWHEN' a b t) = $false) & ((('const/Past_Temporal_Logic/PSUNTIL' a b t) = $false) & ((('const/Past_Temporal_Logic/PSBEFORE' a b t) = ('const/Past_Temporal_Logic/PEVENTUAL' a t)) & (('const/Past_Temporal_Logic/PSBEFORE' b a t) = $false))))))))))).
tt('thm/Past_Temporal_Logic/SOME_FUTURE_EVENT_0', ax, (![t0 : 'type/num/num', b : ('type/num/num' > $o)]: (('const/Temporal_Logic/EVENTUAL' b t0) = (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/WHEN' a b t0) = ('const/Temporal_Logic/SWHEN' a b t0)))))).
tt('thm/Past_Temporal_Logic/SOME_FUTURE_EVENT_1', ax, (![t0 : 'type/num/num', b : ('type/num/num' > $o)]: (('const/Temporal_Logic/EVENTUAL' b t0) = (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/UNTIL' a b t0) = ('const/Temporal_Logic/SUNTIL' a b t0)))))).
tt('thm/Past_Temporal_Logic/SOME_FUTURE_EVENT_e2', ax, (![t0 : 'type/num/num', b : ('type/num/num' > $o)]: (('const/Temporal_Logic/EVENTUAL' b t0) = (![a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' a b t0) = ('const/Temporal_Logic/SBEFORE' a b t0)))))).
tt('thm/Past_Temporal_Logic/SOME_PAST_EVENT_', ax, (![t : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PEVENTUAL' b t) => ((('const/Past_Temporal_Logic/PWHEN' a b t) = ('const/Past_Temporal_Logic/PSWHEN' a b t)) & ((('const/Past_Temporal_Logic/PUNTIL' a b t) = ('const/Past_Temporal_Logic/PSUNTIL' a b t)) & ((('const/Past_Temporal_Logic/PBEFORE' a b t) = ('const/Past_Temporal_Logic/PSBEFORE' a b t)) & (('const/Past_Temporal_Logic/PBEFORE' b a t) = ('const/Past_Temporal_Logic/PSBEFORE' b a t)))))))).
tt('thm/Past_Temporal_Logic/SEPARATE_NEXT_THM_0', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' (^[t : 'type/num/num']: ((a t) & ('const/Past_Temporal_Logic/PNEXT' b t)))) = (^[t : 'type/num/num']: ((b t) & ('const/Temporal_Logic/NEXT' a t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_NEXT_THM_1', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' (^[t : 'type/num/num']: ((a t) & ('const/Past_Temporal_Logic/PSNEXT' b t)))) = (^[t : 'type/num/num']: ((b t) & ('const/Temporal_Logic/NEXT' a t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_NEXT_THM_2', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' (^[t : 'type/num/num']: ((a t) & ('const/Past_Temporal_Logic/PSUNTIL' b c t)))) = (^[t : 'type/num/num']: (('const/Temporal_Logic/NEXT' (^[t0 : 'type/num/num']: ((a t0) & (c t0))) t) | (('const/Past_Temporal_Logic/PSUNTIL' b c t) & ('const/Temporal_Logic/NEXT' (^[t0 : 'type/num/num']: ((a t0) & (b t0))) t))))))).
tt('thm/Past_Temporal_Logic/SEPARATE_NEXT_THM_3', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' (^[t : 'type/num/num']: ((a t) & ('const/Past_Temporal_Logic/PBEFORE' b c t)))) = (^[t : 'type/num/num']: (('const/Temporal_Logic/NEXT' (^[t0 : 'type/num/num']: ((a t0) & ((b t0) & (~ (c t0))))) t) | (('const/Past_Temporal_Logic/PBEFORE' b c t) & ('const/Temporal_Logic/NEXT' (^[t0 : 'type/num/num']: ((a t0) & (~ (c t0)))) t))))))).
tt('thm/Past_Temporal_Logic/SEPARATE_NEXT_THM_4', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' (^[t : 'type/num/num']: ((a t) | ('const/Past_Temporal_Logic/PNEXT' b t)))) = (^[t : 'type/num/num']: ((b t) | ('const/Temporal_Logic/NEXT' a t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_NEXT_THM_5', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' (^[t : 'type/num/num']: ((a t) | ('const/Past_Temporal_Logic/PSNEXT' b t)))) = (^[t : 'type/num/num']: ((b t) | ('const/Temporal_Logic/NEXT' a t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_NEXT_THM_6', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' (^[t : 'type/num/num']: ((a t) | ('const/Past_Temporal_Logic/PSUNTIL' b c t)))) = (^[t : 'type/num/num']: (('const/Temporal_Logic/NEXT' (^[t0 : 'type/num/num']: ((a t0) | (c t0))) t) | (('const/Past_Temporal_Logic/PSUNTIL' b c t) & ('const/Temporal_Logic/NEXT' b t))))))).
tt('thm/Past_Temporal_Logic/SEPARATE_NEXT_THM_e7', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' (^[t : 'type/num/num']: ((a t) | ('const/Past_Temporal_Logic/PBEFORE' b c t)))) = (^[t : 'type/num/num']: (('const/Temporal_Logic/NEXT' (^[t0 : 'type/num/num']: ((a t0) | (~ (c t0)))) t) & (('const/Past_Temporal_Logic/PBEFORE' b c t) | ('const/Temporal_Logic/NEXT' (^[t0 : 'type/num/num']: ((a t0) | (b t0))) t))))))).
tt('thm/Past_Temporal_Logic/SEPARATE_SUNTIL_THM_0', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' a (^[t : 'type/num/num']: ((b t) | (c t)))) = (^[t : 'type/num/num']: (('const/Temporal_Logic/SUNTIL' a b t) | ('const/Temporal_Logic/SUNTIL' a c t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_SUNTIL_THM_1', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' a (^[t : 'type/num/num']: ((b t) & ('const/Past_Temporal_Logic/PNEXT' c t)))) = (^[t : 'type/num/num']: (((b t) & ('const/Past_Temporal_Logic/PNEXT' c t)) | ('const/Temporal_Logic/SUNTIL' a (^[t0 : 'type/num/num']: ((a t0) & ((c t0) & ('const/Temporal_Logic/NEXT' b t0)))) t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_SUNTIL_THM_2', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' a (^[t : 'type/num/num']: ((b t) & ('const/Past_Temporal_Logic/PSNEXT' c t)))) = (^[t : 'type/num/num']: (((b t) & ('const/Past_Temporal_Logic/PSNEXT' c t)) | ('const/Temporal_Logic/SUNTIL' a (^[t0 : 'type/num/num']: ((a t0) & ((c t0) & ('const/Temporal_Logic/NEXT' b t0)))) t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_SUNTIL_THM_3', ax, (![d : ('type/num/num' > $o), c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' a (^[t : 'type/num/num']: ((b t) & ('const/Past_Temporal_Logic/PSUNTIL' c d t)))) = (^[t : 'type/num/num']: ((('const/Past_Temporal_Logic/PSUNTIL' c d t) & ('const/Temporal_Logic/SUNTIL' (^[t0 : 'type/num/num']: ((a t0) & ('const/Temporal_Logic/NEXT' c t0))) b t)) | ('const/Temporal_Logic/SUNTIL' a (^[t0 : 'type/num/num']: ((d t0) & ('const/Temporal_Logic/SUNTIL' (^[t1 : 'type/num/num']: ((a t1) & ('const/Temporal_Logic/NEXT' c t1))) b t0))) t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_SUNTIL_THM_4', ax, (![d : ('type/num/num' > $o), c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' a (^[t : 'type/num/num']: ((b t) & ('const/Past_Temporal_Logic/PBEFORE' c d t)))) = (^[t : 'type/num/num']: ((('const/Past_Temporal_Logic/PBEFORE' c d t) & ('const/Temporal_Logic/SUNTIL' (^[t0 : 'type/num/num']: ((a t0) & (~ ('const/Temporal_Logic/NEXT' d t0)))) b t)) | ('const/Temporal_Logic/SUNTIL' a (^[t0 : 'type/num/num']: ((c t0) & ((~ (d t0)) & ('const/Temporal_Logic/SUNTIL' (^[t1 : 'type/num/num']: ((a t1) & (~ ('const/Temporal_Logic/NEXT' d t1)))) b t0)))) t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_SUNTIL_THM_5', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' (^[t : 'type/num/num']: ((a t) & (b t))) c) = (^[t : 'type/num/num']: (('const/Temporal_Logic/SUNTIL' a c t) & ('const/Temporal_Logic/SUNTIL' b c t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_SUNTIL_THM_6', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' (^[t : 'type/num/num']: ((a t) | ('const/Past_Temporal_Logic/PNEXT' b t))) c) = (^[t : 'type/num/num']: ((c t) | (((a t) | ('const/Past_Temporal_Logic/PNEXT' b t)) & ('const/Temporal_Logic/SUNTIL' (^[t0 : 'type/num/num']: ((b t0) | ('const/Temporal_Logic/NEXT' a t0))) ('const/Temporal_Logic/NEXT' c) t))))))).
tt('thm/Past_Temporal_Logic/SEPARATE_SUNTIL_THM_7', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' (^[t : 'type/num/num']: ((a t) | ('const/Past_Temporal_Logic/PSNEXT' b t))) c) = (^[t : 'type/num/num']: ((c t) | (((a t) | ('const/Past_Temporal_Logic/PSNEXT' b t)) & ('const/Temporal_Logic/SUNTIL' (^[t0 : 'type/num/num']: ((b t0) | ('const/Temporal_Logic/NEXT' a t0))) ('const/Temporal_Logic/NEXT' c) t))))))).
tt('thm/Past_Temporal_Logic/SEPARATE_SUNTIL_THM_8', ax, (![d : ('type/num/num' > $o), c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' (^[t : 'type/num/num']: ((a t) | ('const/Past_Temporal_Logic/PSUNTIL' b c t))) d) = (^[t : 'type/num/num']: ((('const/Past_Temporal_Logic/PSUNTIL' b c t) | ('const/Temporal_Logic/BEFORE' (^[t0 : 'type/num/num']: ((d t0) | ('const/Temporal_Logic/NEXT' c t0))) (^[t0 : 'type/num/num']: ((~ (a t0)) & (~ (d t0)))) t)) & ('const/Temporal_Logic/SUNTIL' (^[t0 : 'type/num/num']: ((b t0) | ((c t0) | ('const/Temporal_Logic/BEFORE' (^[t1 : 'type/num/num']: ((d t1) | ('const/Temporal_Logic/NEXT' c t1))) (^[t1 : 'type/num/num']: ((~ (a t1)) & (~ (d t1)))) t0)))) d t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_SUNTIL_THM_e9', ax, (![d : ('type/num/num' > $o), c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' (^[t : 'type/num/num']: ((a t) | ('const/Past_Temporal_Logic/PBEFORE' b c t))) d) = (^[t : 'type/num/num']: ((('const/Past_Temporal_Logic/PBEFORE' b c t) | ('const/Temporal_Logic/BEFORE' (^[t0 : 'type/num/num']: ((d t0) | ('const/Temporal_Logic/NEXT' b t0))) (^[t0 : 'type/num/num']: ((~ (a t0)) & (~ (d t0)))) t)) & ('const/Temporal_Logic/SUNTIL' (^[t0 : 'type/num/num']: ((~ (c t0)) | ('const/Temporal_Logic/BEFORE' (^[t1 : 'type/num/num']: ((d t1) | ('const/Temporal_Logic/NEXT' b t1))) (^[t1 : 'type/num/num']: ((~ (a t1)) & (~ (d t1)))) t0))) d t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_BEFORE_THM_0', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' a (^[t : 'type/num/num']: ((b t) | (c t)))) = (^[t : 'type/num/num']: (('const/Temporal_Logic/BEFORE' a b t) & ('const/Temporal_Logic/BEFORE' a c t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_BEFORE_THM_1', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' (^[t : 'type/num/num']: ((a t) | (b t))) c) = (^[t : 'type/num/num']: (('const/Temporal_Logic/BEFORE' a c t) | ('const/Temporal_Logic/BEFORE' b c t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_BEFORE_THM_2', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' a (^[t : 'type/num/num']: ((b t) & ('const/Past_Temporal_Logic/PNEXT' c t)))) = (^[t : 'type/num/num']: ((~ ((b t) & ('const/Past_Temporal_Logic/PNEXT' c t))) & ((a t) | ('const/Temporal_Logic/BEFORE' ('const/Temporal_Logic/NEXT' a) (^[t0 : 'type/num/num']: ((c t0) & ('const/Temporal_Logic/NEXT' b t0))) t))))))).
tt('thm/Past_Temporal_Logic/SEPARATE_BEFORE_THM_3', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' a (^[t : 'type/num/num']: ((b t) & ('const/Past_Temporal_Logic/PSNEXT' c t)))) = (^[t : 'type/num/num']: ((~ ((b t) & ('const/Past_Temporal_Logic/PSNEXT' c t))) & ((a t) | ('const/Temporal_Logic/BEFORE' ('const/Temporal_Logic/NEXT' a) (^[t0 : 'type/num/num']: ((c t0) & ('const/Temporal_Logic/NEXT' b t0))) t))))))).
tt('thm/Past_Temporal_Logic/SEPARATE_BEFORE_THM_4', ax, (![d : ('type/num/num' > $o), c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' a (^[t : 'type/num/num']: ((b t) & ('const/Past_Temporal_Logic/PSUNTIL' c d t)))) = (^[t : 'type/num/num']: ((('const/Past_Temporal_Logic/PBEFORE' (^[t0 : 'type/num/num']: (~ (c t0))) d t) | ('const/Temporal_Logic/BEFORE' (^[t0 : 'type/num/num']: ((a t0) | (~ ('const/Temporal_Logic/NEXT' c t0)))) b t)) & ('const/Temporal_Logic/BEFORE' a (^[t0 : 'type/num/num']: ((d t0) & ('const/Temporal_Logic/SUNTIL' (^[t1 : 'type/num/num']: ((~ (a t1)) & ('const/Temporal_Logic/NEXT' c t1))) b t0))) t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_BEFORE_THM_5', ax, (![d : ('type/num/num' > $o), c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' a (^[t : 'type/num/num']: ((b t) & ('const/Past_Temporal_Logic/PBEFORE' c d t)))) = (^[t : 'type/num/num']: ((('const/Past_Temporal_Logic/PSUNTIL' (^[t0 : 'type/num/num']: (~ (c t0))) d t) | ('const/Temporal_Logic/BEFORE' (^[t0 : 'type/num/num']: ((a t0) | ('const/Temporal_Logic/NEXT' d t0))) b t)) & ('const/Temporal_Logic/BEFORE' a (^[t0 : 'type/num/num']: ((c t0) & ((~ (d t0)) & ('const/Temporal_Logic/SUNTIL' (^[t1 : 'type/num/num']: ((~ (a t1)) & (~ ('const/Temporal_Logic/NEXT' d t1)))) b t0)))) t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_BEFORE_THM_6', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' (^[t : 'type/num/num']: ((a t) & ('const/Past_Temporal_Logic/PNEXT' b t))) c) = (^[t : 'type/num/num']: (((~ (c t)) & ((a t) & ('const/Past_Temporal_Logic/PNEXT' b t))) | ((~ (c t)) & ('const/Temporal_Logic/BEFORE' (^[t0 : 'type/num/num']: ((b t0) & ('const/Temporal_Logic/NEXT' a t0))) ('const/Temporal_Logic/NEXT' c) t))))))).
tt('thm/Past_Temporal_Logic/SEPARATE_BEFORE_THM_7', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' (^[t : 'type/num/num']: ((a t) & ('const/Past_Temporal_Logic/PSNEXT' b t))) c) = (^[t : 'type/num/num']: (((~ (c t)) & ((a t) & ('const/Past_Temporal_Logic/PSNEXT' b t))) | ((~ (c t)) & ('const/Temporal_Logic/BEFORE' (^[t0 : 'type/num/num']: ((b t0) & ('const/Temporal_Logic/NEXT' a t0))) ('const/Temporal_Logic/NEXT' c) t))))))).
tt('thm/Past_Temporal_Logic/SEPARATE_BEFORE_THM_8', ax, (![d : ('type/num/num' > $o), c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' (^[t : 'type/num/num']: ((a t) & ('const/Past_Temporal_Logic/PBEFORE' b c t))) d) = (^[t : 'type/num/num']: ((('const/Past_Temporal_Logic/PBEFORE' b c t) & ('const/Temporal_Logic/SUNTIL' (^[t0 : 'type/num/num']: ((~ (d t0)) & (~ ('const/Temporal_Logic/NEXT' c t0)))) (^[t0 : 'type/num/num']: ((a t0) & (~ (d t0)))) t)) | ('const/Temporal_Logic/BEFORE' (^[t0 : 'type/num/num']: ((b t0) & ((~ (c t0)) & ('const/Temporal_Logic/SUNTIL' (^[t1 : 'type/num/num']: ((~ (d t1)) & (~ ('const/Temporal_Logic/NEXT' c t1)))) (^[t1 : 'type/num/num']: ((a t1) & (~ (d t1)))) t0)))) d t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_BEFORE_THM_e9', ax, (![d : ('type/num/num' > $o), c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' (^[t : 'type/num/num']: ((a t) & ('const/Past_Temporal_Logic/PSUNTIL' b c t))) d) = (^[t : 'type/num/num']: ((('const/Past_Temporal_Logic/PSUNTIL' b c t) & ('const/Temporal_Logic/SUNTIL' (^[t0 : 'type/num/num']: ((~ (d t0)) & ('const/Temporal_Logic/NEXT' b t0))) (^[t0 : 'type/num/num']: ((a t0) & (~ (d t0)))) t)) | ('const/Temporal_Logic/BEFORE' (^[t0 : 'type/num/num']: ((c t0) & ('const/Temporal_Logic/SUNTIL' (^[t1 : 'type/num/num']: ((~ (d t1)) & ('const/Temporal_Logic/NEXT' b t1))) (^[t1 : 'type/num/num']: ((a t1) & (~ (d t1)))) t0))) d t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_PNEXT_THM_0', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' (^[t : 'type/num/num']: ((a t) & ('const/Temporal_Logic/NEXT' b t)))) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/InitPoint' t) | ((b t) & ('const/Past_Temporal_Logic/PNEXT' a t))))))).
tt('thm/Past_Temporal_Logic/SEPARATE_PNEXT_THM_1', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' (^[t : 'type/num/num']: ((a t) & ('const/Temporal_Logic/SUNTIL' b c t)))) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PNEXT' (^[t0 : 'type/num/num']: ((a t0) & (c t0))) t) | (('const/Temporal_Logic/SUNTIL' b c t) & ('const/Past_Temporal_Logic/PNEXT' (^[t0 : 'type/num/num']: ((a t0) & (b t0))) t))))))).
tt('thm/Past_Temporal_Logic/SEPARATE_PNEXT_THM_2', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' (^[t : 'type/num/num']: ((a t) & ('const/Temporal_Logic/BEFORE' b c t)))) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PNEXT' (^[t0 : 'type/num/num']: ((a t0) & ((b t0) & (~ (c t0))))) t) | (('const/Temporal_Logic/BEFORE' b c t) & ('const/Past_Temporal_Logic/PNEXT' (^[t0 : 'type/num/num']: ((a t0) & (~ (c t0)))) t))))))).
tt('thm/Past_Temporal_Logic/SEPARATE_PNEXT_THM_3', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' (^[t : 'type/num/num']: ((a t) | ('const/Temporal_Logic/NEXT' b t)))) = (^[t : 'type/num/num']: ((b t) | ('const/Past_Temporal_Logic/PNEXT' a t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_PNEXT_THM_4', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' (^[t : 'type/num/num']: ((a t) | ('const/Temporal_Logic/SUNTIL' b c t)))) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PNEXT' (^[t0 : 'type/num/num']: ((a t0) | (c t0))) t) | (('const/Temporal_Logic/SUNTIL' b c t) & ('const/Past_Temporal_Logic/PNEXT' b t))))))).
tt('thm/Past_Temporal_Logic/SEPARATE_PNEXT_THM_e5', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PNEXT' (^[t : 'type/num/num']: ((a t) | ('const/Temporal_Logic/BEFORE' b c t)))) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PNEXT' (^[t0 : 'type/num/num']: ((a t0) | (~ (c t0)))) t) & (('const/Temporal_Logic/BEFORE' b c t) | ('const/Past_Temporal_Logic/PNEXT' (^[t0 : 'type/num/num']: ((a t0) | (b t0))) t))))))).
tt('thm/Past_Temporal_Logic/SEPARATE_PSUNTIL_THM_0', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' a (^[t : 'type/num/num']: ((b t) | (c t)))) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PSUNTIL' a b t) | ('const/Past_Temporal_Logic/PSUNTIL' a c t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_PSUNTIL_THM_1', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' a (^[t : 'type/num/num']: ((b t) & ('const/Temporal_Logic/NEXT' c t)))) = (^[t : 'type/num/num']: (((b t) & ('const/Temporal_Logic/NEXT' c t)) | ('const/Past_Temporal_Logic/PSUNTIL' a (^[t0 : 'type/num/num']: ((a t0) & ((c t0) & ('const/Past_Temporal_Logic/PSNEXT' b t0)))) t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_PSUNTIL_THM_2', ax, (![d : ('type/num/num' > $o), c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' a (^[t : 'type/num/num']: ((b t) & ('const/Temporal_Logic/SUNTIL' c d t)))) = (^[t : 'type/num/num']: ((('const/Temporal_Logic/SUNTIL' c d t) & ('const/Past_Temporal_Logic/PSUNTIL' (^[t0 : 'type/num/num']: ((a t0) & ('const/Past_Temporal_Logic/PNEXT' c t0))) b t)) | ('const/Past_Temporal_Logic/PSUNTIL' a (^[t0 : 'type/num/num']: ((d t0) & ('const/Past_Temporal_Logic/PSUNTIL' (^[t1 : 'type/num/num']: ((a t1) & ('const/Past_Temporal_Logic/PNEXT' c t1))) b t0))) t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_PSUNTIL_THM_3', ax, (![d : ('type/num/num' > $o), c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' a (^[t : 'type/num/num']: ((b t) & ('const/Temporal_Logic/BEFORE' c d t)))) = (^[t : 'type/num/num']: ((('const/Temporal_Logic/BEFORE' c d t) & ('const/Past_Temporal_Logic/PSUNTIL' (^[t0 : 'type/num/num']: ((a t0) & (~ ('const/Past_Temporal_Logic/PNEXT' d t0)))) b t)) | ('const/Past_Temporal_Logic/PSUNTIL' a (^[t0 : 'type/num/num']: ((c t0) & ((~ (d t0)) & ('const/Past_Temporal_Logic/PSUNTIL' (^[t1 : 'type/num/num']: ((a t1) & (~ ('const/Past_Temporal_Logic/PNEXT' d t1)))) b t0)))) t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_PSUNTIL_THM_4', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' (^[t : 'type/num/num']: ((a t) & (b t))) c) = (^[t : 'type/num/num']: (('const/Past_Temporal_Logic/PSUNTIL' a c t) & ('const/Past_Temporal_Logic/PSUNTIL' b c t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_PSUNTIL_THM_5', ax, (![c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' (^[t : 'type/num/num']: ((a t) | ('const/Temporal_Logic/NEXT' b t))) c) = (^[t : 'type/num/num']: ((c t) | (((a t) | ('const/Temporal_Logic/NEXT' b t)) & ('const/Past_Temporal_Logic/PSUNTIL' (^[t0 : 'type/num/num']: ((b t0) | ('const/Past_Temporal_Logic/PNEXT' a t0))) ('const/Past_Temporal_Logic/PSNEXT' c) t))))))).
tt('thm/Past_Temporal_Logic/SEPARATE_PSUNTIL_THM_6', ax, (![d : ('type/num/num' > $o), c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' (^[t : 'type/num/num']: ((a t) | ('const/Temporal_Logic/SUNTIL' b c t))) d) = (^[t : 'type/num/num']: ((('const/Temporal_Logic/SUNTIL' b c t) | ('const/Past_Temporal_Logic/PBEFORE' (^[t0 : 'type/num/num']: ((d t0) | ('const/Past_Temporal_Logic/PNEXT' c t0))) (^[t0 : 'type/num/num']: ((~ (a t0)) & (~ (d t0)))) t)) & ('const/Past_Temporal_Logic/PSUNTIL' (^[t0 : 'type/num/num']: ((b t0) | ((c t0) | ('const/Past_Temporal_Logic/PBEFORE' (^[t1 : 'type/num/num']: ((d t1) | ('const/Past_Temporal_Logic/PNEXT' c t1))) (^[t1 : 'type/num/num']: ((~ (a t1)) & (~ (d t1)))) t0)))) d t)))))).
tt('thm/Past_Temporal_Logic/SEPARATE_PSUNTIL_THM_e7', ax, (![d : ('type/num/num' > $o), c : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Past_Temporal_Logic/PSUNTIL' (^[t : 'type/num/num']: ((a t) | ('const/Temporal_Logic/BEFORE' b c t))) d) = (^[t : 'type/num/num']: ((('const/Temporal_Logic/BEFORE' b c t) | ('const/Past_Temporal_Logic/PBEFORE' (^[t0 : 'type/num/num']: ((d t0) | ('const/Past_Temporal_Logic/PSNEXT' b t0))) (^[t0 : 'type/num/num']: ((~ (a t0)) & (~ (d t0)))) t)) & ('const/Past_Temporal_Logic/PSUNTIL' (^[t0 : 'type/num/num']: ((~ (c t0)) | ('const/Past_Temporal_Logic/PBEFORE' (^[t1 : 'type/num/num']: ((d t1) | ('const/Past_Temporal_Logic/PSNEXT' b t1))) (^[t1 : 'type/num/num']: ((~ (a t1)) & (~ (d t1)))) t0))) d t)))))).
