In z_app_thm, which states
∀ a : 𝕌; f : 𝕌; x : 𝕌
⦁ (∀ f_a : 𝕌 | (a, f_a) ∈ f ⦁ f_a = x) ∧ (a, x) ∈ f ⇒ f a = x
I notice that the antecedent
(a, x) ∈ f
does not actually need to map a to x because that is already captured in
the first antecedent. It only needs to say that a is in the domain of
f, so the theorem could state
∀ a : 𝕌; f : 𝕌; x, y : 𝕌
⦁ (∀ f_a : 𝕌 | (a, f_a) ∈ f ⦁ f_a = x) ∧ (a, y) ∈ f ⇒ f a = x
As it stands, I suspect there could be some unnecessary proof overhead
for users (and perhaps in the PP implementation) because it may be
necessary to forward chain with the left antecedent, once established,
and eliminate a variable to get the form required by z_app_thm.
I think other proof operations like z_app_eq_tac and z_app_λ_rule would
naturally become simpler:
- z_app_eq_tac could return a goal containing
... ∧ (∃ v : 𝕌 ⦁ (a, v) ∈ f)
so we can choose any v, instead of
... ∧ (a, v) ∈ f
- z_app_λ_rule would not include the predicate V' = x in the
antecedents.
Phil
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
