-
Notifications
You must be signed in to change notification settings - Fork 88
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Surreal 4 #4243
Conversation
In the comment of sltn0, should not A and B be X and Y ? |
set.mm
Outdated
$( If ` B ` is conitial with ` C ` and ` A ` precedes ` C ` , then ` A ` | ||
precedes ` B ` . (Contributed by Scott Fenton, 24-Sep-2024.) $) | ||
coinitsslt $p |- ( ( B e. ~P No /\ | ||
A. x e. B E. y e. C y <s x /\ A <<s C ) -> A <<s B ) $= |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
conitial > coinitial
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fixed
set.mm
Outdated
sssslt1 $p |- ( ( A <<s B /\ C C_ A ) -> C <<s B ) $= | ||
( vx vy csslt wbr wss wa cvv wcel csur cslt wral w3a ssltex1 adantr simpr | ||
cv ssexd ssltex2 ssltss1 sstrd ssltss2 ssltsep ssralv mpan9 3jca brsslt | ||
syl21anbrc ) ABFGZCAHZIZCJKBJKZCLHZBLHZDSESMGEBNZDCNZOCBFGUMCAJUKAJKULABP | ||
QUKULRZTUKUNULABUAQUMUOUPURUMCALUSUKALHULABUBQUCUKUPULABUDQUKUQDANULURDEA | ||
BUEUQDCAUFUGUHDECBUIUJ $. | ||
( vx vy csslt wbr wss wa cvv wcel ssltex1 adantr simpr ssexd ssltex2 csur | ||
ssltss1 sstrd cv ssltss2 cslt simp1l simp1r simp2 sseldd ssltsepc syl3anc | ||
w3a simp3 ssltd ) ABFGZCAHZIZDECBJJUNCAJULAJKUMABLMULUMNZOULBJKUMABPMUNCA | ||
QUOULAQHUMABRMSULBQHUMABUAMUNDTZCKZETZBKZUIZULUPAKUSUPURUBGULUMUQUSUCUTCA | ||
UPULUMUQUSUDUNUQUSUEUFUNUQUSUJABUPURUGUHUK $. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
this proof gets longer
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
New proof
ssltun1 $p |- ( ( A <<s C /\ B <<s C ) -> ( A u. B ) <<s C ) $= | ||
( vx vy csslt wbr wa cvv wcel csur wss wral ssltex1 adantr ssltss1 adantl | ||
cv ssltsep sylanbrc cun w3a unexg syl2an ssltex2 jca unssd ssltss2 ralunb | ||
cslt 3jca brsslt ) ACFGZBCFGZHZABUAZIJZCIJZHUPKLZCKLZDRERUJGECMZDUPMZUBUP | ||
CFGUOUQURUMAIJBIJUQUNACNBCNABIIUCUDUMURUNACUEOUFUOUSUTVBUOABKUMAKLUNACPOU | ||
NBKLUMBCPQUGUNUTUMBCUHQUOVADAMZVADBMZVBUMVCUNDEACSOUNVDUMDEBCSQVADABUITUK | ||
DEUPCULT $. | ||
( vx vy csslt wbr cvv wcel ssltex1 adantr adantl csur ssltss1 cv ssltsepc | ||
wss wi 3exp com12 wa cun unexd ssltex2 unssd ssltss2 cslt elun jaoi sylbi | ||
wo 3imp21 ssltd ) ACFGZBCFGZUAZDEABUBZCHHUPABHHUNAHIUOACJKUOBHIUNBCJLUCUN | ||
CHIUOACUDKUPABMUNAMQUOACNKUOBMQUNBCNLUEUNCMQUOACUFKDOZUQIZUPEOZCIZURUTUGG | ||
ZUSURAIZURBIZUKUPVAVBRZRZURABUHVCVFVDUPVCVEUNVCVERUOUNVCVAVBACURUTPSKTUPV | ||
DVEUOVDVERUNUOVDVAVBBCURUTPSLTUIUJULUM $. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
this proof gets longer
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
New proof
Fixed |
Some basic surreal work. I got a little stuck in the past few weeks, so I thought it would be best to send along what I've got. Easiest to review via file view.