# Library models

verified partial models proving the independence of all axioms but A3

Module A1.

CoInductive X := T | U | D.
Notation "1" := U.
Notation "2" := D.
Definition mult x y :=
match x,y with
| 1,1 => 1
| 2,2 => T
| 2,_
| _,2 => 2
| _,_ => T
end.
Infix "*" := mult.
Definition inter x y :=
match x,y with
| T,_ => y
| _,T => x
| 1,_ => y
| _,1 => x
| 2,2 => T
end.
Infix "^" := inter.
Definition conv (x: X) := x.
Notation "x `" := (conv x) (at level 20).

Lemma iA: ~forall a b c, a^(b^c) = (a^b)^c.
Proof. intro H; discriminate (H 1 2 2). Qed.
Lemma iC: forall a b, a^b = b^a.
Proof. now destruct a; destruct b. Qed.
Lemma ixT: forall a, a^T = a.
Proof. now destruct a. Qed.

Lemma mA: forall a b c, a*(b*c) = (a*b)*c.
Proof. now destruct a; destruct b; destruct c. Qed.
Lemma mx1: forall a, a*1 = a.
Proof. now destruct a. Qed.

Lemma cI: forall a, a``= a.
Proof. now destruct a. Qed.
Lemma ci: forall a b, (a ^ b)`= a` ^ b`.
Proof. now destruct a; destruct b. Qed.
Lemma cm: forall a b, (a * b)`= b` * a`.
Proof. now destruct a; destruct b. Qed.

Lemma uu: 1 ^ 1 = 1.
Proof. reflexivity. Qed.
Lemma mT: forall a, a*T = (1^(a*T))*T.
Proof. now destruct a. Qed.
Lemma mi1: forall a b, (1^a)*b = ((1^a)*T)^b.
Proof. now destruct a; destruct b. Qed.
Lemma i1m: forall a b, 1^(a*b) = 1 ^ ((a ^ b`)*T).
Proof. now destruct a; destruct b. Qed.

End A1.

Module A2.

CoInductive X := T | U | D.
Notation "1" := U.
Notation "2" := D.
Definition mult x y :=
match x,y with
| 1,1 => 1
| 1,2
| 2,1 => 2
| _,_ => T
end.
Infix "*" := mult.
Definition inter x y :=
match x,y with
| T,_ => y
| _,_ => x
end.
Infix "^" := inter.
Definition conv (x: X) := x.
Notation "x `" := (conv x) (at level 20).

Lemma iA: forall a b c, a^(b^c) = (a^b)^c.
Proof. now destruct a; destruct b; destruct c. Qed.
Lemma iC: ~forall a b, a^b = b^a.
Proof. intro H. discriminate (H 1 2). Qed.
Lemma ixT: forall a, a^T = a.
Proof. now destruct a. Qed.

Lemma mA: forall a b c, a*(b*c) = (a*b)*c.
Proof. now destruct a; destruct b; destruct c. Qed.
Lemma mx1: forall a, a*1 = a.
Proof. now destruct a. Qed.

Lemma cI: forall a, a``= a.
Proof. now destruct a. Qed.
Lemma ci: forall a b, (a ^ b)`= a` ^ b`.
Proof. now destruct a; destruct b. Qed.
Lemma cm: forall a b, (a * b)`= b` * a`.
Proof. now destruct a; destruct b. Qed.

Lemma uu: 1 ^ 1 = 1.
Proof. reflexivity. Qed.
Lemma mT: forall a, a*T = (1^(a*T))*T.
Proof. now destruct a. Qed.
Lemma mi1: forall a b, (1^a)*b = ((1^a)*T)^b.
Proof. now destruct a; destruct b. Qed.
Lemma i1m: forall a b, 1^(a*b) = 1 ^ ((a ^ b`)*T).
Proof. now destruct a; destruct b. Qed.

End A2.

A3 is a consequence of A9 and A12 (plus symmetries)

Module A4.

CoInductive X := T | U | D.
Notation "1" := U.
Notation "2" := D.
Definition mult x y :=
match x,y with
| 1,1
| 2,2 => 1
| 2,_
| _,2 => 2
| _,_ => T
end.
Infix "*" := mult.
Definition inter x y :=
match x,y with
| T,_ => y
| _,T => x
| 1,_ => y
| _,1 => x
| 2,2 => 1
end.
Infix "^" := inter.
Definition conv (x: X) := x.
Notation "x `" := (conv x) (at level 20).

Lemma iA: forall a b c, a^(b^c) = (a^b)^c.
Proof. now destruct a; destruct b; destruct c. Qed.
Lemma iC: forall a b, a^b = b^a.
Proof. now destruct a; destruct b. Qed.
Lemma ixT: forall a, a^T = a.
Proof. now destruct a. Qed.

Lemma mA: ~forall a b c, a*(b*c) = (a*b)*c.
Proof. intro H; discriminate (H T 2 2). Qed.
Lemma mx1: forall a, a*1 = a.
Proof. now destruct a. Qed.

Lemma cI: forall a, a``= a.
Proof. now destruct a. Qed.
Lemma ci: forall a b, (a ^ b)`= a` ^ b`.
Proof. now destruct a; destruct b. Qed.
Lemma cm: forall a b, (a * b)`= b` * a`.
Proof. now destruct a; destruct b. Qed.

Lemma uu: 1 ^ 1 = 1.
Proof. reflexivity. Qed.
Lemma mT: forall a, a*T = (1^(a*T))*T.
Proof. now destruct a. Qed.
Lemma mi1: forall a b, (1^a)*b = ((1^a)*T)^b.
Proof. now destruct a; destruct b. Qed.
Lemma i1m: forall a b, 1^(a*b) = 1 ^ ((a ^ b`)*T).
Proof. now destruct a; destruct b. Qed.

End A4.

Module A5.

CoInductive X := T | U.
Notation "1" := U.
Definition mult (x y: X) :=
match x,y with
| _,_ => 1
end.
Infix "*" := mult.
Definition inter x y :=
match x,y with
| T,T => T
| _,_ => 1
end.
Infix "^" := inter.
Definition conv (x: X) := x.
Notation "x `" := (conv x) (at level 20).

Lemma iA: forall a b c, a^(b^c) = (a^b)^c.
Proof. now destruct a; destruct b; destruct c. Qed.
Lemma iC: forall a b, a^b = b^a.
Proof. now destruct a; destruct b. Qed.
Lemma ixT: forall a, T^a = a.
Proof. now destruct a. Qed.

Lemma mA: forall a b c, a*(b*c) = (a*b)*c.
Proof. now destruct a; destruct b; destruct c. Qed.
Lemma mx1: ~forall a, a*1 = a.
Proof. intro H. discriminate (H T). Qed.

Lemma cI: forall a, a``= a.
Proof. now destruct a. Qed.
Lemma ci: forall a b, (a ^ b)`= a` ^ b`.
Proof. now destruct a; destruct b. Qed.
Lemma cm: forall a b, (a * b)`= b` * a`.
Proof. now destruct a; destruct b. Qed.

Lemma uu: 1 ^ 1 = 1.
Proof. reflexivity. Qed.
Lemma mT: forall a, a*T = (1^(a*T))*T.
Proof. now destruct a. Qed.
Lemma mi1: forall a b, (1^a)*b = ((1^a)*T)^b.
Proof. now destruct a; destruct b. Qed.
Lemma i1m: forall a b, 1^(a*b) = 1 ^ ((a ^ b`)*T).
Proof. now destruct a; destruct b. Qed.

End A5.

Module A6.

CoInductive X := T | U.
Notation "1" := U.
Definition mult x y :=
match x,y with
| 1,1 => 1
| _,_ => T
end.
Infix "*" := mult.
Definition inter x y :=
match x,y with
| T,T => T
| _,_ => 1
end.
Infix "^" := inter.
Definition conv (x: X) := T.
Notation "x `" := (conv x) (at level 20).

Lemma iA: forall a b c, a^(b^c) = (a^b)^c.
Proof. now destruct a; destruct b; destruct c. Qed.
Lemma iC: forall a b, a^b = b^a.
Proof. now destruct a; destruct b. Qed.
Lemma ixT: forall a, T^a = a.
Proof. now destruct a. Qed.

Lemma mA: forall a b c, a*(b*c) = (a*b)*c.
Proof. now destruct a; destruct b; destruct c. Qed.
Lemma mx1: forall a, a*1 = a.
Proof. now destruct a. Qed.

Lemma cI: ~forall a, a``= a.
Proof. intro H. discriminate (H 1). Qed.
Lemma ci: forall a b, (a ^ b)`= a` ^ b`.
Proof. now destruct a; destruct b. Qed.
Lemma cm: forall a b, (a * b)`= b` * a`.
Proof. now destruct a; destruct b. Qed.
Lemma uu: 1 ^ 1 = 1.
Proof. reflexivity. Qed.
Lemma mT: forall a, a*T = (1^(a*T))*T.
Proof. now destruct a. Qed.
Lemma mi1: forall a b, (1^a)*b = ((1^a)*T)^b.
Proof. now destruct a; destruct b. Qed.
Lemma i1m: forall a b, 1^(a*b) = 1 ^ ((a ^ b`)*T).
Proof. now destruct a; destruct b. Qed.

End A6.

Module A7.

CoInductive X := T | U | D | E.
Notation "1" := U.
Notation "2" := D.
Notation "3" := E.
Definition mult x y :=
match x,y with
| _,1 => x
| 1,_ => y
| _,_ => T
end.
Infix "*" := mult.
Definition inter x y :=
match x,y with
| T,_ => y
| _,T => x
| 2,3
| 3,2 => 2
| 3,3 => T
| _,_ => 1
end.
Infix "^" := inter.
Definition conv x :=
match x with
| 3 => 2
| 2 => 3
| x => x
end.
Notation "x `" := (conv x) (at level 20).

Lemma iA: forall a b c, a^(b^c) = (a^b)^c.
Proof. now destruct a; destruct b; destruct c. Qed.
Lemma iC: forall a b, a^b = b^a.
Proof. now destruct a; destruct b. Qed.
Lemma ixT: forall a, a^T = a.
Proof. now destruct a. Qed.

Lemma mA: forall a b c, a*(b*c) = (a*b)*c.
Proof. now destruct a; destruct b; destruct c. Qed.
Lemma mx1: forall a, a*1 = a.
Proof. now destruct a. Qed.

Lemma cI: forall a, a``= a.
Proof. now destruct a. Qed.
Lemma ci: ~forall a b, (a ^ b)`= a` ^ b`.
Proof. intro H. discriminate (H 2 2). Qed.
Lemma cm: forall a b, (a * b)`= b` * a`.
Proof. now destruct a; destruct b. Qed.

Lemma uu: 1 ^ 1 = 1.
Proof. reflexivity. Qed.
Lemma mT: forall a, a*T = (1^(a*T))*T.
Proof. now destruct a. Qed.
Lemma mi1: forall a b, (1^a)*b = ((1^a)*T)^b.
Proof. now destruct a; destruct b. Qed.
Lemma i1m: forall a b, 1^(a*b) = 1 ^ ((a ^ b`)*T).
Proof. now destruct a; destruct b. Qed.

End A7.

Module A8.

CoInductive X := T | U | D.
Notation "1" := U.
Notation "2" := D.
Definition mult x y :=
match x,y with
| _,T => T
| _,1 => x
| _,_ => 2
end.
Infix "*" := mult.
Definition inter x y :=
match x,y with
| 1,_
| _,1 => 1
| T,T
| 2,2 => T
|_,_ => 2
end.
Infix "^" := inter.
Definition conv (x: X) := x.
Notation "x `" := (conv x) (at level 20).

Lemma iA: forall a b c, a^(b^c) = (a^b)^c.
Proof. now destruct a; destruct b; destruct c. Qed.
Lemma iC: forall a b, a^b = b^a.
Proof. now destruct a; destruct b. Qed.
Lemma ixT: forall a, a^T = a.
Proof. now destruct a. Qed.

Lemma mA: forall a b c, a*(b*c) = (a*b)*c.
Proof. now destruct a; destruct b; destruct c. Qed.
Lemma mx1: forall a, a*1 = a.
Proof. now destruct a. Qed.

Lemma cI: forall a, a``= a.
Proof. now destruct a. Qed.
Lemma ci: forall a b, (a ^ b)`= a` ^ b`.
Proof. now destruct a; destruct b. Qed.
Lemma cm: ~forall a b, (a * b)`= b` * a`.
Proof. intro H. discriminate (H T 2). Qed.

Lemma uu: 1 ^ 1 = 1.
Proof. reflexivity. Qed.
Lemma mT: forall a, a*T = (1^(a*T))*T.
Proof. now destruct a. Qed.
Lemma mi1: forall a b, (1^a)*b = ((1^a)*T)^b.
Proof. now destruct a; destruct b. Qed.
Lemma i1m: forall a b, 1^(a*b) = 1 ^ ((a ^ b`)*T).
Proof. now destruct a; destruct b. Qed.

End A8.

Module A9.

CoInductive X := T | U.
Notation "1" := U.
Definition mult x y :=
match x,y with
| 1,_ => y
| _,1 => x
| T,T => 1
end.
Infix "*" := mult.
Definition inter x y :=
match x,y with
| T,_ => y
| _,T => x
| 1,1 => T
end.
Infix "^" := inter.
Definition conv (x: X) := x.
Notation "x `" := (conv x) (at level 20).

Lemma iA: forall a b c, a^(b^c) = (a^b)^c.
Proof. now destruct a; destruct b; destruct c. Qed.
Lemma iC: forall a b, a^b = b^a.
Proof. now destruct a; destruct b. Qed.
Lemma ixT: forall a, a^T = a.
Proof. now destruct a. Qed.

Lemma mA: forall a b c, a*(b*c) = (a*b)*c.
Proof. now destruct a; destruct b; destruct c. Qed.
Lemma mx1: forall a, a*1 = a.
Proof. now destruct a. Qed.

Lemma cI: forall a, a``= a.
Proof. now destruct a. Qed.
Lemma ci: forall a b, (a ^ b)`= a` ^ b`.
Proof. now destruct a; destruct b. Qed.
Lemma cm: forall a b, (a * b)`= b` * a`.
Proof. now destruct a; destruct b. Qed.

Lemma uu: 1 ^ 1 <> 1.
Proof. discriminate. Qed.
Lemma mT: forall a, a*T = (1^(a*T))*T.
Proof. now destruct a. Qed.
Lemma mi1: forall a b, (1^a)*b = ((1^a)*T)^b.
Proof. now destruct a; destruct b. Qed.
Lemma i1m: forall a b, 1^(a*b) = 1 ^ ((a ^ b`)*T).
Proof. now destruct a; destruct b. Qed.

End A9.

Module A10.

CoInductive X := T | U | D | E.
Notation "1" := U.
Notation "2" := D.
Notation "3" := E.
Definition mult x y :=
match x,y with
| 1,_ => y
| _,1 => x
| 3,3 => T
| _,_ => 2
end.
Infix "*" := mult.
Definition inter x y :=
match x,y with
| T,_ => y
| _,T => x
| 2,_ => 2
| _,2 => 2
| 3,3 => T
| _,_ => 1
end.
Infix "^" := inter.
Definition conv (x: X) := x.
Notation "x `" := (conv x) (at level 20).

Lemma iA: forall a b c, a^(b^c) = (a^b)^c.
Proof. now destruct a; destruct b; destruct c. Qed.
Lemma iC: forall a b, a^b = b^a.
Proof. now destruct a; destruct b. Qed.
Lemma ixT: forall a, a^T = a.
Proof. now destruct a. Qed.

Lemma mA: forall a b c, a*(b*c) = (a*b)*c.
Proof. now destruct a; destruct b; destruct c. Qed.
Lemma mx1: forall a, a*1 = a.
Proof. now destruct a. Qed.

Lemma cI: forall a, a``= a.
Proof. now destruct a. Qed.
Lemma ci: forall a b, (a ^ b)`= a` ^ b`.
Proof. now destruct a; destruct b. Qed.
Lemma cm: forall a b, (a * b)`= b` * a`.
Proof. now destruct a; destruct b. Qed.

Lemma uu: 1 ^ 1 = 1.
Proof. reflexivity. Qed.
Lemma mT: forall a, a*T = (1^(a*T))*T.
Proof. now destruct a. Qed.
Lemma mi1: forall a b, (1^a)*b = ((1^a)*T)^b.
Proof. now destruct a; destruct b. Qed.
Lemma i1m: ~forall a b, 1^(a*b) = 1 ^ ((a ^ b`)*T).
Proof. intro H. discriminate (H 3 3). Qed.

End A10.

Module A11.

CoInductive X := T | U.
Notation "1" := U.
Definition mult x y :=
match x,y with
| 1,_ => y
| _,1 => x
| T,T => 1
end.
Infix "*" := mult.
Definition inter x y :=
match x,y with
| T,_ => y
| _,T => x
| 1,1 => 1
end.
Infix "^" := inter.
Definition conv (x: X) := x.
Notation "x `" := (conv x) (at level 20).

Lemma iA: forall a b c, a^(b^c) = (a^b)^c.
Proof. now destruct a; destruct b; destruct c. Qed.
Lemma iC: forall a b, a^b = b^a.
Proof. now destruct a; destruct b. Qed.
Lemma ixT: forall a, a^T = a.
Proof. now destruct a. Qed.

Lemma mA: forall a b c, a*(b*c) = (a*b)*c.
Proof. now destruct a; destruct b; destruct c. Qed.
Lemma mx1: forall a, a*1 = a.
Proof. now destruct a. Qed.

Lemma cI: forall a, a``= a.
Proof. now destruct a. Qed.
Lemma ci: forall a b, (a ^ b)`= a` ^ b`.
Proof. now destruct a; destruct b. Qed.
Lemma cm: forall a b, (a * b)`= b` * a`.
Proof. now destruct a; destruct b. Qed.

Lemma uu: 1 ^ 1 = 1.
Proof. reflexivity. Qed.
Lemma mT: ~forall a, a*T = (1^(a*T))*T.
Proof. intro H. discriminate (H T). Qed.
Lemma mi1: forall a b, (1^a)*b = ((1^a)*T)^b.
Proof. now destruct a; destruct b. Qed.
Lemma i1m: forall a b, 1^(a*b) = 1 ^ ((a ^ b`)*T).
Proof. now destruct a; destruct b. Qed.

End A11.

Module A12.

CoInductive X := T | U | D.
Notation "1" := U.
Notation "2" := D.
Definition mult x y :=
match x,y with
| 1,_ => y
| _,1 => x
| T,T => T
| 2,2 => T
| _,_ => 2
end.
Infix "*" := mult.
Definition inter x y :=
match x,y with
| T,_ => y
| _,T => x
| 1,1 => 1
| 2,2 => 1
| _,_ => 2
end.
Infix "^" := inter.
Definition conv (x: X) := x.
Notation "x `" := (conv x) (at level 20).

Lemma iA: forall a b c, a^(b^c) = (a^b)^c.
Proof. now destruct a; destruct b; destruct c. Qed.
Lemma iC: forall a b, a^b = b^a.
Proof. now destruct a; destruct b. Qed.
Lemma ixT: forall a, a^T = a.
Proof. now destruct a. Qed.

Lemma mA: forall a b c, a*(b*c) = (a*b)*c.
Proof. now destruct a; destruct b; destruct c. Qed.
Lemma mx1: forall a, a*1 = a.
Proof. now destruct a. Qed.

Lemma cI: forall a, a``= a.
Proof. now destruct a. Qed.
Lemma ci: forall a b, (a ^ b)`= a` ^ b`.
Proof. now destruct a; destruct b. Qed.
Lemma cm: forall a b, (a * b)`= b` * a`.
Proof. now destruct a; destruct b. Qed.

Lemma uu: 1 ^ 1 = 1.
Proof. reflexivity. Qed.
Lemma mT: forall a, a*T = (1^(a*T))*T.
Proof. now destruct a. Qed.
Lemma mi1: ~forall a b, (1^a)*b = ((1^a)*T)^b.
Proof. intro H. discriminate (H 2 2). Qed.
Lemma i1m: forall a b, 1^(a*b) = 1 ^ ((a ^ b`)*T).
Proof. now destruct a; destruct b. Qed.

End A12.