Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
%%%%% bool.elf %%%%% Boolean literals %%%%% John Boyland %%%% Definitions bool : type. true : bool. false : bool. %freeze bool. eq : bool -> bool -> type. eq/ : eq B B. ne : bool -> bool -> type. ne/TF : ne true false. ne/FT : ne false true. eq? : bool -> bool -> bool -> type. eq?/yes : eq? B B true. eq?/no : eq? B1 B2 false <- ne B1 B2. %%%% Theorems %%% theorems about eq %theorem false-implies-eq : forall* {X1} {X2} forall {F:void} exists {E:eq X1 X2} true. %worlds () (false-implies-eq _ _). %total { } (false-implies-eq _ _). %theorem meta-eq : forall {X1} {X2} {E:eq X1 X2} true. - : meta-eq _ _ eq/. %worlds () (meta-eq _ _ _). %total { } (meta-eq _ _ _). %reduces X = Y (meta-eq X Y _). %theorem eq-reflexive : forall {X} exists {E:eq X X} true. - : eq-reflexive _ eq/. %worlds () (eq-reflexive _ _). %total { } (eq-reflexive _ _). %theorem eq-symmetric : forall* {X} {Y} forall {E:eq X Y} exists {F:eq Y X} true. - : eq-symmetric (eq/) (eq/). %worlds () (eq-symmetric _ _). %total { } (eq-symmetric _ _). %theorem eq-transitive : forall* {X} {Y} {Z} forall {E1:eq X Y} {E2:eq Y Z} exists {F:eq X Z} true. - : eq-transitive (eq/) (eq/) (eq/). %worlds () (eq-transitive _ _ _). %total { } (eq-transitive _ _ _). %%% theorems about ne %theorem false-implies-ne : forall* {X1} {X2} forall {F:void} exists {G:ne X1 X2} true. %worlds () (false-implies-ne _ _). %total { } (false-implies-ne _ _). %theorem ne-respects-eq : forall* {X1} {X2} {Y1} {Y2} forall {D1:ne X1 X2} {E1:eq X1 Y1} {E2:eq X2 Y2} exists {D2:ne Y1 Y2} true. - : ne-respects-eq X1<>X2 eq/ eq/ X1<>X2. %worlds () (ne-respects-eq _ _ _ _). %total { } (ne-respects-eq _ _ _ _). %theorem ne-anti-reflexive : forall* {B} forall {R:ne B B} exists {F:void} true. %worlds () (ne-anti-reflexive _ _). %total { } (ne-anti-reflexive _ _). %theorem ne-symmetric : forall* {B1} {B2} forall {R1:ne B1 B2} exists {R2:ne B2 B1} true. - : ne-symmetric ne/TF ne/FT. - : ne-symmetric ne/FT ne/TF. %worlds () (ne-symmetric _ _). %total { } (ne-symmetric _ _). %theorem eq-ne-implies-false : forall* {B1} {B2} forall {D1:eq B1 B2} {D2:ne B1 B2} exists {F:void} true. %worlds () (eq-ne-implies-false _ _ _). %total { } (eq-ne-implies-false _ _ _). %%% theorems about eq? %theorem eq?-total* : forall {B1} {B2} exists {B} {EQ?:eq? B1 B2 B} true. - : eq?-total* true true _ (eq?/yes). - : eq?-total* false false _ (eq?/yes). - : eq?-total* true false _ (eq?/no ne/TF). - : eq?-total* false true _ (eq?/no ne/FT). %worlds () (eq?-total* _ _ _ _). %total { } (eq?-total* _ _ _ _). %abbrev eq?-total = eq?-total* _ _ _. %abbrev bool`bool = bool. %abbrev bool`true = true. %abbrev bool`false = false. %abbrev bool`eq = eq. %abbrev bool`eq/ = eq/. %abbrev bool`ne = ne. %abbrev bool`ne/TF = ne/TF. %abbrev bool`ne/FT = ne/FT. %abbrev bool`eq? = eq?. %abbrev bool`eq?/yes = eq?/yes. %abbrev bool`eq?/no = eq?/no. %abbrev bool`false-implies-eq = false-implies-eq. %abbrev bool`meta-eq = meta-eq. %abbrev bool`eq-reflexive = eq-reflexive. %abbrev bool`eq-symmetric = eq-symmetric. %abbrev bool`eq-transitive = eq-transitive. %abbrev bool`false-implies-ne = false-implies-ne. %abbrev bool`ne-respects-eq = ne-respects-eq. %abbrev bool`ne-anti-reflexive = ne-anti-reflexive. %abbrev bool`ne-symmetric = ne-symmetric. %abbrev bool`eq-ne-implies-false = eq-ne-implies-false. %abbrev bool`eq?-total* = eq?-total*. %abbrev bool`eq?-total = eq?-total.