Home	Quantum Logic Explorer Theorem List (p. 13 of 13)	< Previous  Wrap >
		Browser slow? Try the Unicode version.
Mirrors  >  Metamath Home Page  >  QLE Home Page  >  Theorem List Contents       This page: Page List

---

Theorem List for Quantum Logic Explorer - 1201-1215   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xxdp53 1201	Part of proof (5)=>(3) in Day/Pickering 1982.
p2 a2 b2      c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a2 a0 a1 b1       b0 a0 p0       a0 b0 a1 b1 a2 b2      p0 a1 b1 a2 b2      p2 a0 b0 a1 b1       a0 b0 b1 c2 c0 c1
Theorem	xdp45lem 1202	Part of proof (4)=>(5) in Day/Pickering 1982.
p2 a2 b2      c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a2 a0 a1 b1       b0 a0 p0       a0 b0 a1 b1 a2 b2      p0 a1 b1 a2 b2      p2 a0 b0 a1 b1      a0 a1 b0 a0 p0 b1 c0 c1 b1 a0 a1
Theorem	xdp43lem 1203	Part of proof (4)=>(3) in Day/Pickering 1982.
p2 a2 b2      c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a2 a0 a1 b1       b0 a0 p0       a0 b0 a1 b1 a2 b2      p0 a1 b1 a2 b2      p2 a0 b0 a1 b1       a0 b0 b1 c2 c0 c1
Theorem	xdp45 1204	Part of proof (4)=>(5) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a2 a0 a1 b1       b0 a0 p0       a0 b0 a1 b1 a2 b2      p0 a1 b1 a2 b2      p2 a0 b0 a1 b1      a0 a1 b0 a0 p0 b1 c0 c1 b1 a0 a1
Theorem	xdp43 1205	Part of proof (4)=>(3) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a2 a0 a1 b1       b0 a0 p0       a0 b0 a1 b1 a2 b2      p0 a1 b1 a2 b2      p2 a0 b0 a1 b1       a0 b0 b1 c2 c0 c1
Theorem	3dp43 1206	"3OA" version of xdp43 1205. Changed a2 to a1 and b2 to b1.
c0 a1 a1 b1 b1      c1 a0 a1 b0 b1      c2 a0 a1 b0 b1       a1 a0 a1 b1       b0 a0 p0       a0 b0 a1 b1 a1 b1      p0 a1 b1 a1 b1      p2 a0 b0 a1 b1       a0 b0 b1 c2 c0 c1
Theorem	oadp35lemg 1207	Part of proof (3)=>(5) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1      p0 a1 b1 a2 b2       a0 b0 a1 b1 a2 b2       a0 b0 b1 c2 c0 c1
Theorem	oadp35lemf 1208	Part of proof (3)=>(5) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1      p0 a1 b1 a2 b2       a0 b0 a1 b1 a2 b2      a0 a0 b0 b1 c2 c0 c1
Theorem	oadp35lemc 1209	Part of proof (3)=>(5) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1      p0 a1 b1 a2 b2       a0 b0 a1 b1 a2 b2      b0 a0 b0 b1 c2 c0 c1 b0 b1 c2 c0 c1
Theorem	oadp35 1210	Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (3)=>(5)
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      p0 a1 b1 a2 b2      a0 a1 b0 a0 p0 b1 c0 c1 b1 a0 a1
Theorem	testmod 1211	A modular law experiment.
Theorem	testmod1 1212	A modular law experiment.
Theorem	testmod2 1213	A modular law experiment.
Theorem	testmod2expanded 1214	A modular law experiment.
Theorem	testmod3 1215	A modular law experiment.

< Previous  Wrap >

---

Page List Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1215

---

Copyright terms: Public domain

< Previous  Wrap >