-
Notifications
You must be signed in to change notification settings - Fork 0
/
4agents.sagews
executable file
·16 lines (7 loc) · 6.89 KB
/
4agents.sagews
1
2
3
4
5
6
7
︠30948c53-04c4-4702-a181-b5dcd0253af3s︠
load("4agents.sage")
︡4c1f1605-2089-409d-9b8b-210ae8561fd1︡︡{"stdout":"class Pref defined.\n","done":false}︡{"done":true}
︠6526f052-d624-4a3c-afad-962cbf725d4es︠
prove_4pieces()
︡eb8b7e2a-0a8c-454c-bd64-c0666ec579f5︡︡{"stdout":"Initially, agent a cuts four equal pieces: 1,2,3,4 .\nAssume w.l.o.g. that b's preferences are 1<2<3<4 .\nConsider the following 24 cases regarding the preferences of c:\n\nCASE 1 OF 24 : c's order is 4<3<2<1 :\n b:Equalize(2) makes b's best pieces: 3=4b. This always succeeds.","done":false}︡{"stdout":"\n\nCASE 2 OF 24 : c's order is 4<3<1<2 :\n b:Equalize(2) makes b's best pieces: 3=4b. This always succeeds.\n\nCASE 3 OF 24 : c's order is 4<2<3<1 :\n b:Equalize(2) makes b's best pieces: 3=4b. This always succeeds.\n\nCASE 4 OF 24 : c's order is 4<2<1<3 :\n b:Equalize(2) makes b's best pieces: 3=4b. This must fail because of c.\n c:Equalize(2) makes c's best pieces: 1=3c. This always succeeds.\n\nCASE 5 OF 24 : c's order is 4<1<3<2 :\n b:Equalize(2) makes b's best pieces: 3=4b. This always succeeds.\n\nCASE 6 OF 24 : c's order is 4<1<2<3 :\n b:Equalize(2) makes b's best pieces: 3=4b. This must fail because of c.\n c:Equalize(2) makes c's best pieces: 2=3c. This always succeeds.\n\nCASE 7 OF 24 : c's order is 3<4<2<1 :\n b:Equalize(2) makes b's best pieces: 3=4b. This always succeeds.\n\nCASE 8 OF 24 : c's order is 3<4<1<2 :\n b:Equalize(2) makes b's best pieces: 3=4b. This always succeeds.\n\nCASE 9 OF 24 : c's order is 3<2<4<1 :\n b:Equalize(2) makes b's best pieces: 3=4b. This always succeeds.\n\nCASE 10 OF 24 : c's order is 3<2<1<4 :\n b:Equalize(2) makes b's best pieces: 3=4b. This may fail in 1 case : c prefers 4b to 1 2 3 .\n Assume the case c prefers 4b to 1 2 3. Then:\n c:Equalize(2) makes c's best pieces: 1=4c, so globally: 4c<4b . This always succeeds.\n\nCASE 11 OF 24 : c's order is 3<1<4<2 :\n b:Equalize(2) makes b's best pieces: 3=4b. This always succeeds.\n\nCASE 12 OF 24 : c's order is 3<1<2<4 :\n b:Equalize(2) makes b's best pieces: 3=4b. This may fail in 1 case : c prefers 4b to 1 2 3 .\n Assume the case c prefers 4b to 1 2 3. Then:\n c:Equalize(2) makes c's best pieces: 2=4c, so globally: 4c<4b . This always succeeds.\n\nCASE 13 OF 24 : c's order is 2<4<3<1 :\n b:Equalize(2) makes b's best pieces: 3=4b. This always succeeds.\n\nCASE 14 OF 24 : c's order is 2<4<1<3 :\n b:Equalize(2) makes b's best pieces: 3=4b. This must fail because of c.\n c:Equalize(2) makes c's best pieces: 1=3c. This always succeeds.\n\nCASE 15 OF 24 : c's order is 2<3<4<1 :\n b:Equalize(2) makes b's best pieces: 3=4b. This always succeeds.\n\nCASE 16 OF 24 : c's order is 2<3<1<4 :\n b:Equalize(2) makes b's best pieces: 3=4b. This may fail in 1 case : c prefers 4b to 1 2 3 .\n Assume the case c prefers 4b to 1 2 3. Then:\n c:Equalize(2) makes c's best pieces: 1=4c, so globally: 4c<4b . This always succeeds.\n\nCASE 17 OF 24 : c's order is 2<1<4<3 :\n b:Equalize(2) makes b's best pieces: 3=4b. This must fail because of c.\n c:Equalize(2) makes c's best pieces: 4=3c. This must fail because of b.\n b:Equalize(3) makes b's best pieces: 2=3bb=4bb. This may fail in 1 case : c prefers 1 to 2 3bb 4bb .\n Assume the case c prefers 1 to 2 3bb 4bb. Then:\n c:Equalize(3) makes c's best pieces: 1=4cc=3cc, so globally: 4bb<4cc 3bb<3cc . This always succeeds.\n\nCASE 18 OF 24 : c's order is 2<1<3<4 :\n b:Equalize(2) makes b's best pieces: 3=4b. This may fail in 2 cases : c prefers 4b to 1 2 3; c prefers 3 to 1 2 4b .\n Assume the case c prefers 4b to 1 2 3. Then:\n c:Equalize(2) makes c's best pieces: 3=4c, so globally: 4c<4b . This may fail in 1 case : b prefers 3 to 2 1 4c .\n Assume the case b prefers 3 to 2 1 4c. Then:\n b:Equalize(3) makes b's best pieces: 2=3bb=4bb. This may fail in 1 case : c prefers 1 to 2 3bb 4bb .\n Assume the case c prefers 1 to 2 3bb 4bb. Then:\n c:Equalize(3) makes c's best pieces: 1=3cc=4cc, so globally: 3bb<3cc 4bb<4cc . This always succeeds.\n Assume the case c prefers 3 to 1 2 4b. Then:\n c:Equalize(2) makes c's best pieces: 3=4c, so globally: 4b<4c . This may fail in 1 case : b prefers 4c to 2 1 3 .\n Assume the case b prefers 4c to 2 1 3. Then:\n b:Equalize(3) makes b's best pieces: 2=3bb=4bb. This may fail in 1 case : c prefers 1 to 2 3bb 4bb .\n Assume the case c prefers 1 to 2 3bb 4bb. Then:\n c:Equalize(3) makes c's best pieces: 1=3cc=4cc, so globally: 3bb<3cc 4bb<4cc . This always succeeds.\n\nCASE 19 OF 24 : c's order is 1<4<3<2 :\n b:Equalize(2) makes b's best pieces: 3=4b. This always succeeds.\n\nCASE 20 OF 24 : c's order is 1<4<2<3 :\n b:Equalize(2) makes b's best pieces: 3=4b. This must fail because of c.","done":false}︡{"stdout":"\n c:Equalize(2) makes c's best pieces: 2=3c. This always succeeds.\n\nCASE 21 OF 24 : c's order is 1<3<4<2 :\n b:Equalize(2) makes b's best pieces: 3=4b. This always succeeds.\n\nCASE 22 OF 24 : c's order is 1<3<2<4 :\n b:Equalize(2) makes b's best pieces: 3=4b. This may fail in 1 case : c prefers 4b to 1 2 3 .\n Assume the case c prefers 4b to 1 2 3. Then:\n c:Equalize(2) makes c's best pieces: 2=4c, so globally: 4c<4b . This always succeeds.\n\nCASE 23 OF 24 : c's order is 1<2<4<3 :\n b:Equalize(2) makes b's best pieces: 3=4b. This must fail because of c.\n c:Equalize(2) makes c's best pieces: 4=3c. This must fail because of b.\n b:Equalize(3) makes b's best pieces: 2=3bb=4bb. This may fail in 1 case : c prefers 2 to 1 3bb 4bb .\n Assume the case c prefers 2 to 1 3bb 4bb. Then:\n c:Equalize(3) makes c's best pieces: 2=4cc=3cc, so globally: 4bb<4cc 3bb<3cc . This always succeeds.\n\nCASE 24 OF 24 : c's order is 1<2<3<4 :\n b:Equalize(2) makes b's best pieces: 3=4b. This may fail in 2 cases : c prefers 4b to 1 2 3; c prefers 3 to 1 2 4b .\n Assume the case c prefers 4b to 1 2 3. Then:\n c:Equalize(2) makes c's best pieces: 3=4c, so globally: 4c<4b . This may fail in 1 case : b prefers 3 to 1 2 4c .\n Assume the case b prefers 3 to 1 2 4c. Then:\n b:Equalize(3) makes b's best pieces: 2=3bb=4bb. This may fail in 1 case : c prefers 2 to 1 3bb 4bb .\n Assume the case c prefers 2 to 1 3bb 4bb. Then:\n c:Equalize(3) makes c's best pieces: 2=3cc=4cc, so globally: 3bb<3cc 4bb<4cc . This always succeeds.\n Assume the case c prefers 3 to 1 2 4b. Then:\n c:Equalize(2) makes c's best pieces: 3=4c, so globally: 4b<4c . This may fail in 1 case : b prefers 4c to 1 2 3 .\n Assume the case b prefers 4c to 1 2 3. Then:\n b:Equalize(3) makes b's best pieces: 2=3bb=4bb. This may fail in 1 case : c prefers 2 to 1 3bb 4bb .\n Assume the case c prefers 2 to 1 3bb 4bb. Then:\n c:Equalize(3) makes c's best pieces: 2=3cc=4cc, so globally: 3bb<3cc 4bb<4cc . This always succeeds.\n\nQ.E.D!\n","done":false}︡{"done":true}
︠fd82f05e-4e57-455e-bf7c-716831577f67︠