digraph { label="proof" subgraph cluster_not_a { label="not_a" h[shape=triangle] And_left h -> And_left[ label="￢A∧￢B"] } subgraph cluster_not_b { label="not_b" h1[shape=triangle, label="h"] And_right h1 -> And_right[ label="￢A∧￢B"] An…

全部事実上同義語。 平叙文 疑問文 型判断 型質問 シーケント 質問シーケント 関数定義 関数定義要求 定理記述 定理証明要求 クロージャ 大きいラムダ式 大きいタプル 大きいlet式

theorem half_DeMorgan premise h: ￢A∧￢B entails ￢(A∨B) proof we have not_a: ￢A by using And_left with h we have not_b: ￢B by using And_light with h we conclude ￢(A ∨ B) by using Or_tuple with not_a and not_b end 定理 ド・モルガンの半…