IndisputableMonolith.Verification.WallpaperEndogenousBridge

declarations in this module (13)

• def W_endogenous L36
• theorem W_endogenous_formula L41
• theorem W_endogenous_at_D3 L46
• theorem W_endogenous_matches_wallpaper_groups L50
• theorem decomposition_at_D3 L55
• def unique17ScanUpTo64 L60
• theorem unique17ScanUpTo64_true L63
• def W_from_cube L67
• theorem W_from_cube_eq_17 L69
• theorem W_from_cube_eq_wallpaper_groups L72
• theorem wallpaper_slot_iff_endogenous_formula L77
• theorem wallpaper_slot_unique_from_endogenous_formula L95
• theorem endogenous_wallpaper_bridge_complete L102