[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] proving a property of some predefined set item
- From: Алексей Тимаков <timakov.alan@xxxxxxxxx>
- Date: Wed, 16 Feb 2022 13:21:24 -0800 (PST)
- Ironport-data: A9a23:OhgfVa8hlVDAx8gFacdGDrUDHnuTJUtcMsCJ2f8bNWPcYEJGY0x3y mFNUWyEa/eLazb1L9twPou39x5U6JXWx9FnTQpoqi1EQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHvylYAL9EngZqTVMEU/Nsjo+3b5p6mJUqYLhWVnV4 4qs+5e31GKNglaYDEpEs8pvlzs05JweiBtA1rDpTa0jUPf2zhH5PbpHTU2DByOQrrp8QoZWc 93+IISRpQs1yfuC5uSNyd4XemVSKlLb0JPnZnB+A8BOiTAazsA+PzpS2Pc0MS9qZzu1c99Z7 u1ulrLge18QD6zJo/wsckFRFz1TFPgTkFPHCSDXXc27ykTHdz7rwqwrAhhmYMsX/eF4BWwI/ vsdQNwPRkrb1qTmnfTiFLYq35R+RCXoFNt3VnVI0TXQFfI7WtPJRa7gzuR/5BAQ2v0SOtz0T vUmVgVORTHvWjBsZ2wxKKIXtOivgXb7fjJCr0+Nvuw85G27IAlZiuGya4eOI4PiqcN9u2Gh9 37EvD7ALFIEBu66imuY8U/xibqa9c/8cNtKSOfQGuRRqFGS3WcOEwY+SV+y5/yikAu/XcheI goV/DAvpO487iSWosLVWhS5pDuDv0dZVYMATqs17waCzqeS6AGcboQZctJfQPoel+wYFQ5y7 26ImujxNB03ubmJZFvIo994sgiOESQSKGYDYwoNQg0E/8TvrekPYvTnHoYL/Emd3o2dJN3g/ 9yZhHNh2OhL3Kbnw43+rA+X2Wv9znTcZldtvl2/Y46z0u9uiGeYi2GA7FHa6bNHLd/cQADR4 T4LnM+R6O1IBpaI/MBsfAnvNO7zjxpmGGeH6bKKI3XH32jyk5JEVd0IiAyS3G8zbq45lcbBO Sc/Qz956p5JJ2eNZqRqeY+3AMlC5fG+SYi0CqGENoIVPMkZmOq7EMdGNR74M4fFwBhErE3DE crznTuEUSxDUvw+lFJauc9HieNznkjSOl8/tbiil0j9uVZvTHGSTrgBPTOzghMRvcu5TPHu2 48Hb6Oikk0BOMWnO3m/2dNNcTgicCZqbbir+50/XrPSfmJORTBxY9ePmulJU9I+wMxoehLgr xlRrGcFkAKn7ZAGQC3RAk1ehETHB8Yv9ylqYnZ1YD5FGRELOO6S0UvWTLNvFZFPyQCp5acco yAtd5rSD/JRZC7A/jhBP5DxoJY7KkakggWBOyeqej8iZ4UmTAvMo4e2cgzq/SgILyy2qcpv8 +b7j1iEH8UOF1Z4EcLbSPOz1Fft73ITr+R/AhnTKd5JdUSwrYVncnSjjvI+L8wWBw/Ewz+Wi 1SfDRsC9LvCpoY09J/CgqXd99WlFO53H0x7GWjH7ObuZXOKoDb7mYIZCbSGZzHQUm/w6Z6OX +QNwqGuKuADkXZLr5F4TORmwKc40N3l+O1XwwFiK3PUNgj5B75lJE6G6slBrKh6wLFU5FmtU UWV99gGYLiENZq+Ql4cLQYodN6OzfUFhj7W4ahnKUn2/nYprrWAVkpWMhaWjzFFN/1+N4Z8m bUtv8sf6gqejBs2M4fW1XsNrDvScXFQAb86spw6AZPwjlZ5wF91Z5GBWDT954uCaokRP0Qnf m2Uia7Fi+gOz0bOaSBvR33E3O4YgpVX/R4TnAJEKFOOld7IwPQw2UQJozgwSw1UyDRB0v5ya jc3bRwrff3W8mc6ntVHUkCtBxpFWE+T9Hv3xgZbj2beVUSpCjHAITxvPeeW4H0f6H9WejQHr riUxHy7AWTvdcD1wixgVklipPjuQsZ26xXZ3cWuGc2KEtphPmq03vLwNTVR8kWkHMUqmUfcr vNr9utYZqr8OiodrLc8FpGBk78XTUncdmBFRPhg+oIPHH3dKWHpgmHVdB7ud5MfPeHO/G+5F 9dqepBFWSO42XvctTscH6MNf+J5kfJ1ttMOdqm3dDwGr6eHtWgu953K8TXmnykkRNJhlct7I YTUMD2YFXGIwmdQknfJsdIDIXeyetIeZQfx0e3pov8FEYkP7LNlfU0oiOfmunyUNE5g/kvRs lqTOunZyOttzYkqlIzpS/0RCwKxINL1deKJ7AHj7IgUPI2XaZ/D51EPt13qHwVKJr9NCd55o rKA7Yzs10TfsbdqDm3UlvFtzUWSCRlegQaWDi72EJWetS6LWcup5Bpavm7hecEPn9Ra6c2qA QC/baNcsDLTt8h1nBVoh+p2Sn7xyJgbqo/voiSyq/mDEB8AyReBJ9SinZMsRX8ObTcGYvUSF Set08tDJblkQEBkCxgDCPVrDIV/PUf4H6AhcrUdcNVe4naA2ju/h1cpqfbsBfwnxJVJ/AYWL K8pniTDSSk=
- Ironport-hdrordr: A9a23:/tXGxK5GiIipxW7CWgPXwD7XdLJyesId70hD6qkRc20oTiX8ra rCoB11726TtN98YgBYpThvUJPwNk812/ZOkP0s1PSZLXrbUFLBFvAW0WKa+UyXJ8SczJ8h6U /UGJIOeOEYc2IK9voSuzPIYurIqePvmMvY55a7854Kd3AVV0hO1WhE422gYzdLrWd9dOIE/F v13Lslm9NiQxoqhwaAakXs74P41q/2fV7dACLv93UcmXazZPqTiM+eYn+l4is=
- Ironport-sdr: wt5BzpZtGFwaKS4baZZz9o/LYBPaZ+gnT1s2yGpXdUo49ql5tmo0PzOdH/wQJ6mwDtUzF45UKr /cVTN/nvdaHGUhYnF8Tbr3lrQy5LmA2mb2+IKUdhWNEqqBL0gLY4MhM7XqHtD1ayqmx40wGuhJ TE1nWU/L3BcM/FAl2sHOk+6+XKxW5s1UCBInyY1jU5F6/08sl42Xyz9LqTDjWKhNw6jYBQgmw+ HKJKrljaLHXxXLY9KJfiT4pXwGys5gtrAWqt0nr8ojI4BictYw4c1K2KqPyqcfknYXjKyHvrQS fkAWNMen+Et/ptuYA/kbAcQM
Hi all.
I'm a newbie on TLAPS and need some help.
Can not manage to prove a simple fact
LEMMA LEM1 == ASSUME NEW S1, NEW S2,
NEW Set \in SUBSET {<<x, y>> : x \in S1, y \in S2},
NEW p \in Set
PROVE p[1] \in S1
OBVIOUS
Set of tuples is not supported.
However
LEMMA LEM2 == ASSUME NEW S1,
NEW Set \in SUBSET {x : x \in S1},
NEW p \in Set
PROVE p \in S1
OBVIOUS
works.
Should we accept LEMMA1 as an axiom?
Thanks in advance.
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/27027cc2-b30b-4efa-a6bd-7dee86f8235bn%40googlegroups.com.