CoCalc -- CARD.pht

open-axiom repository from github
open-axiom / src / hyper / pages / CARD.pht
²⁴⁷⁰⁸ views
\begin{patch}{CardinalNumberXmpPagePatch1}
\begin{paste}{CardinalNumberXmpPageFull1}{CardinalNumberXmpPageEmpty1}
\pastebutton{CardinalNumberXmpPageFull1}{\hidepaste}
\tab{5}\spadcommand{c0 := 0 :: CardinalNumber\bound{c0 }}
\indentrel{3}\begin{verbatim}
   (1)  0
                                   Type: CardinalNumber
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPageEmpty1}
\begin{paste}{CardinalNumberXmpPageEmpty1}{CardinalNumberXmpPagePatch1}
\pastebutton{CardinalNumberXmpPageEmpty1}{\showpaste}
\tab{5}\spadcommand{c0 := 0 :: CardinalNumber\bound{c0 }}
\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPagePatch2}
\begin{paste}{CardinalNumberXmpPageFull2}{CardinalNumberXmpPageEmpty2}
\pastebutton{CardinalNumberXmpPageFull2}{\hidepaste}
\tab{5}\spadcommand{c1 := 1 :: CardinalNumber\bound{c1 }}
\indentrel{3}\begin{verbatim}
   (2)  1
                                   Type: CardinalNumber
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPageEmpty2}
\begin{paste}{CardinalNumberXmpPageEmpty2}{CardinalNumberXmpPagePatch2}
\pastebutton{CardinalNumberXmpPageEmpty2}{\showpaste}
\tab{5}\spadcommand{c1 := 1 :: CardinalNumber\bound{c1 }}
\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPagePatch3}
\begin{paste}{CardinalNumberXmpPageFull3}{CardinalNumberXmpPageEmpty3}
\pastebutton{CardinalNumberXmpPageFull3}{\hidepaste}
\tab{5}\spadcommand{c2 := 2 :: CardinalNumber\bound{c2 }}
\indentrel{3}\begin{verbatim}
   (3)  2
                                   Type: CardinalNumber
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPageEmpty3}
\begin{paste}{CardinalNumberXmpPageEmpty3}{CardinalNumberXmpPagePatch3}
\pastebutton{CardinalNumberXmpPageEmpty3}{\showpaste}
\tab{5}\spadcommand{c2 := 2 :: CardinalNumber\bound{c2 }}
\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPagePatch4}
\begin{paste}{CardinalNumberXmpPageFull4}{CardinalNumberXmpPageEmpty4}
\pastebutton{CardinalNumberXmpPageFull4}{\hidepaste}
\tab{5}\spadcommand{c3 := 3 :: CardinalNumber\bound{c3 }}
\indentrel{3}\begin{verbatim}
   (4)  3
                                   Type: CardinalNumber
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPageEmpty4}
\begin{paste}{CardinalNumberXmpPageEmpty4}{CardinalNumberXmpPagePatch4}
\pastebutton{CardinalNumberXmpPageEmpty4}{\showpaste}
\tab{5}\spadcommand{c3 := 3 :: CardinalNumber\bound{c3 }}
\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPagePatch5}
\begin{paste}{CardinalNumberXmpPageFull5}{CardinalNumberXmpPageEmpty5}
\pastebutton{CardinalNumberXmpPageFull5}{\hidepaste}
\tab{5}\spadcommand{A0 := Aleph 0\bound{A0 }}
\indentrel{3}\begin{verbatim}
   (5)  Aleph(0)
                                   Type: CardinalNumber
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPageEmpty5}
\begin{paste}{CardinalNumberXmpPageEmpty5}{CardinalNumberXmpPagePatch5}
\pastebutton{CardinalNumberXmpPageEmpty5}{\showpaste}
\tab{5}\spadcommand{A0 := Aleph 0\bound{A0 }}
\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPagePatch6}
\begin{paste}{CardinalNumberXmpPageFull6}{CardinalNumberXmpPageEmpty6}
\pastebutton{CardinalNumberXmpPageFull6}{\hidepaste}
\tab{5}\spadcommand{A1 := Aleph 1\bound{A1 }}
\indentrel{3}\begin{verbatim}
   (6)  Aleph(1)
                                   Type: CardinalNumber
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPageEmpty6}
\begin{paste}{CardinalNumberXmpPageEmpty6}{CardinalNumberXmpPagePatch6}
\pastebutton{CardinalNumberXmpPageEmpty6}{\showpaste}
\tab{5}\spadcommand{A1 := Aleph 1\bound{A1 }}
\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPagePatch7}
\begin{paste}{CardinalNumberXmpPageFull7}{CardinalNumberXmpPageEmpty7}
\pastebutton{CardinalNumberXmpPageFull7}{\hidepaste}
\tab{5}\spadcommand{finite? c2\free{c2 }}
\indentrel{3}\begin{verbatim}
   (7)  true
                                          Type: Boolean
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPageEmpty7}
\begin{paste}{CardinalNumberXmpPageEmpty7}{CardinalNumberXmpPagePatch7}
\pastebutton{CardinalNumberXmpPageEmpty7}{\showpaste}
\tab{5}\spadcommand{finite? c2\free{c2 }}
\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPagePatch8}
\begin{paste}{CardinalNumberXmpPageFull8}{CardinalNumberXmpPageEmpty8}
\pastebutton{CardinalNumberXmpPageFull8}{\hidepaste}
\tab{5}\spadcommand{finite? A0\free{A0 }}
\indentrel{3}\begin{verbatim}
   (8)  false
                                          Type: Boolean
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPageEmpty8}
\begin{paste}{CardinalNumberXmpPageEmpty8}{CardinalNumberXmpPagePatch8}
\pastebutton{CardinalNumberXmpPageEmpty8}{\showpaste}
\tab{5}\spadcommand{finite? A0\free{A0 }}
\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPagePatch9}
\begin{paste}{CardinalNumberXmpPageFull9}{CardinalNumberXmpPageEmpty9}
\pastebutton{CardinalNumberXmpPageFull9}{\hidepaste}
\tab{5}\spadcommand{countable? c2\free{c2 }}
\indentrel{3}\begin{verbatim}
   (9)  true
                                          Type: Boolean
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPageEmpty9}
\begin{paste}{CardinalNumberXmpPageEmpty9}{CardinalNumberXmpPagePatch9}
\pastebutton{CardinalNumberXmpPageEmpty9}{\showpaste}
\tab{5}\spadcommand{countable? c2\free{c2 }}
\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPagePatch10}
\begin{paste}{CardinalNumberXmpPageFull10}{CardinalNumberXmpPageEmpty10}
\pastebutton{CardinalNumberXmpPageFull10}{\hidepaste}
\tab{5}\spadcommand{countable? A0\free{A0 }}
\indentrel{3}\begin{verbatim}
   (10)  true
                                          Type: Boolean
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPageEmpty10}
\begin{paste}{CardinalNumberXmpPageEmpty10}{CardinalNumberXmpPagePatch10}
\pastebutton{CardinalNumberXmpPageEmpty10}{\showpaste}
\tab{5}\spadcommand{countable? A0\free{A0 }}
\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPagePatch11}
\begin{paste}{CardinalNumberXmpPageFull11}{CardinalNumberXmpPageEmpty11}
\pastebutton{CardinalNumberXmpPageFull11}{\hidepaste}
\tab{5}\spadcommand{countable? A1\free{A1 }}
\indentrel{3}\begin{verbatim}
   (11)  false
                                          Type: Boolean
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPageEmpty11}
\begin{paste}{CardinalNumberXmpPageEmpty11}{CardinalNumberXmpPagePatch11}
\pastebutton{CardinalNumberXmpPageEmpty11}{\showpaste}
\tab{5}\spadcommand{countable? A1\free{A1 }}
\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPagePatch12}
\begin{paste}{CardinalNumberXmpPageFull12}{CardinalNumberXmpPageEmpty12}
\pastebutton{CardinalNumberXmpPageFull12}{\hidepaste}
\tab{5}\spadcommand{[c2 + c2, c2 + A1]\free{c2 A1 }}
\indentrel{3}\begin{verbatim}
   (12)  [4,Aleph(1)]
                              Type: List CardinalNumber
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPageEmpty12}
\begin{paste}{CardinalNumberXmpPageEmpty12}{CardinalNumberXmpPagePatch12}
\pastebutton{CardinalNumberXmpPageEmpty12}{\showpaste}
\tab{5}\spadcommand{[c2 + c2, c2 + A1]\free{c2 A1 }}
\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPagePatch13}
\begin{paste}{CardinalNumberXmpPageFull13}{CardinalNumberXmpPageEmpty13}
\pastebutton{CardinalNumberXmpPageFull13}{\hidepaste}
\tab{5}\spadcommand{[c0*c2, c1*c2, c2*c2, c0*A1, c1*A1, c2*A1, A0*A1]\free{c0 c1 c2 A0 A1 }}
\indentrel{3}\begin{verbatim}
   (13)  [0,2,4,0,Aleph(1),Aleph(1),Aleph(1)]
                              Type: List CardinalNumber
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPageEmpty13}
\begin{paste}{CardinalNumberXmpPageEmpty13}{CardinalNumberXmpPagePatch13}
\pastebutton{CardinalNumberXmpPageEmpty13}{\showpaste}
\tab{5}\spadcommand{[c0*c2, c1*c2, c2*c2, c0*A1, c1*A1, c2*A1, A0*A1]\free{c0 c1 c2 A0 A1 }}
\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPagePatch14}
\begin{paste}{CardinalNumberXmpPageFull14}{CardinalNumberXmpPageEmpty14}
\pastebutton{CardinalNumberXmpPageFull14}{\hidepaste}
\tab{5}\spadcommand{[c2**c0, c2**c1, c2**c2, A1**c0, A1**c1, A1**c2]\free{c0 c1 c2 A1 }}
\indentrel{3}\begin{verbatim}
   (14)  [1,2,4,1,Aleph(1),Aleph(1)]
                              Type: List CardinalNumber
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPageEmpty14}
\begin{paste}{CardinalNumberXmpPageEmpty14}{CardinalNumberXmpPagePatch14}
\pastebutton{CardinalNumberXmpPageEmpty14}{\showpaste}
\tab{5}\spadcommand{[c2**c0, c2**c1, c2**c2, A1**c0, A1**c1, A1**c2]\free{c0 c1 c2 A1 }}
\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPagePatch15}
\begin{paste}{CardinalNumberXmpPageFull15}{CardinalNumberXmpPageEmpty15}
\pastebutton{CardinalNumberXmpPageFull15}{\hidepaste}
\tab{5}\spadcommand{[c2-c1, c2-c2, c2-c3, A1-c2, A1-A0, A1-A1]\free{c1 c2 c3 A0 A1 }}
\indentrel{3}\begin{verbatim}
   (15)  [1,0,"failed",Aleph(1),Aleph(1),"failed"]
              Type: List Union(CardinalNumber,"failed")
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPageEmpty15}
\begin{paste}{CardinalNumberXmpPageEmpty15}{CardinalNumberXmpPagePatch15}
\pastebutton{CardinalNumberXmpPageEmpty15}{\showpaste}
\tab{5}\spadcommand{[c2-c1, c2-c2, c2-c3, A1-c2, A1-A0, A1-A1]\free{c1 c2 c3 A0 A1 }}
\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPagePatch16}
\begin{paste}{CardinalNumberXmpPageFull16}{CardinalNumberXmpPageEmpty16}
\pastebutton{CardinalNumberXmpPageFull16}{\hidepaste}
\tab{5}\spadcommand{generalizedContinuumHypothesisAssumed true\bound{GCH }}
\indentrel{3}\begin{verbatim}
   (16)  true
                                          Type: Boolean
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPageEmpty16}
\begin{paste}{CardinalNumberXmpPageEmpty16}{CardinalNumberXmpPagePatch16}
\pastebutton{CardinalNumberXmpPageEmpty16}{\showpaste}
\tab{5}\spadcommand{generalizedContinuumHypothesisAssumed true\bound{GCH }}
\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPagePatch17}
\begin{paste}{CardinalNumberXmpPageFull17}{CardinalNumberXmpPageEmpty17}
\pastebutton{CardinalNumberXmpPageFull17}{\hidepaste}
\tab{5}\spadcommand{[c0**A0, c1**A0, c2**A0, A0**A0, A0**A1, A1**A0, A1**A1]\free{c0 c1 c2 A0 A1 GCH }}
\indentrel{3}\begin{verbatim}
   (17)
   [0,1,Aleph(1),Aleph(1),Aleph(2),Aleph(1),Aleph(2)]
                              Type: List CardinalNumber
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPageEmpty17}
\begin{paste}{CardinalNumberXmpPageEmpty17}{CardinalNumberXmpPagePatch17}
\pastebutton{CardinalNumberXmpPageEmpty17}{\showpaste}
\tab{5}\spadcommand{[c0**A0, c1**A0, c2**A0, A0**A0, A0**A1, A1**A0, A1**A1]\free{c0 c1 c2 A0 A1 GCH }}
\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPagePatch18}
\begin{paste}{CardinalNumberXmpPageFull18}{CardinalNumberXmpPageEmpty18}
\pastebutton{CardinalNumberXmpPageFull18}{\hidepaste}
\tab{5}\spadcommand{a := Aleph 0\free{GCH }\bound{a }}
\indentrel{3}\begin{verbatim}
   (18)  Aleph(0)
                                   Type: CardinalNumber
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPageEmpty18}
\begin{paste}{CardinalNumberXmpPageEmpty18}{CardinalNumberXmpPagePatch18}
\pastebutton{CardinalNumberXmpPageEmpty18}{\showpaste}
\tab{5}\spadcommand{a := Aleph 0\free{GCH }\bound{a }}
\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPagePatch19}
\begin{paste}{CardinalNumberXmpPageFull19}{CardinalNumberXmpPageEmpty19}
\pastebutton{CardinalNumberXmpPageFull19}{\hidepaste}
\tab{5}\spadcommand{c := 2**a\free{a }\bound{c }}
\indentrel{3}\begin{verbatim}
   (19)  Aleph(1)
                                   Type: CardinalNumber
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPageEmpty19}
\begin{paste}{CardinalNumberXmpPageEmpty19}{CardinalNumberXmpPagePatch19}
\pastebutton{CardinalNumberXmpPageEmpty19}{\showpaste}
\tab{5}\spadcommand{c := 2**a\free{a }\bound{c }}
\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPagePatch20}
\begin{paste}{CardinalNumberXmpPageFull20}{CardinalNumberXmpPageEmpty20}
\pastebutton{CardinalNumberXmpPageFull20}{\hidepaste}
\tab{5}\spadcommand{f := 2**c\free{c }\bound{f }}
\indentrel{3}\begin{verbatim}
   (20)  Aleph(2)
                                   Type: CardinalNumber
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}

\begin{patch}{CardinalNumberXmpPageEmpty20}
\begin{paste}{CardinalNumberXmpPageEmpty20}{CardinalNumberXmpPagePatch20}
\pastebutton{CardinalNumberXmpPageEmpty20}{\showpaste}
\tab{5}\spadcommand{f := 2**c\free{c }\bound{f }}
\end{paste}\end{patch}
Product

Resources

Company
