Documentation

Projects.Expr.Basic

source
def List.wfLex {α : Type u_1} [LT α] (xs ys : List α) :
Prop
Equations
Instances For
    source
    theorem List.length_le_of_wfLex {α : Type u_1} {xs ys : List α} [ha : LT α] (h : xs.wfLex ys) :
    xs.length ≤ ys.length
    source
    @[simp]
    theorem Expr.isNil_nil :
    nil.isNil
    source
    @[simp]
    theorem Expr.not_isNil_pair {a b : Expr} :
    ¬(a.pair b).isNil
    source
    @[simp]
    theorem Expr.not_isPair_nil :
    ¬nil.isPair
    source
    @[simp]
    theorem Expr.isPair_pair {a b : Expr} :
    (a.pair b).isPair
    source
    @[simp]
    theorem Expr.fst_nil :
    nil.fst = nil
    source
    @[simp]
    theorem Expr.snd_nil :
    nil.snd = nil
    source
    @[simp]
    theorem Expr.fst_pair {a b : Expr} :
    (a.pair b).fst = a
    source
    @[simp]
    theorem Expr.snd_pair {a b : Expr} :
    (a.pair b).snd = b
    source
    @[simp]
    theorem Expr.toPair_nil :
    nil.toPair = nil.pair nil
    source
    @[simp]
    theorem Expr.toPair_pair {a b : Expr} :
    (a.pair b).toPair = a.pair b
    source
    @[simp]
    theorem Expr.ite_nil {a b : Expr} :
    nil.ite a b = b
    source
    @[simp]
    theorem Expr.ite_pair {a b c d : Expr} :
    (a.pair b).ite c d = c
    source
    @[simp]
    theorem Expr.ite_toPair {a b c : Expr} :
    a.toPair.ite b c = b
    source
    @[simp]
    theorem Expr.not_isNil_T :
    ¬T.isNil
    source
    @[simp]
    theorem Expr.isNil_F :
    F.isNil
    source
    @[simp]
    theorem Expr.isPair_T :
    T.isPair
    source
    @[simp]
    theorem Expr.not_F :
    ¬F.isPair
    source
    @[simp]
    theorem Expr.not_nil_and {a : Expr} :
    ¬(nil.and a).isPair
    source
    @[simp]
    theorem Expr.isPair_toPair {a : Expr} :
    a.toPair.isPair
    source
    @[simp]
    theorem Expr.toProp_nil :
    nil.toProp = F
    source
    @[simp]
    theorem Expr.toProp_pair {a b : Expr} :
    (a.pair b).toProp = T
    source
    @[simp]
    theorem Expr.isPair_toProp {a : Expr} :
    a.toProp.isPair ↔ a.isPair
    source
    @[simp]
    theorem Expr.and_iff {a b : Expr} :
    (a.and b).isPair ↔ a.isPair ∧ b.isPair
    source
    theorem Expr.cases {p : Expr → Expr → Expr} {f : Expr → Expr} (h : ∀ (x : Expr), ((p x nil).and (p x (f x).toPair)).isPair) (x : Expr) :
    (p x (f x)).isPair
    source
    theorem Expr.ind {p : Expr → Expr} (h : ∀ (x : Expr), ((p nil).and (p x.toPair)).isPair) (x : Expr) :
    (p x).isPair
    source
    @[simp]
    theorem Expr.eq_iff {a b : Expr} :
    (a.eq b).isPair ↔ a = b
    source
    theorem Expr.le_def {a b : Expr} :
    a ≤ b ↔ (a.sle b).isPair
    source
    theorem Expr.lt_def {a b : Expr} :
    a < b ↔ (a.slt b).isPair
    source
    @[simp]
    theorem Expr.le_refl {a : Expr} :
    a ≤ a
    source
    @[simp]
    theorem Expr.not_lt_nil {a : Expr} :
    ¬a < nil
    source
    @[simp]
    theorem Expr.nil_le {a : Expr} :
    nil ≤ a
    source
    @[simp]
    theorem Expr.or_iff {a b : Expr} :
    (a.or b).isPair ↔ a.isPair ∨ b.isPair
    source
    @[simp]
    theorem Expr.nil_lt_iff {a : Expr} :
    nil < a ↔ a.isPair
    source
    @[simp]
    theorem Expr.pair_ne_fst {a b : Expr} :
    a.pair b ≠ a
    source
    @[simp]
    theorem Expr.pair_ne_snd {a b : Expr} :
    a.pair b ≠ b
    source
    @[simp]
    theorem Expr.fst_ne_pair {a b : Expr} :
    a ≠ a.pair b
    source
    @[simp]
    theorem Expr.snd_ne_pair {a b : Expr} :
    b ≠ a.pair b
    source
    @[simp]
    theorem Expr.depth'_nil :
    nil.depth' = 0
    source
    @[simp]
    theorem Expr.depth'_pair {a b : Expr} :
    (a.pair b).depth' = 1 + max a.depth' b.depth'
    source
    @[simp]
    theorem Expr.depth'_eq_zero_iff {a : Expr} :
    a.depth' = 0 ↔ a = nil
    source
    theorem Expr.depth'_le_of_le {a b : Expr} (h : a ≤ b) :
    a.depth' ≤ b.depth'
    source
    @[simp]
    theorem Expr.not_pair_le_fst {a b : Expr} :
    ¬a.pair b ≤ a
    source
    @[simp]
    theorem Expr.not_pair_le_snd {a b : Expr} :
    ¬a.pair b ≤ b
    source
    @[simp]
    theorem Expr.lt_irrefl {a : Expr} :
    ¬a < a
    source
    theorem Expr.not_pair_le_nil {a b : Expr} :
    ¬a.pair b ≤ nil
    source
    @[simp]
    theorem Expr.le_nil_iff {a : Expr} :
    a ≤ nil ↔ a = nil
    source
    theorem Expr.le_iff_eq_or_lt {a b : Expr} :
    a ≤ b ↔ a = b ∨ a < b
    source
    theorem Expr.lt_iff_le_and_ne {a b : Expr} :
    a < b ↔ a ≤ b ∧ ¬(a.eq b).isPair
    source
    theorem Expr.le_of_lt {a b : Expr} (h : a < b) :
    a ≤ b
    source
    @[simp]
    theorem Expr.lt_pair_iff {a b c : Expr} :
    a < b.pair c ↔ a ≤ b ∨ a ≤ c
    source
    theorem Expr.depth'_lt_of_lt {a b : Expr} (h : a < b) :
    a.depth' < b.depth'
    source
    theorem Expr.depth'_le_of_lt {a b : Expr} (h : a < b) :
    a.depth' ≤ b.depth'
    source
    @[simp]
    theorem Expr.not_pair_lt_fst {a b : Expr} :
    ¬a.pair b < a
    source
    @[simp]
    theorem Expr.not_pair_lt_snd {a b : Expr} :
    ¬a.pair b < b