noncomputable def ISAR.InvariantLayer.empty : InvariantLayer

Equations

• ISAR.InvariantLayer.empty = ISAR.HF_encode HF.empty

noncomputable def ISAR.InvariantLayer.pair (x y : InvariantLayer) : InvariantLayer

Equations

• x.pair y = ISAR.HF_encode ((ISAR.decode_layer x).pair (ISAR.decode_layer y))

noncomputable def ISAR.InvariantLayer.union (x y : InvariantLayer) : InvariantLayer

Equations

• x.union y = ISAR.HF_encode ((ISAR.decode_layer x).union (ISAR.decode_layer y))

theorem ISAR.HF_encode_empty : HF_encode HF.empty = InvariantLayer.empty

theorem ISAR.HF_encode_pair (x y : HF) : HF_encode (x.pair y) = (HF_encode x).pair (HF_encode y)

theorem ISAR.HF_encode_union (x y : HF) : HF_encode (x.union y) = (HF_encode x).union (HF_encode y)