xboolean.miz

    begin

    definition

      :: XBOOLEAN:def1

      func FALSE -> object equals 0 ;

      coherence ;

      :: XBOOLEAN:def2

      func TRUE -> object equals 1;

      coherence ;

    end

    definition

      let p be object;

      :: XBOOLEAN:def3

      attr p is boolean means

      : Def3: p = FALSE or p = TRUE ;

    end

    registration

      cluster FALSE -> boolean;

      coherence ;

      cluster TRUE -> boolean;

      coherence ;

      cluster boolean for object;

      existence by Def3;

      cluster boolean -> natural for object;

      coherence ;

    end

    reserve p,q,r,s for boolean object;

    definition

      let p;

      :: XBOOLEAN:def4

      func 'not' p -> boolean object equals (1 - p);

      coherence

      proof

        p = FALSE or p = TRUE by Def3;

        hence thesis by Def3;

      end;

      involutiveness ;

      let q;

      :: XBOOLEAN:def5

      func p '&' q -> object equals (p * q);

      correctness ;

      commutativity ;

      idempotence

      proof

        let p;

        p = FALSE or p = TRUE by Def3;

        hence thesis;

      end;

    end

    registration

      let p, q;

      cluster (p '&' q) -> boolean;

      coherence

      proof

        p = FALSE or p = TRUE by Def3;

        hence thesis;

      end;

    end

    definition

      let p, q;

      :: XBOOLEAN:def6

      func p 'or' q -> object equals ( 'not' (( 'not' p) '&' ( 'not' q)));

      coherence ;

      commutativity ;

      idempotence ;

    end

    definition

      let p, q;

      :: XBOOLEAN:def7

      func p => q -> object equals (( 'not' p) 'or' q);

      coherence ;

    end

    registration

      let p, q;

      cluster (p 'or' q) -> boolean;

      coherence ;

      cluster (p => q) -> boolean;

      coherence ;

    end

    definition

      let p, q;

      :: XBOOLEAN:def8

      func p <=> q -> object equals ((p => q) '&' (q => p));

      coherence ;

      commutativity ;

    end

    registration

      let p, q;

      cluster (p <=> q) -> boolean;

      coherence ;

    end

    definition

      let p, q;

      :: XBOOLEAN:def9

      func p 'nand' q -> object equals ( 'not' (p '&' q));

      coherence ;

      commutativity ;

      :: XBOOLEAN:def10

      func p 'nor' q -> object equals ( 'not' (p 'or' q));

      coherence ;

      commutativity ;

      :: XBOOLEAN:def11

      func p 'xor' q -> object equals ( 'not' (p <=> q));

      coherence ;

      commutativity ;

      :: XBOOLEAN:def12

      func p '\' q -> object equals (p '&' ( 'not' q));

      coherence ;

    end

    registration

      let p, q;

      cluster (p 'nand' q) -> boolean;

      coherence ;

      cluster (p 'nor' q) -> boolean;

      coherence ;

      cluster (p 'xor' q) -> boolean;

      coherence ;

      cluster (p '\' q) -> boolean;

      coherence ;

    end

    begin

    theorem :: XBOOLEAN:1

    (p '&' p) = p;

    theorem :: XBOOLEAN:2

    (p '&' (p '&' q)) = (p '&' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:3

    (p 'or' p) = p;

    theorem :: XBOOLEAN:4

    (p 'or' (p 'or' q)) = (p 'or' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:5

    (p 'or' (p '&' q)) = p

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:6

    (p '&' (p 'or' q)) = p

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:7

    (p '&' (p 'or' q)) = (p 'or' (p '&' q))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:8

    (p '&' (q 'or' r)) = ((p '&' q) 'or' (p '&' r))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:9

    (p 'or' (q '&' r)) = ((p 'or' q) '&' (p 'or' r))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:10

    (((p '&' q) 'or' (q '&' r)) 'or' (r '&' p)) = (((p 'or' q) '&' (q 'or' r)) '&' (r 'or' p))

    proof



       A1: q = FALSE or q = TRUE by Def3;

      p = FALSE or p = TRUE by Def3;

      hence thesis by A1;

    end;

    theorem :: XBOOLEAN:11

    (p '&' (( 'not' p) 'or' q)) = (p '&' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:12

    (p 'or' (( 'not' p) '&' q)) = (p 'or' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:13

    (p => (p => q)) = (p => q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:14

    (p '&' (p => q)) = (p '&' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:15

    (p => (p '&' q)) = (p => q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:16

    (p '&' ( 'not' (p => q))) = (p '&' ( 'not' q))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:17

    (( 'not' p) 'or' (p => q)) = (p => q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:18

    (( 'not' p) '&' (p => q)) = (( 'not' p) 'or' (( 'not' p) '&' q))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:19

    ((p <=> q) <=> r) = (p <=> (q <=> r))

    proof

      q = FALSE or q = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:20

    (p '&' (p <=> q)) = (p '&' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:21

    (( 'not' p) '&' (p <=> q)) = (( 'not' p) '&' ( 'not' q))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:22

    (p '&' (q <=> r)) = ((p '&' (( 'not' q) 'or' r)) '&' (( 'not' r) 'or' q));

    theorem :: XBOOLEAN:23

    (p 'or' (q <=> r)) = (((p 'or' ( 'not' q)) 'or' r) '&' ((p 'or' ( 'not' r)) 'or' q))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:24

    (( 'not' p) '&' (p <=> q)) = ((( 'not' p) '&' ( 'not' q)) '&' (( 'not' p) 'or' q))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:25

    (( 'not' p) '&' (q <=> r)) = ((( 'not' p) '&' (( 'not' q) 'or' r)) '&' (( 'not' r) 'or' q));

    theorem :: XBOOLEAN:26

    (p => (p <=> q)) = (p => q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:27

    (p => (p <=> q)) = (p => (p => q))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:28

    (p 'or' (p <=> q)) = (q => p)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:29

    (( 'not' p) 'or' (p <=> q)) = (p => q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:30

    (p => (q <=> r)) = (((( 'not' p) 'or' ( 'not' q)) 'or' r) '&' ((( 'not' p) 'or' q) 'or' ( 'not' r)))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:31

    (p 'nor' p) = ( 'not' p);

    theorem :: XBOOLEAN:32

    (p 'nor' (p '&' q)) = ( 'not' p)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:33

    (p 'nor' (p 'or' q)) = (( 'not' p) '&' ( 'not' q))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:34

    (p 'nor' (p 'nor' q)) = (( 'not' p) '&' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:35

    (p 'nor' (p '&' q)) = ( 'not' p)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:36

    (p 'nor' (p 'or' q)) = (p 'nor' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:37

    (( 'not' p) '&' (p 'nor' q)) = (p 'nor' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:38

    (p 'or' (q 'nor' r)) = ((p 'or' ( 'not' q)) '&' (p 'or' ( 'not' r)))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:39

    (p 'nor' (q 'nor' r)) = ((( 'not' p) '&' q) 'or' (( 'not' p) '&' r))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:40

    (p 'nor' (q '&' r)) = (( 'not' (p 'or' q)) 'or' ( 'not' (p 'or' r)))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:41

    (p '&' (q 'nor' r)) = ((p '&' ( 'not' q)) '&' ( 'not' r))

    proof



      thus (p '&' (q 'nor' r)) = (p '&' (( 'not' q) '&' ( 'not' r)))

      .= ((p '&' ( 'not' q)) '&' ( 'not' r));

    end;

    theorem :: XBOOLEAN:42

    (p => (p 'nor' q)) = ( 'not' p)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:43

    (p => (q 'nor' r)) = ((p => ( 'not' q)) '&' (p => ( 'not' r)))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:44

    (p 'or' (p 'nor' q)) = (q => p)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:45

    (p 'or' (q 'nor' r)) = ((q => p) '&' (r => p))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:46

    (p => (q 'nor' r)) = ((( 'not' p) 'or' ( 'not' q)) '&' (( 'not' p) 'or' ( 'not' r)))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:47

    (p 'nor' (p <=> q)) = (( 'not' p) '&' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:48

    (( 'not' p) '&' (p <=> q)) = (p 'nor' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:49

    (p 'nor' (q <=> r)) = ( 'not' (((p 'or' ( 'not' q)) 'or' r) '&' ((p 'or' ( 'not' r)) 'or' q)))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:50

    (p <=> q) = ((p '&' q) 'or' (p 'nor' q))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:51

    (p 'nand' p) = ( 'not' p);

    theorem :: XBOOLEAN:52

    (p '&' (p 'nand' q)) = (p '&' ( 'not' q))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:53

    (p 'nand' (p '&' q)) = ( 'not' (p '&' q))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:54

    (p 'nand' (q 'nand' r)) = ((( 'not' p) 'or' q) '&' (( 'not' p) 'or' r))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:55

    (p 'nand' (q 'or' r)) = (( 'not' (p '&' q)) '&' ( 'not' (p '&' r)))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:56

    (p => (p 'nand' q)) = (p 'nand' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:57

    (p 'nand' (p 'nand' q)) = (p => q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:58

    (p 'nand' (q 'nand' r)) = ((p => q) '&' (p => r))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:59

    (p 'nand' (p => q)) = ( 'not' (p '&' q))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:60

    (p 'nand' (q => r)) = ((p => q) '&' (p => ( 'not' r)))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:61

    (( 'not' p) 'or' (p 'nand' q)) = (p 'nand' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:62

    (p 'nand' (q => r)) = ((( 'not' p) 'or' q) '&' (( 'not' p) 'or' ( 'not' r)))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:63

    (( 'not' p) '&' (p 'nand' q)) = (( 'not' p) 'or' (( 'not' p) '&' ( 'not' q)))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:64

    (p '&' (q 'nand' r)) = ((p '&' ( 'not' q)) 'or' (p '&' ( 'not' r)))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:65

    (p 'nand' (p <=> q)) = ( 'not' (p '&' q))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:66

    (p 'nand' (q <=> r)) = ( 'not' ((p '&' (( 'not' q) 'or' r)) '&' (( 'not' r) 'or' q)));

    theorem :: XBOOLEAN:67

    (p 'nand' (q 'nor' r)) = ((( 'not' p) 'or' q) 'or' r)

    proof



      thus (p 'nand' (q 'nor' r)) = (( 'not' p) 'or' (q 'or' r))

      .= ((( 'not' p) 'or' q) 'or' r);

    end;

    theorem :: XBOOLEAN:68

    ((p '\' q) '\' q) = (p '\' q)

    proof

      q = FALSE or q = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:69

    (p '&' (p '\' q)) = (p '\' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:70

    (p 'nor' (p <=> q)) = (q '\' p)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:71

    (p 'nor' (p 'nor' q)) = (q '\' p)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:72

    (p 'xor' (p 'xor' q)) = q

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:73

    ((p 'xor' q) 'xor' r) = (p 'xor' (q 'xor' r))

    proof

      q = FALSE or q = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:74

    ( 'not' (p 'xor' q)) = (( 'not' p) 'xor' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:75

    (p '&' (q 'xor' r)) = ((p '&' q) 'xor' (p '&' r))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:76

    (p '&' (p 'xor' q)) = (p '&' ( 'not' q))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:77

    (p 'xor' (p '&' q)) = (p '&' ( 'not' q))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:78

    (( 'not' p) '&' (p 'xor' q)) = (( 'not' p) '&' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:79

    (p 'or' (p 'xor' q)) = (p 'or' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:80

    (p 'or' (( 'not' p) 'xor' q)) = (p 'or' ( 'not' q))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:81

    (p 'xor' (( 'not' p) '&' q)) = (p 'or' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:82

    (p 'xor' (p 'or' q)) = (( 'not' p) '&' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:83

    (p 'xor' (q '&' r)) = ((p 'or' (q '&' r)) '&' (( 'not' p) 'or' ( 'not' (q '&' r))))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:84

    (( 'not' p) 'xor' (p => q)) = (p '&' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:85

    (p => (p 'xor' q)) = (( 'not' p) 'or' ( 'not' q))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:86

    (p 'xor' (p => q)) = (( 'not' p) 'or' ( 'not' q))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:87

    (( 'not' p) 'xor' (q => p)) = ((p '&' (p 'or' ( 'not' q))) 'or' (( 'not' p) '&' q))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:88

    (p 'xor' (p <=> q)) = ( 'not' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:89

    (( 'not' p) 'xor' (p <=> q)) = q

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:90

    (p 'nor' (p 'xor' q)) = (( 'not' p) '&' ( 'not' q))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:91

    (p 'nor' (p 'xor' q)) = (p 'nor' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:92

    (p 'xor' (p 'nor' q)) = (q => p)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:93

    (p 'nand' (p 'xor' q)) = (p => q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:94

    (p 'xor' (p 'nand' q)) = (p => q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:95

    (p 'xor' (p => q)) = (p 'nand' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:96

    (p 'nand' (q 'xor' r)) = ((p '&' q) <=> (p '&' r))

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:97

    (p 'xor' (p '&' q)) = (p '\' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:98

    (p '&' (p 'xor' q)) = (p '\' q)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:99

    (( 'not' p) '&' (p 'xor' q)) = (q '\' p)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:100

    (p 'xor' (p 'or' q)) = (q '\' p)

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    begin

    theorem :: XBOOLEAN:101

    (p '&' q) = TRUE implies p = TRUE & q = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:102

    ( 'not' (p '&' ( 'not' p))) = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:103

    (p => p) = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:104

    (p => (q => p)) = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:105

    (p => ((p => q) => q)) = TRUE

    proof



       A1: q = FALSE or q = TRUE by Def3;

      p = FALSE or p = TRUE by Def3;

      hence thesis by A1;

    end;

    theorem :: XBOOLEAN:106

    ((p => q) => ((q => r) => (p => r))) = TRUE

    proof



       A1: q = FALSE or q = TRUE by Def3;



       A2: p = FALSE or p = TRUE by Def3;

      r = FALSE or r = TRUE by Def3;

      hence thesis by A1, A2;

    end;

    theorem :: XBOOLEAN:107

    ((p => q) => ((r => p) => (r => q))) = TRUE

    proof



       A1: q = FALSE or q = TRUE by Def3;



       A2: p = FALSE or p = TRUE by Def3;

      r = FALSE or r = TRUE by Def3;

      hence thesis by A1, A2;

    end;

    theorem :: XBOOLEAN:108

    ((p => (p => q)) => (p => q)) = TRUE

    proof



       A1: q = FALSE or q = TRUE by Def3;

      p = FALSE or p = TRUE by Def3;

      hence thesis by A1;

    end;

    theorem :: XBOOLEAN:109

    ((p => (q => r)) => ((p => q) => (p => r))) = TRUE

    proof



       A1: q = FALSE or q = TRUE by Def3;



       A2: p = FALSE or p = TRUE by Def3;

      r = FALSE or r = TRUE by Def3;

      hence thesis by A1, A2;

    end;

    theorem :: XBOOLEAN:110

    ((p => (q => r)) => (q => (p => r))) = TRUE

    proof



       A1: q = FALSE or q = TRUE by Def3;



       A2: p = FALSE or p = TRUE by Def3;

      r = FALSE or r = TRUE by Def3;

      hence thesis by A1, A2;

    end;

    theorem :: XBOOLEAN:111

    (((p => q) => r) => (q => r)) = TRUE

    proof



       A1: q = FALSE or q = TRUE by Def3;

      r = FALSE or r = TRUE by Def3;

      hence thesis by A1;

    end;

    theorem :: XBOOLEAN:112

    (( TRUE => p) => p) = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:113

    (p => q) = TRUE implies ((q => r) => (p => r)) = TRUE

    proof

      r = FALSE or r = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:114

    (p => (p => q)) = TRUE implies (p => q) = TRUE

    proof

      q = FALSE or q = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:115

    (p => (q => r)) = TRUE implies ((p => q) => (p => r)) = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:116

    (p => q) = TRUE & (q => p) = TRUE implies p = q

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:117

    (p => q) = TRUE & (q => r) = TRUE implies (p => r) = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:118

    ((( 'not' p) => p) => p) = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:119

    ( 'not' p) = TRUE implies (p => q) = TRUE ;

    theorem :: XBOOLEAN:120

    (p => q) = TRUE & (p => ( 'not' q)) = TRUE implies ( 'not' p) = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:121

    ((p => q) => (( 'not' (q '&' r)) => ( 'not' (p '&' r)))) = TRUE

    proof



       A1: q = FALSE or q = TRUE by Def3;



       A2: p = FALSE or p = TRUE by Def3;

      r = FALSE or r = TRUE by Def3;

      hence thesis by A1, A2;

    end;

    theorem :: XBOOLEAN:122

    (p 'or' (p => q)) = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:123

    (p => (p 'or' q)) = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:124

    (( 'not' q) 'or' ((q => p) => p)) = TRUE

    proof



       A1: q = FALSE or q = TRUE by Def3;

      p = FALSE or p = TRUE by Def3;

      hence thesis by A1;

    end;

    theorem :: XBOOLEAN:125

    (p <=> p) = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:126

    ((((p <=> q) <=> r) <=> p) <=> (q <=> r)) = TRUE

    proof



       A1: q = FALSE or q = TRUE by Def3;



       A2: p = FALSE or p = TRUE by Def3;

      r = FALSE or r = TRUE by Def3;

      hence thesis by A1, A2;

    end;

    theorem :: XBOOLEAN:127

    (p <=> q) = TRUE & (q <=> r) = TRUE implies (p <=> r) = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:128

    (p <=> q) = TRUE & (r <=> s) = TRUE implies ((p <=> r) <=> (q <=> s)) = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:129

    ( 'not' (p <=> ( 'not' p))) = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:130

    (p <=> q) = TRUE & (r <=> s) = TRUE implies ((p '&' r) <=> (q '&' s)) = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:131

    (p <=> q) = TRUE & (r <=> s) = TRUE implies ((p 'or' r) <=> (q 'or' s)) = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:132

    (p <=> q) = TRUE iff (p => q) = TRUE & (q => p) = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:133

    (p <=> q) = TRUE & (r <=> s) = TRUE implies ((p => r) <=> (q => s)) = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:134

    ( 'not' (p 'nor' ( 'not' p))) = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:135

    (p 'nand' ( 'not' p)) = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:136

    (p 'or' (p 'nand' q)) = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:137

    (p 'nand' (p 'nor' q)) = TRUE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:138

    (p '&' ( 'not' p)) = FALSE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:139

    (p '&' p) = FALSE implies p = FALSE ;

    theorem :: XBOOLEAN:140

    (p '&' q) = FALSE implies p = FALSE or q = FALSE ;

    theorem :: XBOOLEAN:141

    ( 'not' (p => p)) = FALSE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:142

    (p <=> ( 'not' p)) = FALSE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:143

    ( 'not' (p <=> p)) = FALSE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:144

    (p '&' (p 'nor' q)) = FALSE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:145

    (p 'nor' (p => q)) = FALSE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:146

    (p 'nor' (p 'nand' q)) = FALSE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;

    theorem :: XBOOLEAN:147

    (p 'xor' p) = FALSE

    proof

      p = FALSE or p = TRUE by Def3;

      hence thesis;

    end;