I have a Logika file that needs revision for only the justifications and not what is listed in the steps. I have already attempted, but some justifications are incorrect and I need help making it logika verified. Here is the code from the file:

import org.sireum.logika._ // one bit adder simulator // Fill in the justifications val X: Z = readInt() val Y: Z = readInt() // least significant bit of answer var Zlsb: Z = 0 // most SB of answer, sometimes called the "carry" var Zmsb: Z = 0 assume(X == 0 | X == 1) assume(Y == 0 | Y == 1) if (!(X == Y)) { Zlsb =1 l"""{ 1. X == 0 | X == 1 premise 2. Y == 0 | Y == 1 premise 3. (X = Y) premise 19. Zlsb = 1 premise 4. { 5. X == 1 assume 6. { 7. Y = 1 assume 8. X = Y algebra 5 7 9.  e 8 3 10. !(X == Y ) | ( Zlsb == 0) e 9 11. (X == Y ) | ( Zlsb == 1) i1 8 } 12. { 13. Y = 0 assume 14. !(X== Y) algebra 5 13 15. !(X == Y ) | ( Zlsb == 0) i1 14 16. ( X == Y ) | ( Zlsb == 1) i2 19 } 17. !(X == Y ) | ( Zlsb == 0) i 12 18. ( X == Y ) | ( Zlsb == 1) pbc 6 } 20. { 21. X == 0 assume 22. { 23. Y = 1 assume 24. (X = Y) algebra 26. !(X == Y ) | ( Zlsb == 0) i1 24 27. (X == Y ) | ( Zlsb == 1) i2 19 } 28. { 29. Y = 0 assume 30. (X== Y) algebra 35.  e 30 24 31. !(X == Y ) | ( Zlsb == 0) e 35 32. ( X == Y ) | ( Zlsb == 1) i2 19 } 33. !(X == Y ) | ( Zlsb == 0) i 28 34. ( X == Y ) | ( Zlsb == 1) pbc 6 } 40. !(X == Y ) | ( Zlsb == 0) i 20 41. ( X == Y ) | ( Zlsb == 1) pbc 4 }""" }else{ l"""{ 1.!(!(X = Y)) premise 2. X = Y algebra 3. Zlsb = 0 premise 4. !(X == Y ) | ( Zlsb == 0) i2 3 5. (X == Y ) | ( Zlsb == 1) i1 2 }""" } assert(!(X == Y ) | ( Zlsb == 0)) assert((X == Y ) | ( Zlsb == 1))