Hi,
I have this proof goal, where I need to prove that two sets are equal.
{{f i | i IN if a IN {b | b IN L} then s1 a else s2 a} |
a |
a IN if j IN L then s3 j else s4 j} =
{{f i | i IN if a IN {b | b IN L} then s1 a else s2 a} |
a IN if j IN L then s3 j else s4 j}
I have two questions regarding this proof, first, what is the difference
between the first format when we use "|a | a IN...." (the left side of the
goal) and the second format "...|a IN..." (the right side of the goal)?
Secondly, are these sets equal? because it seems that HOL treats set L in
the right side of the goal as a dummy variable of the set.
I need help in clarifying the difference between both formats and some
clues about how to proceed with the proof if the sets are equal.
Best Regards,
Yassmeen Elderhalli
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
