Frage:
Wir haben jetzt das Thema Programmverifikation mit der Prädikatenlogik. Ich verstehe nicht genau, wie man dies durch die Prädikatenlogik vereinfachen kann:
≡ (i ≥ a.length ⋁ a[i] = x) ⋀ (∀ j : 0 ≤ j < i : a[j] ≠ x) ⋀ i ≤ a.length
≡ (∀ j : 0 ≤ j < i : a[j] ≠ x) ⋀ ((i ≥ a.length ⋀ i ≤ a.length) ⋁ (a[i] = x ⋀ i ≤ a.length))
≡ (∀ j : 0 ≤ j < i : a[j] ≠ x) ⋀ (i = a.length ⋁ (a[i] = x ⋀ i ≤ a.length))
⇛ (∀ j : 0 ≤ j < i : a[j] ≠ x) ⋀ (i = a.length ⋁ a[i] = x)
Kann mir hier jemand helfen, mit welchen Gesetzen, dass gemacht wurde.
