Solution to final exam question:

[Adrian Nicoara]

Does anybody have a solution to the:

?k . A[k] = c /\ ~(k=j)
|= ?x . ( A (+) {(i,A[j])}) (+) {(j,A[i])}[x] = c

question on the exam?
I can't figure this one out. Thx

[Woong Bin Kang]

Post by Adrian Nicoara
?k . A[k] = c /\ ~(k=j)
|= ?x . ( A (+) {(i,A[j])}) (+) {(j,A[i])}[x] = c
question on the exam?
I can't figure this one out. Thx

Basically, you introduce k_u
and use LEM to get (k_u=i) \/ (k_u != i)
then you can go on and use case analysis with exists introduction to get
the desired result and finish it off with exists elimination.

In the case analysis, when k_u=i, (btw in this case, i != j)
you get
A+(i,A[j])+(j,A[i])[i]=A[i]
with the defn of override, and use =_E to get the desired result.
When k_u != i, you get
A+(i,A[j])+(j,A[i])[k_u]=A[k_u]
with the defn of override, with the fact that k_u != i and k_u != j.
So you just use exist intro again.
Close all the cases.

I'll post the full solution if you want.


Woongbin.

[Adrian Nicoara]

Post by Woong Bin Kang
In the case analysis, when k_u=i, (btw in this case, i != j)
you get
A+(i,A[j])+(j,A[i])[i]=A[i]

When you are doing:
A+(i,A[j])+(j,A[i])[i] isn't it equal to A[j] by the definition of override?

Post by Woong Bin Kang

Post by Adrian Nicoara
?k . A[k] = c /\ ~(k=j)
|= ?x . ( A (+) {(i,A[j])}) (+) {(j,A[i])}[x] = c
question on the exam?
I can't figure this one out. Thx

Basically, you introduce k_u
and use LEM to get (k_u=i) \/ (k_u != i)
then you can go on and use case analysis with exists introduction to get
the desired result and finish it off with exists elimination.
In the case analysis, when k_u=i, (btw in this case, i != j)
you get
A+(i,A[j])+(j,A[i])[i]=A[i]
with the defn of override, and use =_E to get the desired result.
When k_u != i, you get
A+(i,A[j])+(j,A[i])[k_u]=A[k_u]
with the defn of override, with the fact that k_u != i and k_u != j.
So you just use exist intro again.
Close all the cases.
I'll post the full solution if you want.
Woongbin.

[Woong Bin Kang]

Post by Adrian Nicoara

Post by Woong Bin Kang
In the case analysis, when k_u=i, (btw in this case, i != j)
you get
A+(i,A[j])+(j,A[i])[i]=A[i]

A+(i,A[j])+(j,A[i])[i] isn't it equal to A[j] by the definition of override?

Post by Woong Bin Kang

Post by Adrian Nicoara
?k . A[k] = c /\ ~(k=j)
|= ?x . ( A (+) {(i,A[j])}) (+) {(j,A[i])}[x] = c
question on the exam?
I can't figure this one out. Thx

Basically, you introduce k_u
and use LEM to get (k_u=i) \/ (k_u != i)
then you can go on and use case analysis with exists introduction to
get the desired result and finish it off with exists elimination.
In the case analysis, when k_u=i, (btw in this case, i != j)
you get
A+(i,A[j])+(j,A[i])[i]=A[i]
with the defn of override, and use =_E to get the desired result.
When k_u != i, you get
A+(i,A[j])+(j,A[i])[k_u]=A[k_u]
with the defn of override, with the fact that k_u != i and k_u != j.
So you just use exist intro again.
Close all the cases.
I'll post the full solution if you want.
Woongbin.

I think I wrote down something different on the exam... I'll post again
when I come up with the correct one.
Woongbin

[Woong Bin Kang]

Post by Adrian Nicoara

Post by Woong Bin Kang
In the case analysis, when k_u=i, (btw in this case, i != j)
you get
A+(i,A[j])+(j,A[i])[i]=A[i]

A+(i,A[j])+(j,A[i])[i] isn't it equal to A[j] by the definition of override?

Post by Woong Bin Kang

Post by Adrian Nicoara
?k . A[k] = c /\ ~(k=j)
|= ?x . ( A (+) {(i,A[j])}) (+) {(j,A[i])}[x] = c
question on the exam?
I can't figure this one out. Thx

Basically, you introduce k_u
and use LEM to get (k_u=i) \/ (k_u != i)
then you can go on and use case analysis with exists introduction to
get the desired result and finish it off with exists elimination.
In the case analysis, when k_u=i, (btw in this case, i != j)
you get
A+(i,A[j])+(j,A[i])[i]=A[i]
with the defn of override, and use =_E to get the desired result.
When k_u != i, you get
A+(i,A[j])+(j,A[i])[k_u]=A[k_u]
with the defn of override, with the fact that k_u != i and k_u != j.
So you just use exist intro again.
Close all the cases.
I'll post the full solution if you want.
Woongbin.

A[k_u] =c
k_u = i
k_u != j
i != j

A+(i,A[j])+(j,A[i])[j] = c

?x.A+(i,A[j])+(j,A[i])[x] = c

I think this is *hopefully* what I did on the exam.

This one makes sense.

Woongbin

[Adrian Nicoara]

I still don't get how you got those equalities, with those premises,

Post by Woong Bin Kang
A[k_u] =c
k_u = i
k_u != j
i != j
A+(i,A[j])+(j,A[i])[j] = c
?x.A+(i,A[j])+(j,A[i])[x] = c

but, (A + {(i, A[j])}) + (j,A[i])[j] = (A + {(i, A[j])}) [i] = A[j] (by
defn of override, unless i made a mistake)
, which would not be c...

Let me know if you see a mistake...

Post by Woong Bin Kang

Post by Adrian Nicoara

Post by Woong Bin Kang
In the case analysis, when k_u=i, (btw in this case, i != j)
you get
A+(i,A[j])+(j,A[i])[i]=A[i]

A+(i,A[j])+(j,A[i])[i] isn't it equal to A[j] by the definition of override?

Post by Woong Bin Kang

Post by Adrian Nicoara
?k . A[k] = c /\ ~(k=j)
|= ?x . ( A (+) {(i,A[j])}) (+) {(j,A[i])}[x] = c
question on the exam?
I can't figure this one out. Thx

Basically, you introduce k_u
and use LEM to get (k_u=i) \/ (k_u != i)
then you can go on and use case analysis with exists introduction to
get the desired result and finish it off with exists elimination.
In the case analysis, when k_u=i, (btw in this case, i != j)
you get
A+(i,A[j])+(j,A[i])[i]=A[i]
with the defn of override, and use =_E to get the desired result.
When k_u != i, you get
A+(i,A[j])+(j,A[i])[k_u]=A[k_u]
with the defn of override, with the fact that k_u != i and k_u != j.
So you just use exist intro again.
Close all the cases.
I'll post the full solution if you want.
Woongbin.

A[k_u] =c
k_u = i
k_u != j
i != j
A+(i,A[j])+(j,A[i])[j] = c
?x.A+(i,A[j])+(j,A[i])[x] = c
I think this is *hopefully* what I did on the exam.
This one makes sense.
Woongbin

[Woong Bin Kang]

We all agree on these, right?
A[k_u] =c
k_u = i
k_u != j
i != j

Post by Adrian Nicoara
but,
(A + {(i, A[j])}) + (j,A[i])[j] = (A + {(i, A[j])}) [i] = A[j]

|
i replace this to j

A+(i,A[j])+(j,A[i])[j] is A[i] right after resolving the first
override, and you don't resolve it any further.
This is by defn of override. It resolved from right-most override.
So, since the index j is overriden with A[i], you get A[i].


Array+(i,something)+(j,something2)[j] is something2.

And now the rest follows.

Woongbin

[Adrian Nicoara]

Bah,
I think i finally got what happened...
the right most override references the original array A[i]...
Thanks for helping me understand this...
If only i got this during the exam :-<

Post by Woong Bin Kang
We all agree on these, right?
A[k_u] =c
k_u = i
k_u != j
i != j

Post by Adrian Nicoara
but,
(A + {(i, A[j])}) + (j,A[i])[j] = (A + {(i, A[j])}) [i] = A[j]

|
i replace this to j
A+(i,A[j])+(j,A[i])[j] is A[i] right after resolving the first
override, and you don't resolve it any further.
This is by defn of override. It resolved from right-most override.
So, since the index j is overriden with A[i], you get A[i].
Array+(i,something)+(j,something2)[j] is something2.
And now the rest follows.
Woongbin

[Woong Bin Kang]

Post by Adrian Nicoara
Bah,
I think i finally got what happened...
the right most override references the original array A[i]...
Thanks for helping me understand this...
If only i got this during the exam :-<

No problem.
Honestly, you scared the crap out of me lol! I almost remember making
the first mistake during the exam and fixing it... and now I'm not sure
if I got this question right anymore :( Only time will tell.

Anyways, have a good summer!
Woongbin

[Nancy Day]

Woongbin, Adrian --

Looks like you figured out the solution!

cheers, nancy

Post by Woong Bin Kang

Post by Adrian Nicoara
Bah,
I think i finally got what happened...
the right most override references the original array A[i]...
Thanks for helping me understand this...
If only i got this during the exam :-<

No problem.
Honestly, you scared the crap out of me lol! I almost remember making
the first mistake during the exam and fixing it... and now I'm not sure
if I got this question right anymore :( Only time will tell.
Anyways, have a good summer!
Woongbin

[Woong Bin Kang]

yes, k_u=i is the assumption in the first case created with the LEM.
wbkang