### 3 Derived Constructs

Frequently used derived constructs are listed in Table 36.

Table 3: Frequently used non-temporal derived constructs
 false ≜ ¬true false value f1 ∨ f2 ≜ ¬(¬f1 ∧¬f2) or f1 ⊃f2 ≜ ¬f1 ∨ f2 implies f1 ≡ f2 ≜ (f1 ⊃f2) ∧ (f2 ⊃f1) equivalent ∃v f ≜ ¬∀v ¬f exists

Table 4: Frequently used temporal derived constructs
 f ≜ skip ; f next more ≜ true non-empty interval empty ≜ ¬more empty interval inf ≜ true ; false inﬁnite interval isinf(f) ≜ inf ∧ f is inﬁnite ﬁnite ≜ ¬inf ﬁnite interval isﬁn(f) ≜ ﬁnite ∧ f is ﬁnite fmore ≜ more ∧ ﬁnite non-empty ﬁnite interval f ≜ ﬁnite ; f sometimes f ≜ ¬¬f always f ≜ ¬¬f weak next f ≜ f ; true some initial subinterval f ≜ ¬( ¬f) all initial subintervals f ≜ ﬁnite ; f ; true some subinterval f ≜ ¬( ¬f) all subintervals

Table 5: Frequently used concrete derived constructs
 if f0 then f1 else f2 ≜ (f0 ∧ f1) ∨ (¬f0 ∧ f2) if then else if f0 then f1 ≜ if f0 then f1 else true if then ﬁn f ≜ (empty ⊃f) ﬁnal state sﬁn f ≜ ¬(ﬁn(¬f)) strong ﬁnal state halt f ≜ (empty ≡ f) terminate interval when shalt f ≜ ¬(halt(¬f)) strong terminate interval when keep f ≜ (skip ⊃f) all unit subintervals keepnow f ≜ (skip ∧ f) initial unit subinterval fω ≜ isinf(isﬁn(f)∗) inﬁnite chopstar fstar(f) ≜ isﬁn(isﬁn(f)∗) ∨ isﬁn(isﬁn(f)∗) ; isinf(f) ﬁnite chopstar while f0 do f1 ≜ (f0 ∧ f1)∗∧ ﬁn ¬f0 while loop repeat f0 until f1 ≜ f0 ; (while ¬f1 do f0) repeat loop

Table 6: Frequently used derived constructs related to expressions
 A := exp ≜ A = exp assignment A ≈ exp ≜ (A = exp) equal in interval A ← exp ≜ ﬁnite ∧ (ﬁn A) = exp temporal assignment A gets exp ≜ keep(A ← exp) gets stable A ≜ A gets A stability padded A ≜ (stable(A) ; skip) ∨ empty padded expression A <∼ exp ≜ (A ← exp) ∧ padded A padded temporal assignment goodindex A ≜ keep(A ← A ∨ A ← A + 1) increasing index intlen(exp) ≜ ∃I (I = 0) ∧ (I gets I + 1) ∧ (I ← exp) interval length

 2018-03-10 Contact | Home | ITL home | Course | Proofs | Algebra | FL